Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. more tight HTML output: avoid extra lines within <pre>;
  2. HTML output for Markdown elements; clarified HTML operations;
Changeset 67337:4254cfd15b00 by wenzelm:
more tight HTML output: avoid extra lines within &lt;pre&gt;;
The file was modified src/Pure/Thy/html.scala (diff)
The file was modified src/Pure/Thy/present.scala (diff)
The file was modified src/Tools/VSCode/src/state_panel.scala (diff)
Changeset 67336:3ee6da378183 by wenzelm:
HTML output for Markdown elements;<br>clarified HTML operations;
The file was modified etc/isabelle.css (diff)
The file was modified src/Pure/PIDE/markup.ML (diff)
The file was modified src/Pure/PIDE/markup.scala (diff)
The file was modified src/Pure/PIDE/rendering.scala (diff)
The file was modified src/Pure/Thy/html.scala (diff)
The file was modified src/Pure/Thy/markdown.ML (diff)
The file was modified src/Pure/Thy/present.scala (diff)