Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. clarified modules: avoid duplication;
  3. tuned output;
  4. support for generic File_Format.parse_data, with persistent result in document model;
  5. omit warning: somewhat pointless and out-of-context;
  6. clarified signature: avoid case class with mutable state;
  7. tuned;
  8. clarified signature: more explicit types;
  9. merged
  10. tidied some messy old proofs
Changeset 76795:04af11e6557a by wenzelm:
merged
Changeset 76794:941d4f527091 by wenzelm:
clarified modules: avoid duplication;
The file was modified src/Pure/PIDE/editor.scala (diff)
The file was modified src/Tools/VSCode/src/language_server.scala (diff)
The file was modified src/Tools/VSCode/src/vscode_rendering.scala (diff)
The file was modified src/Tools/jEdit/src/completion_popup.scala (diff)
The file was modified src/Tools/jEdit/src/document_model.scala (diff)
The file was modified src/Tools/jEdit/src/jedit_editor.scala (diff)
The file was modified src/Tools/jEdit/src/jedit_rendering.scala (diff)
Changeset 76793:fa70b536ec50 by wenzelm:
tuned output;
The file was modified src/Pure/Thy/bibtex.scala (diff)
The file was modified src/Pure/Thy/file_format.scala (diff)
Changeset 76792:23f433294173 by wenzelm:
support for generic File_Format.parse_data, with persistent result in document model;
The file was modified src/Pure/PIDE/document.scala (diff)
The file was modified src/Pure/Thy/bibtex.scala (diff)
The file was modified src/Pure/Thy/file_format.scala (diff)
The file was modified src/Tools/VSCode/src/vscode_model.scala (diff)
The file was modified src/Tools/jEdit/src/document_model.scala (diff)
Changeset 76791:c36d666ee5ee by wenzelm:
omit warning: somewhat pointless and out-of-context;
The file was modified src/Tools/jEdit/src/document_model.scala (diff)
Changeset 76790:7a0438979e85 by wenzelm:
clarified signature: avoid case class with mutable state;
The file was modified src/Tools/jEdit/src/document_model.scala (diff)
Changeset 76789:27a8e9e8761e by wenzelm:
tuned;
The file was modified src/Pure/GUI/gui.scala (diff)
The file was modified src/Pure/Thy/sessions.scala (diff)
The file was modified src/Tools/jEdit/src/document_model.scala (diff)
Changeset 76788:ce44e714d573 by wenzelm:
clarified signature: more explicit types;
The file was modified src/Pure/PIDE/session.scala (diff)
The file was modified src/Pure/library.scala (diff)
Changeset 76787:7fd705b107f2 by paulson:
merged
Changeset 76786:50672d2d78db by paulson _lp15@cam.ac.uk_:
tidied some messy old proofs
The file was modified src/HOL/Analysis/Brouwer_Fixpoint.thy (diff)
The file was modified src/HOL/Analysis/Lebesgue_Measure.thy (diff)
The file was modified src/HOL/Library/BigO.thy (diff)