--- 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);
--- 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("; ") + "));"
}
-
--- 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 *)
--- 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*)
--- 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)
}
--- 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)
}
}