Skip to content
Success

Changes

Changes from Mercurial (hg http://isabelle.in.tum.de/repos/isabelle/ default)

Summary

  1. clarified files;
  2. tuned whitespace;
  3. clarified parsing vs. semantic errors;
  4. clarified signature;
  5. added document antiquotation @{tool}; formal check of isabelle tools via Isabelle/Scala;
  6. more robust isabelle_scala_files; clarified evaluation;
  7. avoid conflicting base names;
  8. clarified protocol: Doc.check at run-time via Scala function;
  9. more antiquotations (reverting 4df341249348);
  10. tuned;
  11. tuned signature --- more explicit types;
  12. more positions;
  13. support for Scala compile-time positions;
  14. clarified modules;
  15. more robust (amending a4d7da18ac5c);
  16. merged
  17. merged
  18. More removal of apply
Changeset 72767:f6bf65554764 by wenzelm:
clarified files;
The file was addedsrc/Tools/VSCode/src/textmate_grammar.scala
The file was modified src/Pure/System/isabelle_tool.scala
The file was modified src/Pure/build-jars
The file was modified src/Tools/VSCode/src/build_vscode.scala
The file was removedsrc/Tools/VSCode/src/grammar.scala
Changeset 72766:47ffeb3448f4 by wenzelm:
tuned whitespace;
The file was modified src/HOL/SPARK/SPARK_Setup.thy
Changeset 72765:f34f5c057c9e by wenzelm:
clarified parsing vs. semantic errors;
The file was modified src/Pure/Isar/keyword.scala
The file was modified src/Pure/PIDE/command.scala
The file was modified src/Pure/PIDE/resources.scala
The file was modified src/Pure/Thy/thy_header.ML
The file was modified src/Pure/Thy/thy_header.scala
Changeset 72764:722c0d02ffab by wenzelm:
clarified signature;
The file was modified src/Pure/Isar/keyword.scala
The file was modified src/Pure/PIDE/protocol.scala
The file was modified src/Pure/Thy/thy_header.scala
Changeset 72763:3cc73d00553c by wenzelm:
added document antiquotation @{tool};<br>formal check of isabelle tools via Isabelle/Scala;
The file was addedsrc/Pure/System/isabelle_tool.ML
The file was modified NEWS
The file was modified etc/symbols
The file was modified src/Doc/System/Base.thy
The file was modified src/Doc/antiquote_setup.ML
The file was modified src/Pure/Admin/build_csdp.scala
The file was modified src/Pure/Admin/build_cygwin.scala
The file was modified src/Pure/Admin/build_doc.scala
The file was modified src/Pure/Admin/build_e.scala
The file was modified src/Pure/Admin/build_fonts.scala
The file was modified src/Pure/Admin/build_jdk.scala
The file was modified src/Pure/Admin/build_polyml.scala
The file was modified src/Pure/Admin/build_spass.scala
The file was modified src/Pure/Admin/build_sqlite.scala
The file was modified src/Pure/Admin/build_status.scala
The file was modified src/Pure/Admin/build_verit.scala
The file was modified src/Pure/Admin/build_zipperposition.scala
The file was modified src/Pure/Admin/check_sources.scala
The file was modified src/Pure/Admin/components.scala
The file was modified src/Pure/General/mercurial.scala
The file was modified src/Pure/ML/ml_process.scala
The file was modified src/Pure/PIDE/markup.ML
The file was modified src/Pure/ROOT.ML
The file was modified src/Pure/System/isabelle_tool.scala
The file was modified src/Pure/System/options.scala
The file was modified src/Pure/System/scala.scala
The file was modified src/Pure/Thy/export.scala
The file was modified src/Pure/Thy/presentation.scala
The file was modified src/Pure/Thy/sessions.scala
The file was modified src/Pure/Tools/build.scala
The file was modified src/Pure/Tools/build_docker.scala
The file was modified src/Pure/Tools/doc.scala
The file was modified src/Pure/Tools/dump.scala
The file was modified src/Pure/Tools/mkroot.scala
The file was modified src/Pure/Tools/phabricator.scala
The file was modified src/Pure/Tools/profiling_report.scala
The file was modified src/Pure/Tools/scala_project.scala
The file was modified src/Pure/Tools/server.scala
The file was modified src/Pure/Tools/update.scala
The file was modified src/Pure/Tools/update_cartouches.scala
The file was modified src/Pure/Tools/update_comments.scala
The file was modified src/Pure/Tools/update_header.scala
The file was modified src/Pure/Tools/update_then.scala
The file was modified src/Pure/Tools/update_theorems.scala
The file was modified src/Tools/VSCode/src/build_vscode.scala
The file was modified src/Tools/VSCode/src/grammar.scala
The file was modified src/Tools/VSCode/src/language_server.scala
Changeset 72762:d9a54c4c9da9 by wenzelm:
more robust isabelle_scala_files;<br>clarified evaluation;
The file was modified src/Pure/Tools/scala_project.scala
Changeset 72761:4519eeefe3b5 by wenzelm:
avoid conflicting base names;
The file was addedsrc/Tools/VSCode/src/language_server.scala
The file was addedsrc/Tools/VSCode/src/lsp.scala
The file was addedsrc/Tools/VSCode/src/vscode_model.scala
The file was modified src/Pure/System/isabelle_tool.scala
The file was modified src/Pure/build-jars
The file was modified src/Tools/VSCode/src/channel.scala
The file was modified src/Tools/VSCode/src/dynamic_output.scala
The file was modified src/Tools/VSCode/src/preview_panel.scala
The file was modified src/Tools/VSCode/src/state_panel.scala
The file was modified src/Tools/VSCode/src/vscode_rendering.scala
The file was modified src/Tools/VSCode/src/vscode_resources.scala
The file was modified src/Tools/VSCode/src/vscode_spell_checker.scala
The file was removedsrc/Tools/VSCode/src/document_model.scala
The file was removedsrc/Tools/VSCode/src/protocol.scala
The file was removedsrc/Tools/VSCode/src/server.scala
Changeset 72760:042180540068 by wenzelm:
clarified protocol: Doc.check at run-time via Scala function;
The file was addedsrc/Pure/Tools/doc.ML
The file was modified src/Pure/PIDE/resources.ML
The file was modified src/Pure/PIDE/resources.scala
The file was modified src/Pure/ROOT.ML
The file was modified src/Pure/System/scala.scala
The file was modified src/Pure/Thy/sessions.scala
The file was modified src/Pure/Tools/doc.scala
Changeset 72759:bd5ee3148132 by wenzelm:
more antiquotations (reverting 4df341249348);
The file was modified src/Doc/System/Scala.thy
The file was modified src/Pure/System/scala.ML
Changeset 72758:9d0951e24e61 by wenzelm:
tuned;
The file was modified src/Pure/PIDE/resources.ML
Changeset 72757:38e05b7ded61 by wenzelm:
tuned signature --- more explicit types;
The file was modified src/Pure/PIDE/command.scala
The file was modified src/Pure/PIDE/command_span.scala
The file was modified src/Pure/PIDE/resources.scala
Changeset 72756:72ac27ea12b2 by wenzelm:
more positions;
The file was modified src/HOL/Tools/Nitpick/kodkod.scala
The file was modified src/Pure/PIDE/resources.ML
The file was modified src/Pure/PIDE/resources.scala
The file was modified src/Pure/System/scala.ML
The file was modified src/Pure/System/scala.scala
The file was modified src/Pure/Thy/bibtex.scala
Changeset 72755:8dffbe01a3e1 by wenzelm:
support for Scala compile-time positions;
The file was modified src/Pure/Tools/scala_project.scala
Changeset 72754:1456c5747416 by wenzelm:
clarified modules;
The file was modified src/HOL/SPARK/Tools/spark_commands.ML
The file was modified src/Pure/PIDE/command_span.ML
The file was modified src/Pure/PIDE/resources.ML
Changeset 72753:e8da2cfdfcff by wenzelm:
more robust (amending a4d7da18ac5c);
The file was modified src/Pure/Admin/build_log.scala
Changeset 72752:80ae03520fda by paulson:
merged
Changeset 72751:8765ca252772 by paulson:
merged
Changeset 72750:96d39c1dd64c by paulson _lp15@cam.ac.uk_:
More removal of apply
The file was modified src/HOL/Computational_Algebra/Polynomial.thy

Changes from Mercurial (hg https://foss.heptapod.net/isa-afp/afp-devel/ default)

Summary

  1. Update change history. Fix a typo.
  2. adjusting for the re-orientation of order_unique_lemma
Changeset 11450:98774839d1ee by "eugene w. stark _stark@cs.stonybrook.edu_":
Update change history.&nbsp; Fix a typo.
The file was modified metadata/metadata
The file was modified thys/Bicategory/document/root.tex
Changeset 11449:1c6c1d15536e by paulson _lp15@cam.ac.uk_:
adjusting for the re-orientation of order_unique_lemma
The file was modified thys/Polynomial_Factorization/Square_Free_Factorization.thy