more uniform Resources.init_session via YXML;
authorwenzelm
Tue, 17 Nov 2020 22:05:59 +0100
changeset 72873 fd68c9c1b90b
parent 72872 09ee9eb7a3d3
child 72874 2a7fc87495e0
more uniform Resources.init_session via YXML;
src/Pure/ML/ml_process.scala
src/Pure/PIDE/protocol.ML
src/Pure/PIDE/protocol.scala
src/Pure/PIDE/resources.ML
src/Pure/PIDE/resources.scala
src/Pure/Tools/build.ML
src/Pure/Tools/build.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(
--- 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)))
             }