# HG changeset patch # User wenzelm # Date 1605647159 -3600 # Node ID fd68c9c1b90b8b5a79e8a2080e4be300015987c0 # Parent 09ee9eb7a3d31d8931de3232a416a16cb8ac8f15 more uniform Resources.init_session via YXML; diff -r 09ee9eb7a3d3 -r fd68c9c1b90b src/Pure/ML/ml_process.scala --- 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( diff -r 09ee9eb7a3d3 -r fd68c9c1b90b src/Pure/PIDE/protocol.ML --- 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" diff -r 09ee9eb7a3d3 -r fd68c9c1b90b src/Pure/PIDE/protocol.scala --- 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 */ diff -r 09ee9eb7a3d3 -r fd68c9c1b90b src/Pure/PIDE/resources.ML --- 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, ...} => diff -r 09ee9eb7a3d3 -r fd68c9c1b90b src/Pure/PIDE/resources.scala --- 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] = diff -r 09ee9eb7a3d3 -r fd68c9c1b90b src/Pure/Tools/build.ML --- 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); diff -r 09ee9eb7a3d3 -r fd68c9c1b90b src/Pure/Tools/build.scala --- 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))) }