--- a/src/Pure/ML/ml_process.scala Tue Nov 17 16:54:49 2020 +0100
+++ b/src/Pure/ML/ml_process.scala Tue Nov 17 22:05:59 2020 +0100
@@ -78,40 +78,16 @@
val eval_options = if (heaps.isEmpty) Nil else List("Options.load_default ()")
// session base
- val init_session = Isabelle_System.tmp_file("init_session", ext = "ML")
- val init_session_name = init_session.getAbsolutePath
+ val init_session = Isabelle_System.tmp_file("init_session")
Isabelle_System.chmod("600", File.path(init_session))
- File.write(init_session,
+ val eval_init_session =
session_base match {
- case None => ""
+ case None => Nil
case Some(base) =>
- def print_symbols: List[(String, Int)] => String =
- ML_Syntax.print_list(
- ML_Syntax.print_pair(ML_Syntax.print_string_bytes, ML_Syntax.print_int))
- def print_table: List[(String, String)] => String =
- ML_Syntax.print_list(
- ML_Syntax.print_pair(
- ML_Syntax.print_string_bytes, ML_Syntax.print_string_bytes))
- def print_list: List[String] => String =
- ML_Syntax.print_list(ML_Syntax.print_string_bytes)
- def print_sessions: List[(String, Position.T)] => String =
- ML_Syntax.print_list(
- ML_Syntax.print_pair(ML_Syntax.print_string_bytes, ML_Syntax.print_properties))
- def print_bibtex_entries: List[(String, List[String])] => String =
- ML_Syntax.print_list(
- ML_Syntax.print_pair(ML_Syntax.print_string_bytes,
- ML_Syntax.print_list(ML_Syntax.print_string_bytes)))
-
- "Resources.init_session" +
- "{html_symbols = " + print_symbols(Symbol.codes) +
- ", session_positions = " + print_sessions(sessions_structure.session_positions) +
- ", session_directories = " + print_table(sessions_structure.dest_session_directories) +
- ", session_chapters = " + print_table(sessions_structure.session_chapters) +
- ", bibtex_entries = " + print_bibtex_entries(sessions_structure.bibtex_entries) +
- ", docs = " + print_list(base.doc_names) +
- ", global_theories = " + print_table(base.global_theories.toList) +
- ", loaded_theories = " + print_list(base.loaded_theories.keys) + "}"
- })
+ File.write(init_session, new Resources(sessions_structure, base).init_session_yxml)
+ List("Resources.init_session_file (Path.explode " +
+ ML_Syntax.print_string_bytes(File.path(init_session).implode) + ")")
+ }
// process
val eval_process =
@@ -144,9 +120,7 @@
// bash
val bash_args =
ml_runtime_options :::
- (eval_init ::: eval_modes ::: eval_options).flatMap(List("--eval", _)) :::
- List("--use", init_session_name,
- "--eval", "OS.FileSys.remove " + ML_Syntax.print_string_bytes(init_session_name)) :::
+ (eval_init ::: eval_modes ::: eval_options ::: eval_init_session).flatMap(List("--eval", _)) :::
use_prelude.flatMap(List("--use", _)) ::: List("--eval", eval_process) ::: args
Bash.process(
--- a/src/Pure/PIDE/protocol.ML Tue Nov 17 16:54:49 2020 +0100
+++ b/src/Pure/PIDE/protocol.ML Tue Nov 17 22:05:59 2020 +0100
@@ -25,27 +25,7 @@
val _ =
Isabelle_Process.protocol_command "Prover.init_session"
- (fn [html_symbols_yxml, session_positions_yxml, session_directories_yxml, session_chapters_yxml,
- bibtex_entries_yxml, doc_names_yxml, global_theories_yxml, loaded_theories_yxml] =>
- let
- val decode_symbols = YXML.parse_body #> let open XML.Decode in list (pair string int) end;
- val decode_table = YXML.parse_body #> let open XML.Decode in list (pair string string) end;
- val decode_list = YXML.parse_body #> let open XML.Decode in list string end;
- val decode_sessions =
- YXML.parse_body #> let open XML.Decode in list (pair string properties) end;
- val decode_bibtex_entries =
- YXML.parse_body #> let open XML.Decode in list (pair string (list string)) end;
- in
- Resources.init_session
- {html_symbols = decode_symbols html_symbols_yxml,
- session_positions = decode_sessions session_positions_yxml,
- session_directories = decode_table session_directories_yxml,
- session_chapters = decode_table session_chapters_yxml,
- bibtex_entries = decode_bibtex_entries bibtex_entries_yxml,
- docs = decode_list doc_names_yxml,
- global_theories = decode_table global_theories_yxml,
- loaded_theories = decode_list loaded_theories_yxml}
- end);
+ (fn [yxml] => Resources.init_session_yxml yxml);
val _ =
Isabelle_Process.protocol_command "Document.define_blob"
--- a/src/Pure/PIDE/protocol.scala Tue Nov 17 16:54:49 2020 +0100
+++ b/src/Pure/PIDE/protocol.scala Tue Nov 17 22:05:59 2020 +0100
@@ -283,33 +283,10 @@
protocol_command("Prover.options", Symbol.encode_yxml(opts.encode))
- /* session base */
-
- def init_session(resources: Resources)
- {
- import XML.Encode._
+ /* resources */
- def encode_symbols(arg: List[(String, Int)]): String =
- Symbol.encode_yxml(list(pair(string, int))(arg))
- def encode_table(arg: List[(String, String)]): String =
- Symbol.encode_yxml(list(pair(string, string))(arg))
- def encode_list(arg: List[String]): String =
- Symbol.encode_yxml(list(string)(arg))
- def encode_sessions(arg: List[(String, Position.T)]): String =
- Symbol.encode_yxml(list(pair(string, properties))(arg))
- def encode_bibtex_entries(arg: List[(String, List[String])]): String =
- Symbol.encode_yxml(list(pair(string, list(string)))(arg))
-
- protocol_command("Prover.init_session",
- encode_symbols(Symbol.codes),
- encode_sessions(resources.sessions_structure.session_positions),
- encode_table(resources.sessions_structure.dest_session_directories),
- encode_table(resources.sessions_structure.session_chapters),
- encode_bibtex_entries(resources.sessions_structure.bibtex_entries),
- encode_list(resources.session_base.doc_names),
- encode_table(resources.session_base.global_theories.toList),
- encode_list(resources.session_base.loaded_theories.keys))
- }
+ def init_session(resources: Resources): Unit =
+ protocol_command("Prover.init_session", resources.init_session_yxml)
/* interned items */
--- a/src/Pure/PIDE/resources.ML Tue Nov 17 16:54:49 2020 +0100
+++ b/src/Pure/PIDE/resources.ML Tue Nov 17 22:05:59 2020 +0100
@@ -16,6 +16,8 @@
docs: string list,
global_theories: (string * string) list,
loaded_theories: string list} -> unit
+ val init_session_yxml: string -> unit
+ val init_session_file: Path.T -> unit
val finish_session_base: unit -> unit
val global_theory: string -> string option
val loaded_theory: string -> bool
@@ -86,6 +88,32 @@
global_theories = Symtab.make global_theories,
loaded_theories = Symtab.make_set loaded_theories});
+fun init_session_yxml yxml =
+ let
+ val (html_symbols, (session_positions, (session_directories, (session_chapters,
+ (bibtex_entries, (docs, (global_theories, loaded_theories))))))) =
+ YXML.parse_body yxml |>
+ let open XML.Decode in
+ pair (list (pair string int)) (pair (list (pair string properties))
+ (pair (list (pair string string)) (pair (list (pair string string))
+ (pair (list (pair string (list string))) (pair (list string)
+ (pair (list (pair string string)) (list string)))))))
+ end;
+ in
+ init_session
+ {html_symbols = html_symbols,
+ session_positions = session_positions,
+ session_directories = session_directories,
+ session_chapters = session_chapters,
+ bibtex_entries = bibtex_entries,
+ docs = docs,
+ global_theories = global_theories,
+ loaded_theories = loaded_theories}
+ end;
+
+fun init_session_file path =
+ init_session_yxml (File.read path) before File.rm path;
+
fun finish_session_base () =
Synchronized.change global_session_base
(fn {global_theories, loaded_theories, ...} =>
--- a/src/Pure/PIDE/resources.scala Tue Nov 17 16:54:49 2020 +0100
+++ b/src/Pure/PIDE/resources.scala Tue Nov 17 22:05:59 2020 +0100
@@ -20,6 +20,31 @@
resources =>
+ /* init session */
+
+ def init_session_yxml: String =
+ {
+ import XML.Encode._
+
+ YXML.string_of_body(
+ pair(list(pair(string, int)),
+ pair(list(pair(string, properties)),
+ pair(list(pair(string, string)),
+ pair(list(pair(string, string)),
+ pair(list(pair(string, list(string))),
+ pair(list(string),
+ pair(list(pair(string, string)), list(string))))))))(
+ (Symbol.codes,
+ (resources.sessions_structure.session_positions,
+ (resources.sessions_structure.dest_session_directories,
+ (resources.sessions_structure.session_chapters,
+ (resources.sessions_structure.bibtex_entries,
+ (resources.session_base.doc_names,
+ (resources.session_base.global_theories.toList,
+ resources.session_base.loaded_theories.keys)))))))))
+ }
+
+
/* file formats */
def make_theory_name(name: Document.Node.Name): Option[Document.Node.Name] =
--- a/src/Pure/Tools/build.ML Tue Nov 17 16:54:49 2020 +0100
+++ b/src/Pure/Tools/build.ML Tue Nov 17 22:05:59 2020 +0100
@@ -84,39 +84,21 @@
val _ =
Isabelle_Process.protocol_command "build_session"
- (fn [args_yxml] =>
+ (fn [resources_yxml, args_yxml] =>
let
- val (html_symbols, (command_timings, (parent_name, (chapter,
- (session_name, (theories,
- (session_positions, (session_directories,
- (session_chapters, (doc_names,
- (global_theories, (loaded_theories, bibtex_entries)))))))))))) =
+ val _ = Resources.init_session_yxml resources_yxml;
+ val (command_timings, (parent_name, (chapter, (session_name, theories)))) =
YXML.parse_body args_yxml |>
let
open XML.Decode;
val position = Position.of_properties o properties;
in
- pair (list (pair string int)) (pair (list properties) (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 (pair string string)) (pair (list string)
- (pair (list (pair string string)) (pair (list string)
- (list (pair string (list string))))))))))))))
+ pair (list properties) (pair string (pair string
+ (pair string (list (pair Options.decode (list (pair string position)))))))
end;
fun build () =
let
- val _ =
- Resources.init_session
- {html_symbols = html_symbols,
- session_positions = session_positions,
- session_directories = session_directories,
- session_chapters = session_chapters,
- bibtex_entries = bibtex_entries,
- docs = doc_names,
- global_theories = global_theories,
- loaded_theories = loaded_theories};
-
val _ = Session.init parent_name (chapter, session_name);
val last_timing = get_timings (fold update_timings command_timings empty_timings);
--- a/src/Pure/Tools/build.scala Tue Nov 17 16:54:49 2020 +0100
+++ b/src/Pure/Tools/build.scala Tue Nov 17 22:05:59 2020 +0100
@@ -170,26 +170,6 @@
Future.thread("build", uninterruptible = true) {
val parent = info.parent.getOrElse("")
val base = deps(parent)
- val args_yxml =
- YXML.string_of_body(
- {
- import XML.Encode._
- pair(list(pair(string, int)), pair(list(properties), pair(string, pair(string,
- pair(string, pair(list(pair(Options.encode, list(pair(string, properties)))),
- pair(list(pair(string, properties)),
- pair(list(pair(string, string)),
- pair(list(pair(string, string)),
- pair(list(string),
- pair(list(pair(string, string)),
- pair(list(string), list(pair(string, list(string)))))))))))))))(
- (Symbol.codes, (command_timings0, (parent, (info.chapter,
- (session_name, (info.theories,
- (sessions_structure.session_positions,
- (sessions_structure.dest_session_directories,
- (sessions_structure.session_chapters,
- (base.doc_names, (base.global_theories.toList,
- (base.loaded_theories.keys, sessions_structure.bibtex_entries)))))))))))))
- })
val env =
Isabelle_System.settings() +
@@ -207,7 +187,7 @@
}
else Nil
- val resources = new Resources(sessions_structure, deps(parent))
+ val resources = new Resources(sessions_structure, base)
val session =
new Session(options, resources) {
override val xml_cache: XML.Cache = store.xml_cache
@@ -356,7 +336,16 @@
Isabelle_Thread.interrupt_handler(_ => process.terminate) {
Exn.capture { process.await_startup } match {
case Exn.Res(_) =>
- session.protocol_command("build_session", args_yxml)
+ val resources_yxml = resources.init_session_yxml
+ val args_yxml =
+ YXML.string_of_body(
+ {
+ import XML.Encode._
+ pair(list(properties), pair(string, pair(string, pair(string,
+ list(pair(Options.encode, list(pair(string, properties))))))))(
+ (command_timings0, (parent, (info.chapter, (session_name, info.theories)))))
+ })
+ session.protocol_command("build_session", resources_yxml, args_yxml)
Build_Session_Errors.result
case Exn.Exn(exn) => Exn.Res(List(Exn.message(exn)))
}