Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. prefer formal comments;
  3. clarified NEWS;
  4. tuned whitespace;
  5. tuned;
  6. support for formal comments in ML in Isabelle/Scala;
  7. tuned;
  8. tuned message;
  9. allow formal comments in ML; ML_Compiler.eval: always suppress comments;
  10. clarified modules;
  11. tuned;
  12. more uniform output: formal comments within {* ... *};
  13. tuned;
  14. clarified output: avoid extra space;
  15. output token content with formal comments and antiquotations;
  16. tuned;
  17. clarified signature;
  18. clarified modules;
  19. inner syntax comments may be written as "\<comment> \<open>text\<close>";
  20. spelling
Changeset 67370:86aa6e2abee1 by wenzelm:
merged
Changeset 67369:7360fe6bb423 by wenzelm:
prefer formal comments;
The file was modified src/Doc/Isar_Ref/Synopsis.thy (diff)
The file was modified src/HOL/Computational_Algebra/Polynomial.thy (diff)
The file was modified src/HOL/Data_Structures/AA_Set.thy (diff)
The file was modified src/HOL/HOLCF/IOA/ABP/Spec.thy (diff)
The file was modified src/HOL/Nitpick_Examples/Hotel_Nits.thy (diff)
The file was modified src/HOL/Quickcheck_Exhaustive.thy (diff)
Changeset 67368:e9bee1ddfe19 by wenzelm:
clarified NEWS;
The file was modified NEWS (diff)
Changeset 67367:2b11c071d016 by wenzelm:
tuned whitespace;
The file was modified src/Pure/Syntax/lexicon.ML (diff)
Changeset 67366:e2575ccc0f5c by wenzelm:
tuned;
The file was modified src/Pure/ML/ml_lex.scala (diff)
Changeset 67365:fb539f83683a by wenzelm:
support for formal comments in ML in Isabelle/Scala;
The file was modified src/Pure/General/scan.scala (diff)
The file was modified src/Pure/ML/ml_lex.scala (diff)
The file was modified src/Tools/jEdit/src/jedit_rendering.scala (diff)
Changeset 67364:f74672cf83c6 by wenzelm:
tuned;
The file was modified src/Pure/General/scan.scala (diff)
The file was modified src/Pure/ML/ml_lex.scala (diff)
Changeset 67363:408a137e2793 by wenzelm:
tuned message;
The file was modified src/Pure/ML/ml_lex.ML (diff)
Changeset 67362:221612c942de by wenzelm:
allow formal comments in ML;<br>ML_Compiler.eval: always suppress comments;
The file was modified src/Pure/ML/ml_compiler.ML (diff)
The file was modified src/Pure/ML/ml_lex.ML (diff)
Changeset 67361:f834d6f21c55 by wenzelm:
clarified modules;
The file was modified src/Pure/General/symbol_pos.ML (diff)
The file was modified src/Pure/Syntax/lexicon.ML (diff)
Changeset 67360:fbc31dea36fa by wenzelm:
tuned;
The file was modified src/Pure/Thy/thy_output.ML (diff)
Changeset 67359:fed0e220be45 by wenzelm:
more uniform output: formal comments within {* ... *};
The file was modified src/Pure/Thy/thy_output.ML (diff)
Changeset 67358:dfee70a24f0c by wenzelm:
tuned;
The file was modified src/Pure/Thy/latex.ML (diff)
The file was modified src/Pure/Thy/thy_output.ML (diff)
Changeset 67357:d7c6054b2ab1 by wenzelm:
clarified output: avoid extra space;
The file was modified src/Pure/Thy/thy_output.ML (diff)
Changeset 67356:ba226b87c69e by wenzelm:
output token content with formal comments and antiquotations;
The file was modified NEWS (diff)
The file was modified src/Pure/Thy/document_antiquotations.ML (diff)
The file was modified src/Pure/Thy/thy_output.ML (diff)
Changeset 67355:4c8280aaf6ad by wenzelm:
tuned;
The file was modified src/Pure/Thy/latex.ML (diff)
Changeset 67354:f243af7b5be3 by wenzelm:
clarified signature;
The file was modified src/Pure/Thy/document_antiquotations.ML (diff)
The file was modified src/Pure/Thy/thy_output.ML (diff)
Changeset 67353:95f5f4bec7af by wenzelm:
clarified modules;
The file was modified src/Pure/Thy/document_antiquotations.ML (diff)
The file was modified src/Pure/Thy/latex.ML (diff)
The file was modified src/Pure/Thy/thy_output.ML (diff)
Changeset 67352:5f7f339f3d7e by wenzelm:
inner syntax comments may be written as &quot;\&lt;comment&gt; \&lt;open&gt;text\&lt;close&gt;&quot;;
The file was modified NEWS (diff)
The file was modified src/Doc/Isar_Ref/Inner_Syntax.thy (diff)
The file was modified src/Pure/Syntax/lexicon.ML (diff)
Changeset 67351:63d7aca15f6b by haftmann:
spelling
The file was modified src/Doc/System/Presentation.thy (diff)