more standard session build process, including browser_info;
clarified final setup of global ML environment;
--- a/lib/html/library_index_content.template Sun Apr 10 21:30:48 2016 +0200
+++ b/lib/html/library_index_content.template Sun Apr 10 21:46:12 2016 +0200
@@ -46,6 +46,8 @@
<li><a href="Cube/index.html">Cube (The Lambda Cube)</a></li>
+ <li><a href="Pure/Pure/index.html">The Pure logical framework</a></li>
+
<li><a href="Doc/index.html">Sources of Documentation</a></li>
</ul>
</li>
--- a/src/Pure/ML/ml_compiler2.ML Sun Apr 10 21:30:48 2016 +0200
+++ b/src/Pure/ML/ml_compiler2.ML Sun Apr 10 21:46:12 2016 +0200
@@ -10,3 +10,5 @@
ML_Context.eval_file flags (Path.explode file)
handle ERROR msg => (writeln msg; error "ML error")
end);
+
+val use = ML_file;
--- a/src/Pure/ML/ml_pervasive1.ML Sun Apr 10 21:30:48 2016 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,15 +0,0 @@
-(* Title: Pure/ML/ml_pervasive1.ML
- Author: Makarius
-
-Pervasive ML environment: final setup.
-*)
-
-List.app ML_Name_Space.forget_structure ML_Name_Space.hidden_structures;
-
-structure PolyML = struct structure IntInf = PolyML.IntInf end;
-
-Proofterm.proofs := 0;
-
-Context.put_generic_context NONE;
-
-val use = ML_file;
--- a/src/Pure/ML_Bootstrap.thy Sun Apr 10 21:30:48 2016 +0200
+++ b/src/Pure/ML_Bootstrap.thy Sun Apr 10 21:46:12 2016 +0200
@@ -8,13 +8,33 @@
imports Pure
begin
+subsection \<open>Standard ML environment for virtual bootstrap\<close>
+
setup \<open>Context.theory_map ML_Env.init_bootstrap\<close>
SML_import \<open>
-structure Output_Primitives = Output_Primitives_Virtual;
-structure Thread_Data = Thread_Data_Virtual;
+ structure Output_Primitives = Output_Primitives_Virtual;
+ structure Thread_Data = Thread_Data_Virtual;
\<close>
+
+subsection \<open>Final setup of global ML environment\<close>
+
+ML \<open>Proofterm.proofs := 0\<close>
+
+ML \<open>
+ Context.setmp_generic_context NONE
+ ML \<open>
+ List.app ML_Name_Space.forget_structure ML_Name_Space.hidden_structures;
+ structure PolyML = struct structure IntInf = PolyML.IntInf end;
+ \<close>
+\<close>
+
+ML \<open>@{assert} (not (can ML \<open>open RunCall\<close>))\<close>
+
+
+subsection \<open>Switch to bootstrap environment\<close>
+
setup \<open>Config.put_global ML_Env.SML_environment true\<close>
end
--- a/src/Pure/PIDE/session.ML Sun Apr 10 21:30:48 2016 +0200
+++ b/src/Pure/PIDE/session.ML Sun Apr 10 21:46:12 2016 +0200
@@ -22,7 +22,7 @@
(** persistent session information **)
-val session = Synchronized.var "Session.session" ({chapter = "Pure", name = "Pure"}, false);
+val session = Synchronized.var "Session.session" ({chapter = "", name = ""}, true);
fun get_name () = #name (#1 (Synchronized.value session));
--- a/src/Pure/Pure.thy Sun Apr 10 21:30:48 2016 +0200
+++ b/src/Pure/Pure.thy Sun Apr 10 21:46:12 2016 +0200
@@ -1,7 +1,7 @@
(* Title: Pure/Pure.thy
Author: Makarius
-Final stage of bootstrapping Pure, based on implicit background theory.
+The Pure theory, with definitions of Isar commands and some lemmas.
*)
theory Pure
@@ -1282,7 +1282,7 @@
in end\<close>
-section \<open>Further content for the Pure theory\<close>
+section \<open>Auxiliary lemmas\<close>
subsection \<open>Meta-level connectives in assumptions\<close>
--- a/src/Pure/ROOT Sun Apr 10 21:30:48 2016 +0200
+++ b/src/Pure/ROOT Sun Apr 10 21:46:12 2016 +0200
@@ -1,6 +1,9 @@
chapter Pure
session Pure =
+ description {*
+ The Pure logical framework
+ *}
global_theories
Pure
theories
--- a/src/Pure/ROOT1.ML Sun Apr 10 21:30:48 2016 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,6 +0,0 @@
-(*** Isabelle/Pure bootstrap: final setup ***)
-
-use_thy "Pure";
-use_thy "ML_Bootstrap";
-
-ML_file "ML/ml_pervasive1.ML";
--- a/src/Pure/Thy/sessions.scala Sun Apr 10 21:30:48 2016 +0200
+++ b/src/Pure/Thy/sessions.scala Sun Apr 10 21:46:12 2016 +0200
@@ -20,7 +20,7 @@
def pure_name(name: String): Boolean = name == "Pure"
- val pure_roots: List[String] = List("ROOT0.ML", "ROOT.ML", "ROOT1.ML")
+ val pure_roots: List[String] = List("ROOT0.ML", "ROOT.ML")
def pure_files(resources: Resources, syntax: Outer_Syntax, dir: Path): List[Path] =
{
--- a/src/Pure/Tools/build.scala Sun Apr 10 21:30:48 2016 +0200
+++ b/src/Pure/Tools/build.scala Sun Apr 10 21:46:12 2016 +0200
@@ -258,36 +258,33 @@
private val future_result: Future[Process_Result] =
Future.thread("build") {
+ val args_file = Isabelle_System.tmp_file("build")
+ File.write(args_file, YXML.string_of_body(
+ {
+ val theories = info.theories.map(x => (x._2, x._3))
+ import XML.Encode._
+ pair(list(pair(string, int)), pair(list(properties), pair(bool, pair(bool,
+ pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string,
+ pair(string, pair(string, pair(string,
+ list(pair(Options.encode, list(Path.encode)))))))))))))(
+ (Symbol.codes, (command_timings, (do_output, (verbose,
+ (store.browser_info, (info.document_files, (File.standard_path(graph_file),
+ (parent, (info.chapter, (name,
+ theories)))))))))))
+ }))
+
+ val eval =
+ "Command_Line.tool0 (fn () => (" +
+ "Build.build " + ML_Syntax.print_string0(File.standard_path(args_file)) +
+ (if (do_output) "; ML_Heap.share_common_data (); " + output_save_state
+ else "") + "));"
val process =
if (Sessions.pure_name(name)) {
- val roots = Sessions.pure_roots.flatMap(root => List("--use", root))
- val eval =
- "Command_Line.tool0 (fn () => (Session.finish (); Options.reset_default ();" +
- " Session.shutdown (); ML_Heap.share_common_data (); " + output_save_state + "));"
- ML_Process(info.options,
- raw_ml_system = true, args = roots ::: List("--eval", eval),
- cwd = info.dir.file, env = env, tree = Some(tree), store = store)
+ ML_Process(info.options, raw_ml_system = true, cwd = info.dir.file,
+ args = List("--use", "ROOT0.ML", "--use", "ROOT.ML", "--eval", eval),
+ env = env, tree = Some(tree), store = store, cleanup = () => args_file.delete)
}
else {
- val args_file = Isabelle_System.tmp_file("build")
- File.write(args_file, YXML.string_of_body(
- {
- val theories = info.theories.map(x => (x._2, x._3))
- import XML.Encode._
- pair(list(pair(string, int)), pair(list(properties), pair(bool, pair(bool,
- pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string,
- pair(string, pair(string, pair(string,
- list(pair(Options.encode, list(Path.encode)))))))))))))(
- (Symbol.codes, (command_timings, (do_output, (verbose,
- (store.browser_info, (info.document_files, (File.standard_path(graph_file),
- (parent, (info.chapter, (name,
- theories)))))))))))
- }))
- val eval =
- "Command_Line.tool0 (fn () => (" +
- "Build.build " + ML_Syntax.print_string0(File.standard_path(args_file)) +
- (if (do_output) "; ML_Heap.share_common_data (); " + output_save_state
- else "") + "));"
ML_Process(info.options, parent, List("--eval", eval), cwd = info.dir.file,
env = env, tree = Some(tree), store = store, cleanup = () => args_file.delete)
}
@@ -320,7 +317,7 @@
{
val result = future_result.join
- if (result.ok && !Sessions.pure_name(name))
+ if (result.ok)
Present.finish(progress, store.browser_info, graph_file, info, name)
graph_file.delete
@@ -677,7 +674,7 @@
val browser_chapters =
(for {
(name, result) <- results0.iterator
- if result.ok && !Sessions.pure_name(name)
+ if result.ok
info = full_tree(name)
if info.options.bool("browser_info")
} yield (info.chapter, (name, info.description))).toList.groupBy(_._1).