Skip to content
Success

Changes

Summary

  1. merged
  2. misc tuning and modernization;
  3. merged
  4. misc tuning and modernization;
  5. auto indentation of quasi commands;
  6. tuned;
  7. clarified indentation (amending 37a3fc20154d);
  8. tuned;
  9. tuned;
  10. tuned;
  11. clarified indentation of proof commands, notably for "notepad begin", which lacks a head goal;
  12. clarified indentation: 'begin' is treated like a separate command without indent;
  13. tuned;
  14. obsolete;
  15. semantic indentation for unstructured proof scripts;
  16. misc tuning and modernization;
Changeset 63488:a7c5074a0251 by wenzelm:
merged
Changeset 63487:6e29fb72e659 by wenzelm:
misc tuning and modernization;
The file was modified src/HOL/Library/Stirling.thy (diff)
Changeset 63486:a4668ec480ad by wenzelm:
merged
Changeset 63485:ea8dfb0ed10e by wenzelm:
misc tuning and modernization;
The file was modified src/HOL/Library/BigO.thy (diff)
The file was modified src/HOL/Library/Convex.thy (diff)
The file was modified src/HOL/Library/Set_Algebras.thy (diff)
Changeset 63484:2033a3960c36 by wenzelm:
auto indentation of quasi commands;
The file was modified src/Tools/jEdit/src/isabelle.scala (diff)
Changeset 63483:2c9444125485 by wenzelm:
tuned;
The file was modified src/Tools/jEdit/src/text_structure.scala (diff)
Changeset 63482:cf2d332acb7c by wenzelm:
clarified indentation (amending 37a3fc20154d);
The file was modified src/Tools/jEdit/src/text_structure.scala (diff)
Changeset 63481:cbc71faf7673 by wenzelm:
tuned;
The file was modified src/Tools/jEdit/src/text_structure.scala (diff)
Changeset 63480:05908c773ca7 by wenzelm:
tuned;
The file was modified src/Tools/jEdit/src/text_structure.scala (diff)
Changeset 63479:464ef556bd21 by wenzelm:
tuned;
The file was modified src/Pure/Isar/keyword.scala (diff)
The file was modified src/Pure/Isar/outer_syntax.scala (diff)
The file was modified src/Tools/jEdit/src/text_structure.scala (diff)
Changeset 63478:37a3fc20154d by wenzelm:
clarified indentation of proof commands, notably for "notepad begin", which lacks a head goal;
The file was modified src/Tools/jEdit/src/text_structure.scala (diff)
Changeset 63477:f5c81436b930 by wenzelm:
clarified indentation: 'begin' is treated like a separate command without indent;
The file was modified src/Pure/Isar/token.scala (diff)
The file was modified src/Tools/jEdit/src/isabelle.scala (diff)
The file was modified src/Tools/jEdit/src/text_structure.scala (diff)
Changeset 63476:ff1d86b07751 by wenzelm:
tuned;
The file was modified src/HOL/Library/AList.thy (diff)
The file was modified src/HOL/Library/AList_Mapping.thy (diff)
The file was modified src/HOL/Library/Mapping.thy (diff)
Changeset 63475:31016a88197b by wenzelm:
obsolete;
The file was modified src/Pure/Isar/proof.ML (diff)
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/markup.scala (diff)
Changeset 63474:f66e3c3b0fb1 by wenzelm:
semantic indentation for unstructured proof scripts;
The file was modified NEWS (diff)
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/markup.scala (diff)
The file was modified src/Tools/jEdit/etc/options (diff)
The file was modified src/Tools/jEdit/src/rendering.scala (diff)
The file was modified src/Tools/jEdit/src/text_structure.scala (diff)
Changeset 63473:151bb79536a7 by wenzelm:
misc tuning and modernization;
The file was modified src/HOL/Library/BigO.thy (diff)
The file was modified src/HOL/Library/Set_Algebras.thy (diff)