Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. more robust syntax;
  2. unused;
  3. clarified document export names;
  4. tuned signature;
  5. tuned;
  6. tuned;
  7. avoid former verbose_latex, which has been renamed to verbose in 52030acb19ac;
  8. compose Latex text as XML, output exported YXML in Isabelle/Scala;
  9. more direct index_entry: no positions required -- text is eventually moved to .ind file;
  10. clarified signature;
Changeset 73787:493b1ae188da by wenzelm:
more robust syntax;
The file was modified src/Pure/Pure.thy (diff)
Changeset 73786:18d80cd51823 by wenzelm:
unused;
The file was modified src/Pure/Tools/build.scala (diff)
Changeset 73785:b5fb99b985b4 by wenzelm:
clarified document export names;
The file was modified src/Pure/Thy/document_build.scala (diff)
The file was modified src/Pure/Thy/export.scala (diff)
The file was modified src/Pure/Thy/thy_info.ML (diff)
The file was modified src/Pure/Tools/build_job.scala (diff)
Changeset 73784:04d39959d1e6 by wenzelm:
tuned signature;
The file was modified src/Pure/Thy/document_build.scala (diff)
Changeset 73783:e4d50a660140 by wenzelm:
tuned;
The file was modified src/Pure/Thy/latex.scala (diff)
Changeset 73782:4606a9cadd83 by wenzelm:
tuned;
The file was modified src/Pure/Thy/latex.scala (diff)
Changeset 73781:0909fd14f8a4 by wenzelm:
avoid former verbose_latex, which has been renamed to verbose in 52030acb19ac;
The file was modified src/Pure/Tools/build_job.scala (diff)
Changeset 73780:466fae6bf22e by wenzelm:
compose Latex text as XML, output exported YXML in Isabelle/Scala;
The file was modified src/Doc/antiquote_setup.ML (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/resources.ML (diff)
The file was modified src/Pure/System/scala_compiler.ML (diff)
The file was modified src/Pure/Thy/document_antiquotation.ML (diff)
The file was modified src/Pure/Thy/document_antiquotations.ML (diff)
The file was modified src/Pure/Thy/document_build.scala (diff)
The file was modified src/Pure/Thy/document_output.ML (diff)
The file was modified src/Pure/Thy/latex.ML (diff)
The file was modified src/Pure/Thy/latex.scala (diff)
The file was modified src/Pure/Thy/thy_info.ML (diff)
The file was modified src/Pure/Tools/rail.ML (diff)
Changeset 73779:546e1e591635 by wenzelm:
more direct index_entry: no positions required -- text is eventually moved to .ind file;
The file was modified src/Pure/Thy/latex.ML (diff)
Changeset 73778:a383c4340c25 by wenzelm:
clarified signature;
The file was modified src/Pure/Thy/document_build.scala (diff)