Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. avoid evaluation of embedded comment;
  3. disable "display" style in marginal (line) comment;
  4. more uniform output of source / text / theory_text, with handling of formal comments etc.;
  5. sort completion result;
  6. recovered antiquotation check without latex mode (cf. dfc93f2b01ea);
  7. formal treatment of documentation names;
  8. support for completion;
  9. adapted to a5ca98950a91;
  10. tuned output of plain name;
  11. clarified signature;
  12. tuned;
  13. tuned;
  14. unused;
  15. clarified access to antiquotation options; define explicit variants of antiquotations; output proper Latex.text; misc tuning and clarification;
  16. more operations;
  17. tuned signature;
  18. discontinued unused wrapper: print_mode is provided directly;
  19. corrected name
  20. moved from AFP/Gromov
  21. moved from AFP/Gromov
  22. added lemma
Changeset 67477:056be95db703 by wenzelm:
merged
Changeset 67476:44b018d4aa5f by wenzelm:
avoid evaluation of embedded comment;
The file was modified src/Doc/Isar_Ref/Outer_Syntax.thy (diff)
Changeset 67475:1a279ad4c6a4 by wenzelm:
disable "display" style in marginal (line) comment;
The file was modified src/Pure/Thy/thy_output.ML (diff)
Changeset 67474:90def2b06305 by wenzelm:
more uniform output of source / text / theory_text, with handling of formal comments etc.;
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/thy_output.ML (diff)
Changeset 67473:aad088768872 by wenzelm:
sort completion result;
The file was modified src/Pure/PIDE/resources.ML (diff)
Changeset 67472:7ed8d4cdfb13 by wenzelm:
recovered antiquotation check without latex mode (cf. dfc93f2b01ea);
The file was modified src/Pure/Thy/document_antiquotation.ML (diff)
Changeset 67471:bddfa23a4ea9 by wenzelm:
formal treatment of documentation names;
The file was modified src/Pure/ML/ml_process.scala (diff)
The file was modified src/Pure/PIDE/protocol.ML (diff)
The file was modified src/Pure/PIDE/protocol.scala (diff)
The file was modified src/Pure/PIDE/resources.ML (diff)
The file was modified src/Pure/Thy/document_antiquotations.ML (diff)
The file was modified src/Pure/Thy/sessions.scala (diff)
The file was modified src/Pure/Tools/build.ML (diff)
The file was modified src/Pure/Tools/build.scala (diff)
The file was modified src/Pure/Tools/doc.scala (diff)
Changeset 67470:d36fcde7e2c0 by wenzelm:
support for completion;
The file was modified etc/symbols (diff)
Changeset 67469:008725a1ed52 by wenzelm:
adapted to a5ca98950a91;
The file was modified src/Doc/more_antiquote.ML (diff)
Changeset 67468:aa8c25c528c0 by wenzelm:
tuned output of plain name;
The file was modified src/Doc/antiquote_setup.ML (diff)
The file was modified src/Pure/Thy/document_antiquotations.ML (diff)
Changeset 67467:482b62d694ca by wenzelm:
clarified signature;
The file was modified src/Pure/General/antiquote.ML (diff)
The file was modified src/Pure/Thy/markdown.ML (diff)
Changeset 67466:82bc0d5d1ef3 by wenzelm:
tuned;
The file was modified src/Pure/Thy/document_antiquotation.ML (diff)
Changeset 67465:d1697ac0fcd1 by wenzelm:
tuned;
The file was modified src/Pure/Thy/thy_output.ML (diff)
Changeset 67464:bc8a76d5839a by wenzelm:
unused;
The file was modified src/Pure/General/symbol_pos.ML (diff)
Changeset 67463:a5ca98950a91 by wenzelm:
clarified access to antiquotation options;<br>define explicit variants of antiquotations;<br>output proper Latex.text;<br>misc tuning and clarification;
The file was modified src/Doc/Main/Main_Doc.thy (diff)
The file was modified src/Doc/Prog_Prove/LaTeXsugar.thy (diff)
The file was modified src/Doc/antiquote_setup.ML (diff)
The file was modified src/Doc/more_antiquote.ML (diff)
The file was modified src/HOL/Library/LaTeXsugar.thy (diff)
The file was modified src/HOL/Tools/BNF/bnf_fp_util.ML (diff)
The file was modified src/HOL/Tools/value_command.ML (diff)
The file was modified src/Pure/PIDE/resources.ML (diff)
The file was modified src/Pure/Thy/bibtex.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/thy_output.ML (diff)
The file was modified src/Pure/Tools/jedit.ML (diff)
The file was modified src/Pure/Tools/rail.ML (diff)
The file was modified src/Tools/Code/code_target.ML (diff)
Changeset 67462:c23d9375e661 by wenzelm:
more operations;
The file was modified src/Pure/Thy/latex.ML (diff)
Changeset 67461:aad5c0982c3d by wenzelm:
tuned signature;
The file was modified src/Pure/Thy/latex.ML (diff)
The file was modified src/Pure/Thy/thy_output.ML (diff)
Changeset 67460:dfc93f2b01ea by wenzelm:
discontinued unused wrapper: print_mode is provided directly;
The file was modified src/Pure/Thy/document_antiquotation.ML (diff)
Changeset 67459:7264dfad077c by nipkow:
corrected name
The file was modified src/HOL/Analysis/Connected.thy (diff)
Changeset 67458:e090941f9f42 by nipkow:
moved from AFP/Gromov
The file was modified src/HOL/Conditionally_Complete_Lattices.thy (diff)
Changeset 67457:4b921bb461f6 by nipkow:
moved from AFP/Gromov
The file was modified src/HOL/Finite_Set.thy (diff)
Changeset 67456:7895c159d7b1 by nipkow:
added lemma
The file was modified CONTRIBUTORS (diff)
The file was modified src/HOL/Library/Extended_Nonnegative_Real.thy (diff)