# HG changeset patch # User wenzelm # Date 1585428871 -3600 # Node ID 74c874b5aed0165c9be0a23162fda889363b014b # Parent beef2e221c2603a666552d218521e966f2a6307a# Parent e6dead7d53348296d0d5c43048a5e67e44f8462d merged diff -r beef2e221c26 -r 74c874b5aed0 src/Pure/PIDE/session.ML --- a/src/Pure/PIDE/session.ML Sat Mar 28 17:27:08 2020 +0000 +++ b/src/Pure/PIDE/session.ML Sat Mar 28 21:54:31 2020 +0100 @@ -9,7 +9,7 @@ val get_name: unit -> string val welcome: unit -> string val get_keywords: unit -> Keyword.keywords - val init: HTML.symbols -> bool -> bool -> Path.T -> string -> string -> (string * string) list -> + val init: HTML.symbols -> bool -> Path.T -> string -> string -> (string * string) list -> (Path.T * Path.T) list -> Path.T -> string -> string * string -> bool -> unit val shutdown: unit -> unit val finish: unit -> unit @@ -48,13 +48,13 @@ (* init *) -fun init symbols build info info_path doc doc_output doc_variants doc_files graph_file +fun init symbols info info_path doc doc_output doc_variants doc_files graph_file parent (chapter, name) verbose = (Synchronized.change session (fn ({name = parent_name, ...}, parent_finished) => if parent_name <> parent orelse not parent_finished then error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name) else ({chapter = chapter, name = name}, false)); - Present.init symbols build info info_path (if doc = "false" then "" else doc) + Present.init symbols info info_path (if doc = "false" then "" else doc) doc_output doc_variants doc_files graph_file (chapter, name) verbose); diff -r beef2e221c26 -r 74c874b5aed0 src/Pure/System/command_line.scala --- a/src/Pure/System/command_line.scala Sat Mar 28 17:27:08 2020 +0000 +++ b/src/Pure/System/command_line.scala Sat Mar 28 21:54:31 2020 +0100 @@ -36,5 +36,7 @@ } def tool0(body: => Unit): Nothing = tool { body; 0 } + + def ML_tool0(body: List[String]): String = + "Command_Line.tool0 (fn () => (" + body.mkString("; ") + "));" } - diff -r beef2e221c26 -r 74c874b5aed0 src/Pure/Thy/present.ML --- a/src/Pure/Thy/present.ML Sat Mar 28 17:27:08 2020 +0000 +++ b/src/Pure/Thy/present.ML Sat Mar 28 21:54:31 2020 +0100 @@ -10,7 +10,7 @@ val theory_qualifier: theory -> string val document_option: Options.T -> {enabled: bool, disabled: bool} val document_variants: Options.T -> (string * string) list - val init: HTML.symbols -> bool -> bool -> Path.T -> string -> string -> (string * string) list -> + val init: HTML.symbols -> bool -> Path.T -> string -> string -> (string * string) list -> (Path.T * Path.T) list -> Path.T -> string * string -> bool -> unit val finish: unit -> unit val theory_output: theory -> string list -> unit @@ -165,28 +165,25 @@ (* init session *) -fun init symbols build info info_path doc document_output doc_variants doc_files graph_file +fun init symbols info info_path doc document_output doc_variants doc_files graph_file (chapter, name) verbose = - if not build andalso not info andalso doc = "" then - (Synchronized.change browser_info (K empty_browser_info); session_info := NONE) - else - let - val doc_output = - if document_output = "" then NONE else SOME (Path.explode document_output); + let + val doc_output = + if document_output = "" then NONE else SOME (Path.explode document_output); + + val documents = if doc = "" orelse null doc_files then [] else doc_variants; + val readme = if File.exists readme_html_path then SOME readme_html_path else NONE; - val documents = if doc = "" orelse null doc_files then [] else doc_variants; - val readme = if File.exists readme_html_path then SOME readme_html_path else NONE; - - val docs = - (case readme of NONE => [] | SOME p => [(Url.File p, "README")]) @ - map (fn (name, _) => (Url.File (Path.ext doc (Path.basic name)), name)) documents; - in - session_info := - SOME (make_session_info (symbols, name, chapter, info_path, info, doc, - doc_output, doc_files, graph_file, documents, verbose, readme)); - Synchronized.change browser_info (K empty_browser_info); - add_html_index (0, HTML.begin_session_index symbols name (Url.File session_graph_path) docs) - end; + val docs = + (case readme of NONE => [] | SOME p => [(Url.File p, "README")]) @ + map (fn (name, _) => (Url.File (Path.ext doc (Path.basic name)), name)) documents; + in + session_info := + SOME (make_session_info (symbols, name, chapter, info_path, info, doc, + doc_output, doc_files, graph_file, documents, verbose, readme)); + Synchronized.change browser_info (K empty_browser_info); + add_html_index (0, HTML.begin_session_index symbols name (Url.File session_graph_path) docs) + end; (* isabelle tool wrappers *) diff -r beef2e221c26 -r 74c874b5aed0 src/Pure/Tools/build.ML --- a/src/Pure/Tools/build.ML Sat Mar 28 17:27:08 2020 +0000 +++ b/src/Pure/Tools/build.ML Sat Mar 28 21:54:31 2020 +0100 @@ -133,7 +133,6 @@ datatype args = Args of {symbol_codes: (string * int) list, command_timings: Properties.T list, - do_output: bool, verbose: bool, browser_info: Path.T, document_files: (Path.T * Path.T) list, @@ -154,20 +153,20 @@ let open XML.Decode; val position = Position.of_properties o properties; - val (symbol_codes, (command_timings, (do_output, (verbose, (browser_info, + val (symbol_codes, (command_timings, (verbose, (browser_info, (document_files, (graph_file, (parent_name, (chapter, (name, (master_dir, (theories, (session_positions, (session_directories, (doc_names, (global_theories, - (loaded_theories, bibtex_entries))))))))))))))))) = - pair (list (pair string int)) (pair (list properties) (pair bool (pair bool (pair string + (loaded_theories, bibtex_entries)))))))))))))))) = + pair (list (pair string int)) (pair (list properties) (pair bool (pair string (pair (list (pair string string)) (pair string (pair string (pair string (pair string (pair string (pair (((list (pair Options.decode (list (pair string position)))))) (pair (list (pair string properties)) (pair (list (pair string string)) (pair (list string) - (pair (list (pair string string)) (pair (list string) (list string))))))))))))))))) + (pair (list (pair string string)) (pair (list string) (list string)))))))))))))))) (YXML.parse_body yxml); in - Args {symbol_codes = symbol_codes, command_timings = command_timings, do_output = do_output, + Args {symbol_codes = symbol_codes, command_timings = command_timings, verbose = verbose, browser_info = Path.explode browser_info, document_files = map (apply2 Path.explode) document_files, graph_file = Path.explode graph_file, parent_name = parent_name, chapter = chapter, @@ -177,7 +176,7 @@ bibtex_entries = bibtex_entries} end; -fun build_session (Args {symbol_codes, command_timings, do_output, verbose, browser_info, +fun build_session (Args {symbol_codes, command_timings, verbose, browser_info, document_files, graph_file, parent_name, chapter, name, master_dir, theories, session_positions, session_directories, doc_names, global_theories, loaded_theories, bibtex_entries}) = let @@ -194,7 +193,6 @@ val _ = Session.init symbols - do_output (Options.default_bool "browser_info") browser_info (Options.default_string "document") @@ -217,6 +215,8 @@ val _ = Resources.finish_session_base (); val _ = Par_Exn.release_all [res1, res2]; + val _ = + if name = Context.PureN then Theory.install_pure (Thy_Info.get_theory Context.PureN) else (); in () end; (*command-line tool*) diff -r beef2e221c26 -r 74c874b5aed0 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Sat Mar 28 17:27:08 2020 +0000 +++ b/src/Pure/Tools/build.scala Sat Mar 28 21:54:31 2020 +0100 @@ -177,8 +177,8 @@ val functions = List( - Markup.BUILD_SESSION_FINISHED -> build_session_finished _, - Markup.LOADING_THEORY -> loading_theory _) + Markup.BUILD_SESSION_FINISHED -> build_session_finished, + Markup.LOADING_THEORY -> loading_theory) } @@ -189,15 +189,15 @@ val info: Sessions.Info, deps: Sessions.Deps, store: Sessions.Store, - do_output: Boolean, + do_store: Boolean, verbose: Boolean, pide: Boolean, val numa_node: Option[Int], command_timings: List[Properties.T]) { - val options = NUMA.policy_options(info.options, numa_node) + private val options = NUMA.policy_options(info.options, numa_node) - val sessions_structure = deps.sessions_structure + private val sessions_structure = deps.sessions_structure private val graph_file = Isabelle_System.tmp_file("session_graph", "pdf") isabelle.graphview.Graph_File.write(options, graph_file, deps(name).session_graph_display) @@ -214,22 +214,22 @@ YXML.string_of_body( { import XML.Encode._ - pair(list(pair(string, int)), pair(list(properties), pair(bool, pair(bool, + pair(list(pair(string, int)), pair(list(properties), pair(bool, pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string, pair(string, pair(string, pair(string, pair(Path.encode, pair(list(pair(Options.encode, list(pair(string, properties)))), pair(list(pair(string, properties)), pair(list(pair(string, string)), pair(list(string), pair(list(pair(string, string)), - pair(list(string), list(string))))))))))))))))))( - (Symbol.codes, (command_timings, (do_output, (verbose, + pair(list(string), list(string)))))))))))))))))( + (Symbol.codes, (command_timings, (verbose, (store.browser_info, (info.document_files, (File.standard_path(graph_file), (parent, (info.chapter, (name, (Path.current, (info.theories, (sessions_structure.session_positions, (sessions_structure.dest_session_directories, (base.doc_names, (base.global_theories.toList, - (base.loaded_theories.keys, info.bibtex_entries.map(_.info))))))))))))))))))) + (base.loaded_theories.keys, info.bibtex_entries.map(_.info)))))))))))))))))) }) val env = @@ -237,12 +237,17 @@ ("ISABELLE_EXPORT_TMP" -> File.standard_path(export_tmp_dir)) + ("ISABELLE_ML_DEBUGGER" -> options.bool("ML_debugger").toString) - def save_heap: String = - (if (info.theories.isEmpty) "" else "ML_Heap.share_common_data (); ") + - "ML_Heap.save_child " + - ML_Syntax.print_string_bytes(File.platform_path(store.output_heap(name))) + val is_pure = Sessions.is_pure(name) - if (pide && !Sessions.is_pure(name)) { + val eval_store = + if (!do_store) Nil + else { + (if (info.theories.nonEmpty) List("ML_Heap.share_common_data ()") else Nil) ::: + List("ML_Heap.save_child " + + ML_Syntax.print_string_bytes(File.platform_path(store.output_heap(name)))) + } + + if (pide && !is_pure) { val resources = new Resources(sessions_structure, deps(parent)) val session = new Session(options, resources) val handler = new Handler(progress, session, name) @@ -267,14 +272,11 @@ val args_file = Isabelle_System.tmp_file("build") File.write(args_file, args_yxml) - val eval = - "Command_Line.tool0 (fn () => (" + - "Build.build " + ML_Syntax.print_string_bytes(File.standard_path(args_file)) + - (if (Sessions.is_pure(name)) "; Theory.install_pure (Thy_Info.get_theory Context.PureN)" - else "") + (if (do_output) "; " + save_heap else "") + "));" + val eval_build = "Build.build " + ML_Syntax.print_string_bytes(File.standard_path(args_file)) + val eval = Command_Line.ML_tool0(eval_build :: eval_store) val process = - if (Sessions.is_pure(name)) { + if (is_pure) { ML_Process(options, deps.sessions_structure, store, raw_ml_system = true, args = (for ((root, _) <- Thy_Header.ml_roots) yield List("--use", root)).flatten ::: @@ -357,7 +359,7 @@ else result1 val heap_digest = - if (result2.ok && do_output && store.output_heap(name).is_file) + if (result2.ok && do_store && store.output_heap(name).is_file) Some(Sessions.write_heap_digest(store.output_heap(name))) else None @@ -596,7 +598,7 @@ map(results(_)) val ancestor_heaps = ancestor_results.flatMap(_.heap_digest) - val do_output = build_heap || Sessions.is_pure(name) || queue.is_inner(name) + val do_store = build_heap || Sessions.is_pure(name) || queue.is_inner(name) val (current, heap_digest) = { @@ -611,7 +613,7 @@ build.sources == sources_stamp(deps, name) && build.input_heaps == ancestor_heaps && build.output_heap == heap_digest && - !(do_output && heap_digest.isEmpty) + !(do_store && heap_digest.isEmpty) (current, heap_digest) case None => (false, None) } @@ -629,14 +631,14 @@ results + (name -> Result(false, heap_digest, Some(Process_Result(1)), info))) } else if (ancestor_results.forall(_.ok) && !progress.stopped) { - progress.echo((if (do_output) "Building " else "Running ") + name + " ...") + progress.echo((if (do_store) "Building " else "Running ") + name + " ...") store.clean_output(name) using(store.open_database(name, output = true))(store.init_session_info(_, name)) val numa_node = numa_nodes.next(used_node) val job = - new Job(progress, name, info, deps, store, do_output, verbose, pide = pide, + new Job(progress, name, info, deps, store, do_store, verbose, pide = pide, numa_node, queue.command_timings(name)) loop(pending, running + (name -> (ancestor_heaps, job)), results) } diff -r beef2e221c26 -r 74c874b5aed0 src/Pure/Tools/simplifier_trace.scala --- a/src/Pure/Tools/simplifier_trace.scala Sat Mar 28 17:27:08 2020 +0000 +++ b/src/Pure/Tools/simplifier_trace.scala Sat Mar 28 21:54:31 2020 +0100 @@ -315,6 +315,6 @@ false } - val functions = List(Markup.SIMP_TRACE_CANCEL -> cancel _) + val functions = List(Markup.SIMP_TRACE_CANCEL -> cancel) } }