Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. expose latex mode operations, to facilitate adhoc changes to it;
  2. tuned signature (see also src/Tools/Haskell/Markup.hs);
  3. tuned spelling;
Changeset 69346:3c29edccf739 by wenzelm:
expose latex mode operations, to facilitate adhoc changes to it;
The file was modified src/Pure/Thy/latex.ML (diff)
Changeset 69345:6bd63c94cf62 by wenzelm:
tuned signature (see also src/Tools/Haskell/Markup.hs);
The file was modified src/Pure/General/pretty.ML (diff)
The file was modified src/Pure/PIDE/markup.ML (diff)
The file was modified src/Pure/PIDE/xml.ML (diff)
Changeset 69344:f87fdd8d2baf by wenzelm:
tuned spelling;
The file was modified src/Pure/Syntax/lexicon.ML (diff)