--- 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 =
--- 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 =
--- 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;
--- 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 =
--- 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)
--- 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(