# HG changeset patch # User wenzelm # Date 1460317572 -7200 # Node ID 3ee643c5ed00c1640e04f880266029d06a585baf # Parent 659a8737501d6848bf68ee1506541f4144d67d6c more standard session build process, including browser_info; clarified final setup of global ML environment; diff -r 659a8737501d -r 3ee643c5ed00 lib/html/library_index_content.template --- 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 @@
  • Cube (The Lambda Cube)
    • +
  • The Pure logical framework
    • +
  • Sources of Documentation
    • diff -r 659a8737501d -r 3ee643c5ed00 src/Pure/ML/ml_compiler2.ML --- 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; diff -r 659a8737501d -r 3ee643c5ed00 src/Pure/ML/ml_pervasive1.ML --- 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; diff -r 659a8737501d -r 3ee643c5ed00 src/Pure/ML_Bootstrap.thy --- 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 \Standard ML environment for virtual bootstrap\ + setup \Context.theory_map ML_Env.init_bootstrap\ SML_import \ -structure Output_Primitives = Output_Primitives_Virtual; -structure Thread_Data = Thread_Data_Virtual; + structure Output_Primitives = Output_Primitives_Virtual; + structure Thread_Data = Thread_Data_Virtual; \ + +subsection \Final setup of global ML environment\ + +ML \Proofterm.proofs := 0\ + +ML \ + Context.setmp_generic_context NONE + ML \ + List.app ML_Name_Space.forget_structure ML_Name_Space.hidden_structures; + structure PolyML = struct structure IntInf = PolyML.IntInf end; + \ +\ + +ML \@{assert} (not (can ML \open RunCall\))\ + + +subsection \Switch to bootstrap environment\ + setup \Config.put_global ML_Env.SML_environment true\ end diff -r 659a8737501d -r 3ee643c5ed00 src/Pure/PIDE/session.ML --- 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)); diff -r 659a8737501d -r 3ee643c5ed00 src/Pure/Pure.thy --- 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\ -section \Further content for the Pure theory\ +section \Auxiliary lemmas\ subsection \Meta-level connectives in assumptions\ diff -r 659a8737501d -r 3ee643c5ed00 src/Pure/ROOT --- 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 diff -r 659a8737501d -r 3ee643c5ed00 src/Pure/ROOT1.ML --- 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"; diff -r 659a8737501d -r 3ee643c5ed00 src/Pure/Thy/sessions.scala --- 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] = { diff -r 659a8737501d -r 3ee643c5ed00 src/Pure/Tools/build.scala --- 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).