Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. more flexible syntax for theory load commands via Isabelle/Scala;
  3. clarified theory keywords: loaded_files are determined statically in Scala, but ML needs to do it semantically; propagate blob src_path from Scala to ML; clarified signature;
  4. proper structural equality;
  5. more explicit types;
  6. unused (see 7634d33c1a79);
  7. clarified signature;
  8. clarified modules;
  9. clarified file names;
  10. tuned signature;
  11. refined syntax for bundle mixins for locale and class specifications
Changeset 72749:38d001186621 by wenzelm:
merged
Changeset 72748:04d5f6d769a7 by wenzelm:
more flexible syntax for theory load commands via Isabelle/Scala;
The file was addedsrc/HOL/SPARK/Tools/spark.scala
The file was addedsrc/HOL/SPARK/etc/settings
The file was modified NEWS (diff)
The file was modified src/HOL/SPARK/SPARK_Setup.thy (diff)
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/Pure/PIDE/command.scala (diff)
The file was modified src/Pure/PIDE/command_span.scala (diff)
The file was modified src/Pure/Thy/thy_header.scala (diff)
The file was modified src/Pure/Tools/scala_project.scala (diff)
The file was modified src/Pure/build-jars (diff)
Changeset 72747:5f9d66155081 by wenzelm:
clarified theory keywords: loaded_files are determined statically in Scala, but ML needs to do it semantically;<br>propagate blob src_path from Scala to ML;<br>clarified signature;
The file was modified src/HOL/SMT_Examples/boogie.ML (diff)
The file was modified src/HOL/SPARK/Tools/spark_commands.ML (diff)
The file was modified src/Pure/Isar/keyword.ML (diff)
The file was modified src/Pure/ML/ml_file.ML (diff)
The file was modified src/Pure/PIDE/command.ML (diff)
The file was modified src/Pure/PIDE/command.scala (diff)
The file was modified src/Pure/PIDE/document.ML (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/Pure.thy (diff)
The file was modified src/Pure/Thy/thy_header.ML (diff)
The file was modified src/Pure/Thy/thy_header.scala (diff)
Changeset 72746:049a71febf05 by wenzelm:
proper structural equality;
The file was modified src/Pure/General/path.scala (diff)
Changeset 72745:5a6f7212fc4d by wenzelm:
more explicit types;
The file was modified src/Pure/PIDE/command.scala (diff)
The file was modified src/Pure/PIDE/protocol.scala (diff)
Changeset 72744:0017eb17ac1c by wenzelm:
unused (see 7634d33c1a79);
The file was modified src/Pure/General/symbol.scala (diff)
The file was modified src/Pure/Isar/token.scala (diff)
The file was modified src/Pure/PIDE/command.scala (diff)
The file was modified src/Pure/PIDE/command_span.scala (diff)
Changeset 72743:bc82fc605424 by wenzelm:
clarified signature;
The file was modified src/Pure/PIDE/command_span.scala (diff)
Changeset 72742:bda424c5819f by wenzelm:
clarified modules;
The file was modified src/Pure/PIDE/command.scala (diff)
The file was modified src/Pure/PIDE/command_span.scala (diff)
The file was modified src/Pure/PIDE/resources.scala (diff)
Changeset 72741:b808eddc83cf by wenzelm:
clarified file names;
The file was modified src/HOL/SMT_Examples/Boogie.thy (diff)
Changeset 72740:082200ee003d by wenzelm:
tuned signature;
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/Pure/PIDE/resources.scala (diff)
Changeset 72739:e7c2848b78e8 by haftmann:
refined syntax for bundle mixins for locale and class specifications
The file was modified NEWS (diff)
The file was modified src/Doc/Isar_Ref/Spec.thy (diff)
The file was modified src/HOL/Product_Type.thy (diff)
The file was modified src/HOL/ex/Specifications_with_bundle_mixins.thy (diff)
The file was modified src/Pure/Isar/parse_spec.ML (diff)
The file was modified src/Pure/Pure.thy (diff)