Skip to content
[Jenkins]Jenkins
log in
Failed

Changes

Summary

  1. merged
  2. proper file extension;
  3. clarified files;
  4. back to static conditional compilation -- simplified bootstrap;
  5. clarified modules -- simplified bootstrap;
  6. avoid malformed Isabelle symbols during bootstrap;
  7. clarified modules -- simplified bootstrap;
  8. clarified bootstrap environment;
  9. actually observe ML_system_unsafe, concerning the environment that is stored in theory ML_Root;
  10. support bootstrap from fresh SML environment, with syntax of Isabelle/ML or SML;
  11. tuned;
  12. proper syntax;
  13. prefer antiquotations;
  14. proper use_thy;
  15. support for ML project ROOT file, with imitation of ML "use" commands;
  16. tuned;
  17. read Pure file dependencies directly from ROOT.ML;
  18. tuned output;
  19. tuned;
Changeset 62882:3c4161728aa8 by wenzelm:
merged
Changeset 62881:20b0cb2f0b87 by wenzelm:
proper file extension;
The file was modified src/Pure/ML/ml_root.scala (diff)
The file was modified src/Pure/ML_Root.thy (diff)
Changeset 62880:76e7d9169b54 by wenzelm:
clarified files;
The file was addedsrc/Pure/ML_Root.thy
The file was modified src/Pure/ROOT (diff)
The file was modified src/Pure/ROOT.ML (diff)
The file was removedsrc/Pure/ML/ML_Root.thy
Changeset 62879:4764473c9b8d by wenzelm:
back to static conditional compilation -- simplified bootstrap;
The file was addedsrc/Pure/System/windows/bash.ML
The file was modified lib/scripts/isabelle-platform (diff)
The file was modified src/Pure/ROOT.ML (diff)
The file was modified src/Pure/System/bash.ML (diff)
Changeset 62878:1cec457e0a03 by wenzelm:
clarified modules -- simplified bootstrap;
The file was addedsrc/Pure/ML/ml_print_depth.ML
The file was addedsrc/Pure/ML/ml_print_depth0.ML
The file was modified src/Pure/Isar/attrib.ML (diff)
The file was modified src/Pure/Isar/runtime.ML (diff)
The file was modified src/Pure/ML/ml_compiler.ML (diff)
The file was modified src/Pure/ML/ml_context.ML (diff)
The file was modified src/Pure/ML/ml_options.ML (diff)
The file was modified src/Pure/ML/ml_pretty.ML (diff)
The file was modified src/Pure/ROOT.ML (diff)
The file was modified src/Pure/System/isabelle_process.ML (diff)
The file was modified src/Pure/System/options.ML (diff)
The file was modified src/Pure/Tools/debugger.ML (diff)
Changeset 62877:741560a5283b by wenzelm:
avoid malformed Isabelle symbols during bootstrap;
The file was modified src/Pure/General/symbol.ML (diff)
The file was modified src/Pure/ML/ml_compiler0.ML (diff)
Changeset 62876:507c90523113 by wenzelm:
clarified modules -- simplified bootstrap;
The file was modified src/Doc/Implementation/ML.thy (diff)
The file was modified src/HOL/Tools/Quickcheck/narrowing_generators.ML (diff)
The file was modified src/Pure/Isar/outer_syntax.ML (diff)
The file was modified src/Pure/ML/ml_context.ML (diff)
The file was modified src/Pure/ML/ml_env.ML (diff)
The file was modified src/Pure/ML/ml_thms.ML (diff)
The file was modified src/Pure/Thy/thy_info.ML (diff)
The file was modified src/Pure/Tools/debugger.ML (diff)
The file was modified src/Pure/conjunction.ML (diff)
The file was modified src/Pure/context.ML (diff)
The file was modified src/Pure/drule.ML (diff)
The file was modified src/Pure/pure_syn.ML (diff)
The file was modified src/Pure/raw_simplifier.ML (diff)
The file was modified src/Tools/Code/code_runtime.ML (diff)
The file was modified src/Tools/Spec_Check/gen_construction.ML (diff)
The file was modified src/Tools/Spec_Check/spec_check.ML (diff)
Changeset 62875:5a0c06491974 by wenzelm:
clarified bootstrap environment;
The file was modified NEWS (diff)
The file was modified etc/options (diff)
The file was modified src/Pure/ML/ml_env.ML (diff)
The file was modified src/Pure/ML/ml_name_space.ML (diff)
The file was modified src/Pure/ML/ml_pervasive_final.ML (diff)
The file was modified src/Pure/System/options.ML (diff)
Changeset 62874:b0194643e64c by wenzelm:
actually observe ML_system_unsafe, concerning the environment that is stored in theory ML_Root;
The file was modified src/Pure/ROOT.ML (diff)
Changeset 62873:2f9c8a18f832 by wenzelm:
support bootstrap from fresh SML environment, with syntax of Isabelle/ML or SML;
The file was modified src/Pure/Isar/isar_syn.ML (diff)
The file was modified src/Pure/ML/ML_Root.thy (diff)
The file was modified src/Pure/ML/ml_compiler.ML (diff)
The file was modified src/Pure/ML/ml_context.ML (diff)
The file was modified src/Pure/ML/ml_env.ML (diff)
The file was modified src/Pure/ML/ml_file.ML (diff)
The file was modified src/Pure/Pure.thy (diff)
The file was modified src/Pure/Tools/debugger.ML (diff)
Changeset 62872:bf1b4d3440a3 by wenzelm:
tuned;
The file was modified src/Pure/ML/ml_name_space.ML (diff)
The file was modified src/Pure/ML/ml_pervasive_final.ML (diff)
Changeset 62871:4a6cbe1239fe by wenzelm:
proper syntax;
The file was modified src/Pure/ML/ML_Root.thy (diff)
Changeset 62870:cf724647f75b by wenzelm:
prefer antiquotations;
The file was modified src/HOL/Matrix_LP/Compute_Oracle/compute.ML (diff)
The file was modified src/Provers/splitter.ML (diff)
The file was modified src/Pure/ML/ml_pervasive_final.ML (diff)
The file was modified src/Pure/ROOT.ML (diff)
Changeset 62869:64a5cf42be1e by wenzelm:
proper use_thy;
The file was modified src/Pure/ROOT.ML (diff)
Changeset 62868:61a691db1c4d by wenzelm:
support for ML project ROOT file, with imitation of ML "use" commands;
The file was addedsrc/Pure/ML/ML_Root.thy
The file was modified src/Pure/ML/ml_file.ML (diff)
The file was modified src/Pure/ROOT (diff)
Changeset 62867:cce0570d1bfa by wenzelm:
tuned;
The file was modified src/Pure/Pure.thy (diff)
Changeset 62866:d20262cd20e8 by wenzelm:
read Pure file dependencies directly from ROOT.ML;
The file was addedsrc/Pure/ML/ml_root.scala
The file was modified src/Pure/ROOT (diff)
The file was modified src/Pure/Tools/build.scala (diff)
The file was modified src/Pure/build-jars (diff)
Changeset 62865:cf03cb9578d4 by wenzelm:
tuned output;
The file was modified src/Pure/Thy/thy_info.scala (diff)
Changeset 62864:2d5959cf3c1a by wenzelm:
tuned;
The file was modified src/Pure/Thy/sessions.scala (diff)