# HG changeset patch
# User wenzelm
# Date 1491586539 -7200
# Node ID 4a3e6cda3b94fc30c480be4f2e9e8888ae6d562a
# Parent  4433d189a77d8ad853d213f1dd5dd73b9422384b
provide session base for "isabelle build" and "isabelle console" ML process;

diff -r 4433d189a77d -r 4a3e6cda3b94 src/Pure/ML/ml_syntax.scala
--- a/src/Pure/ML/ml_syntax.scala	Fri Apr 07 18:26:30 2017 +0200
+++ b/src/Pure/ML/ml_syntax.scala	Fri Apr 07 19:35:39 2017 +0200
@@ -46,6 +46,12 @@
     quote(UTF8.bytes(str).iterator.map(print_chr(_)).mkString)
 
 
+  /* pair */
+
+  def print_pair[A, B](f: A => String, g: B => String)(pair: (A, B)): String =
+    "(" + f(pair._1) + ", " + g(pair._2) + ")"
+
+
   /* list */
 
   def print_list[A](f: A => String)(list: List[A]): String =
diff -r 4433d189a77d -r 4a3e6cda3b94 src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Fri Apr 07 18:26:30 2017 +0200
+++ b/src/Pure/PIDE/resources.ML	Fri Apr 07 19:35:39 2017 +0200
@@ -6,6 +6,9 @@
 
 signature RESOURCES =
 sig
+  val set_session_base: {known_theories: (string * string) list} -> unit
+  val reset_session_base: unit -> unit
+  val known_theory: string -> Path.T option
   val master_directory: theory -> Path.T
   val imports_of: theory -> (string * Position.T) list
   val thy_path: Path.T -> Path.T
@@ -25,6 +28,23 @@
 structure Resources: RESOURCES =
 struct
 
+(* session base *)
+
+val global_session_base =
+  Synchronized.var "Sessions.base"
+    ({known_theories = Symtab.empty: Path.T Symtab.table});
+
+fun set_session_base {known_theories} =
+  Synchronized.change global_session_base
+    (K {known_theories = Symtab.make (map (apsnd Path.explode) known_theories)});
+
+fun reset_session_base () =
+  set_session_base {known_theories = []};
+
+fun known_theory name =
+  Symtab.lookup (#known_theories (Synchronized.value global_session_base)) name;
+
+
 (* manage source files *)
 
 type files =
diff -r 4433d189a77d -r 4a3e6cda3b94 src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Fri Apr 07 18:26:30 2017 +0200
+++ b/src/Pure/Tools/build.ML	Fri Apr 07 19:35:39 2017 +0200
@@ -144,30 +144,37 @@
   chapter: string,
   name: string,
   master_dir: Path.T,
-  theories: (Options.T * (string * Position.T) list) list};
+  theories: (Options.T * (string * Position.T) list) list,
+  known_theories: (string * string) list};
 
 fun decode_args yxml =
   let
     open XML.Decode;
     val (symbol_codes, (command_timings, (do_output, (verbose, (browser_info,
-      (document_files, (graph_file, (parent_name, (chapter, (name, (master_dir, theories))))))))))) =
+      (document_files, (graph_file, (parent_name, (chapter, (name, (master_dir,
+      (theories, known_theories)))))))))))) =
       pair (list (pair string int)) (pair (list properties) (pair bool (pair bool (pair string
         (pair (list (pair string string)) (pair string (pair string (pair string (pair string
-          (pair string (((list (pair Options.decode (list (string #> rpair Position.none))))))))))))))))
+          (pair string
+            (pair (((list (pair Options.decode (list (string #> rpair Position.none))))))
+              (list (pair string string)))))))))))))
       (YXML.parse_body yxml);
   in
     Args {symbol_codes = symbol_codes, command_timings = command_timings, do_output = do_output,
       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,
-      name = name, master_dir = Path.explode master_dir, theories = theories}
+      name = name, master_dir = Path.explode master_dir, theories = theories,
+      known_theories = known_theories}
   end;
 
 fun build_session (Args {symbol_codes, command_timings, do_output, verbose, browser_info,
-    document_files, graph_file, parent_name, chapter, name, master_dir, theories}) =
+    document_files, graph_file, parent_name, chapter, name, master_dir, theories, known_theories}) =
   let
     val symbols = HTML.make_symbols symbol_codes;
 
+    val _ = Resources.set_session_base {known_theories = known_theories};
+
     val _ =
       Session.init
         symbols
@@ -191,6 +198,8 @@
           |> session_timing name verbose
           |> Exn.capture);
     val res2 = Exn.capture Session.finish ();
+
+    val _ = Resources.reset_session_base ();
     val _ = Par_Exn.release_all [res1, res2];
   in () end;
 
diff -r 4433d189a77d -r 4a3e6cda3b94 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Fri Apr 07 18:26:30 2017 +0200
+++ b/src/Pure/Tools/build.scala	Fri Apr 07 19:35:39 2017 +0200
@@ -197,6 +197,10 @@
       Future.thread("build") {
         val parent = info.parent.getOrElse("")
 
+        val known_theories =
+          for ((theory, node_name) <- deps(name).known_theories.toList)
+            yield (theory, node_name.node)
+
         val args_yxml =
           YXML.string_of_body(
             {
@@ -204,11 +208,13 @@
               pair(list(pair(string, int)), pair(list(properties), pair(bool, pair(bool,
                 pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string,
                 pair(string, pair(string, pair(string, pair(Path.encode,
-                list(pair(Options.encode, list(string))))))))))))))(
+                pair(list(pair(Options.encode, list(string))),
+                list(pair(string, string))))))))))))))(
               (Symbol.codes, (command_timings, (do_output, (verbose,
                 (store.browser_info, (info.document_files, (File.standard_path(graph_file),
                 (parent, (info.chapter, (name, (Path.current,
-                info.theories))))))))))))
+                (info.theories,
+                known_theories)))))))))))))
             })
 
         val env =
diff -r 4433d189a77d -r 4a3e6cda3b94 src/Pure/Tools/ml_console.scala
--- a/src/Pure/Tools/ml_console.scala	Fri Apr 07 18:26:30 2017 +0200
+++ b/src/Pure/Tools/ml_console.scala	Fri Apr 07 19:35:39 2017 +0200
@@ -72,7 +72,10 @@
       val process =
         ML_Process(options, logic = logic, args = List("-i"), dirs = dirs, redirect = true,
           modes = if (raw_ml_system) Nil else modes ::: List("ASCII"),
-          raw_ml_system = raw_ml_system, store = Sessions.store(system_mode))
+          raw_ml_system = raw_ml_system, store = Sessions.store(system_mode),
+          session_base =
+            if (raw_ml_system) None
+            else Some(Sessions.session_base(options, logic, dirs)))
       val process_output = Future.thread[Unit]("process_output") {
         try {
           var result = new StringBuilder(100)
diff -r 4433d189a77d -r 4a3e6cda3b94 src/Pure/Tools/ml_process.scala
--- a/src/Pure/Tools/ml_process.scala	Fri Apr 07 18:26:30 2017 +0200
+++ b/src/Pure/Tools/ml_process.scala	Fri Apr 07 19:35:39 2017 +0200
@@ -24,6 +24,7 @@
     cleanup: () => Unit = () => (),
     channel: Option[System_Channel] = None,
     sessions: Option[Sessions.T] = None,
+    session_base: Option[Sessions.Base] = None,
     store: Sessions.Store = Sessions.store()): Bash.Process =
   {
     val logic_name = Isabelle_System.default_logic(logic)
@@ -89,6 +90,21 @@
     val env_options = Map("ISABELLE_PROCESS_OPTIONS" -> File.standard_path(isabelle_process_options))
     val eval_options = if (heaps.isEmpty) Nil else List("Options.load_default ()")
 
+    // session base
+    val eval_session_base =
+      session_base match {
+        case None => Nil
+        case Some(base) =>
+          val known_theories =
+            for ((theory, node_name) <- base.known_theories.toList)
+              yield (theory, node_name.node)
+          List("Resources.set_session_base {known_theories = " +
+            ML_Syntax.print_list(
+              ML_Syntax.print_pair(
+                ML_Syntax.print_string, ML_Syntax.print_string))(known_theories) + "}")
+      }
+
+    // process
     val eval_process =
       if (heaps.isEmpty)
         List("PolyML.print_depth " + ML_Syntax.print_int(options.int("ML_print_depth")))
@@ -114,7 +130,7 @@
     // bash
     val bash_args =
       ml_runtime_options :::
-      (eval_init ::: eval_modes ::: eval_options ::: eval_process).
+      (eval_init ::: eval_modes ::: eval_options ::: eval_session_base ::: eval_process).
         map(eval => List("--eval", eval)).flatten ::: args
 
     Bash.process(