Skip to content
Success

Changes

Summary

  1. spelling;
  2. tuned;
  3. read theory with PIDE markup from session database;
  4. clarified signature: provide XZ.Cache where Export.Entry is created;
  5. tuned signature;
  6. tuned signature;
  7. clarified exports;
  8. clarified markup (refining 1c59b555ac4a);
  9. clarified markup: support more completion, e.g. within ROOTS;
  10. more accurate markup (refining 1c59b555ac4a);
  11. tuned signature --- more operations;
Changeset 72850:4cb480334f48 by wenzelm:
spelling;
The file was modified src/HOL/ROOT (diff)
Changeset 72849:c83883da98d6 by wenzelm:
tuned;
The file was modified src/Pure/Tools/build_job.scala (diff)
Changeset 72848:d5d0e36eda16 by wenzelm:
read theory with PIDE markup from session database;
The file was modified src/Pure/PIDE/command.scala (diff)
The file was modified src/Pure/Tools/build_job.scala (diff)
Changeset 72847:9dda93a753b1 by wenzelm:
clarified signature: provide XZ.Cache where Export.Entry is created;
The file was modified src/Pure/Thy/export.scala (diff)
The file was modified src/Pure/Thy/export_theory.scala (diff)
The file was modified src/Pure/Thy/presentation.scala (diff)
The file was modified src/Pure/Thy/sessions.scala (diff)
The file was modified src/Pure/Tools/dump.scala (diff)
The file was modified src/Pure/Tools/server_commands.scala (diff)
The file was modified src/Tools/jEdit/src/isabelle_export.scala (diff)
Changeset 72846:a23e0964f3c3 by wenzelm:
tuned signature;
The file was modified src/Pure/PIDE/command.scala (diff)
Changeset 72845:60f56f623be2 by wenzelm:
tuned signature;
The file was modified src/Pure/Thy/sessions.scala (diff)
Changeset 72844:240c8a0f6337 by wenzelm:
clarified exports;
The file was modified src/Pure/PIDE/document.scala (diff)
The file was modified src/Pure/Thy/export.scala (diff)
The file was modified src/Pure/Tools/build_job.scala (diff)
Changeset 72843:dd56ba1974e6 by wenzelm:
clarified markup (refining 1c59b555ac4a);
The file was modified src/Pure/PIDE/markup.ML (diff)
The file was modified src/Pure/Thy/document_antiquotations.ML (diff)
Changeset 72842:6aae62f55c2b by wenzelm:
clarified markup: support more completion, e.g. within ROOTS;
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/Tools/update.scala (diff)
Changeset 72841:fd8d82c4433b by wenzelm:
more accurate markup (refining 1c59b555ac4a);
The file was modified src/Pure/PIDE/command.ML (diff)
The file was modified src/Pure/PIDE/markup.ML (diff)
The file was modified src/Pure/PIDE/resources.ML (diff)
The file was modified src/Pure/Pure.thy (diff)
The file was modified src/Pure/Thy/document_antiquotations.ML (diff)
The file was modified src/Pure/Thy/sessions.ML (diff)
The file was modified src/Pure/Tools/generated_files.ML (diff)
The file was modified src/Tools/Code/code_target.ML (diff)
Changeset 72840:6b96464066a0 by wenzelm:
tuned signature --- more operations;
The file was modified src/Pure/General/input.ML (diff)
The file was modified src/Pure/Isar/parse.ML (diff)