--- a/src/Pure/PIDE/resources.ML Sat Apr 08 12:47:34 2017 +0200
+++ b/src/Pure/PIDE/resources.ML Sat Apr 08 20:56:41 2017 +0200
@@ -6,8 +6,15 @@
signature RESOURCES =
sig
- val set_session_base: {known_theories: (string * string) list} -> unit
+ val set_session_base:
+ {default_qualifier: string,
+ global_theories: string list,
+ loaded_theories: (string * string) list,
+ known_theories: (string * string) list} -> unit
val reset_session_base: unit -> unit
+ val default_qualifier: unit -> string
+ val global_theory: string -> bool
+ val loaded_theory: string -> Path.T option
val known_theory: string -> Path.T option
val master_directory: theory -> Path.T
val imports_of: theory -> (string * Position.T) list
@@ -30,19 +37,32 @@
(* session base *)
-val global_session_base =
- Synchronized.var "Sessions.base"
- ({known_theories = Symtab.empty: Path.T Symtab.table});
+val init_session_base =
+ {default_qualifier = "",
+ global_theories = Symtab.make_set [],
+ loaded_theories = Symtab.empty: Path.T Symtab.table,
+ known_theories = Symtab.empty: Path.T Symtab.table};
-fun set_session_base {known_theories} =
+val global_session_base =
+ Synchronized.var "Sessions.base" init_session_base;
+
+fun set_session_base {default_qualifier, global_theories, loaded_theories, known_theories} =
Synchronized.change global_session_base
- (K {known_theories = Symtab.make (map (apsnd Path.explode) known_theories)});
+ (fn _ =>
+ {default_qualifier = default_qualifier,
+ global_theories = Symtab.make_set global_theories,
+ loaded_theories = Symtab.make (map (apsnd Path.explode) loaded_theories),
+ known_theories = Symtab.make (map (apsnd Path.explode) known_theories)});
fun reset_session_base () =
- set_session_base {known_theories = []};
+ Synchronized.change global_session_base (K init_session_base);
+
+fun get_session_base f = f (Synchronized.value global_session_base);
-fun known_theory name =
- Symtab.lookup (#known_theories (Synchronized.value global_session_base)) name;
+fun default_qualifier () = get_session_base #default_qualifier;
+fun global_theory a = Symtab.defined (get_session_base #global_theories) a;
+fun loaded_theory a = Symtab.lookup (get_session_base #loaded_theories) a;
+fun known_theory a = Symtab.lookup (get_session_base #known_theories) a;
(* manage source files *)
--- a/src/Pure/PIDE/resources.scala Sat Apr 08 12:47:34 2017 +0200
+++ b/src/Pure/PIDE/resources.scala Sat Apr 08 20:56:41 2017 +0200
@@ -14,8 +14,8 @@
class Resources(
- val session_name: String,
val session_base: Sessions.Base,
+ val default_qualifier: String = "",
val log: Logger = No_Logger)
{
val thy_info = new Thy_Info(this)
@@ -72,7 +72,7 @@
val theory0 = Thy_Header.base_name(s)
val theory =
if (Long_Name.is_qualified(theory0) || session_base.global_theories.contains(theory0)) theory0
- else Long_Name.qualify(session_name, theory0)
+ else Long_Name.qualify(default_qualifier, theory0)
session_base.loaded_theories.get(theory) orElse
session_base.loaded_theories.get(theory0) orElse
--- a/src/Pure/Thy/sessions.scala Sat Apr 08 12:47:34 2017 +0200
+++ b/src/Pure/Thy/sessions.scala Sat Apr 08 20:56:41 2017 +0200
@@ -58,6 +58,10 @@
def loaded_theory(name: Document.Node.Name): Boolean =
loaded_theories.isDefinedAt(name.theory)
+ def dest_loaded_theories: List[(String, String)] =
+ for ((theory, node_name) <- loaded_theories.toList)
+ yield (theory, node_name.node)
+
def dest_known_theories: List[(String, String)] =
for ((theory, node_name) <- known_theories.toList)
yield (theory, node_name.node)
@@ -91,7 +95,7 @@
case None => Base.bootstrap
case Some(parent) => sessions(parent)
}
- val resources = new Resources(session_name, parent_base)
+ val resources = new Resources(parent_base, default_qualifier = session_name)
if (verbose || list_files) {
val groups =
--- a/src/Pure/Tools/build.ML Sat Apr 08 12:47:34 2017 +0200
+++ b/src/Pure/Tools/build.ML Sat Apr 08 20:56:41 2017 +0200
@@ -145,6 +145,8 @@
name: string,
master_dir: Path.T,
theories: (Options.T * (string * Position.T) list) list,
+ global_theories: string list,
+ loaded_theories: (string * string) list,
known_theories: (string * string) list};
fun decode_args yxml =
@@ -152,12 +154,13 @@
open XML.Decode;
val (symbol_codes, (command_timings, (do_output, (verbose, (browser_info,
(document_files, (graph_file, (parent_name, (chapter, (name, (master_dir,
- (theories, known_theories)))))))))))) =
+ (theories, (global_theories, (loaded_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
(pair (((list (pair Options.decode (list (string #> rpair Position.none))))))
- (list (pair string string)))))))))))))
+ (pair (list string)
+ (pair (list (pair string string)) (list (pair string string)))))))))))))))
(YXML.parse_body yxml);
in
Args {symbol_codes = symbol_codes, command_timings = command_timings, do_output = do_output,
@@ -165,15 +168,22 @@
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,
+ global_theories = global_theories, loaded_theories = loaded_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, known_theories}) =
+ document_files, graph_file, parent_name, chapter, name, master_dir, theories,
+ global_theories, loaded_theories, known_theories}) =
let
val symbols = HTML.make_symbols symbol_codes;
- val _ = Resources.set_session_base {known_theories = known_theories};
+ val _ =
+ Resources.set_session_base
+ {default_qualifier = name,
+ global_theories = global_theories,
+ loaded_theories = loaded_theories,
+ known_theories = known_theories};
val _ =
Session.init
--- a/src/Pure/Tools/build.scala Sat Apr 08 12:47:34 2017 +0200
+++ b/src/Pure/Tools/build.scala Sat Apr 08 20:56:41 2017 +0200
@@ -196,7 +196,7 @@
private val future_result: Future[Process_Result] =
Future.thread("build") {
val parent = info.parent.getOrElse("")
-
+ val base = deps(name)
val args_yxml =
YXML.string_of_body(
{
@@ -205,12 +205,14 @@
pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string,
pair(string, pair(string, pair(string, pair(Path.encode,
pair(list(pair(Options.encode, list(string))),
- list(pair(string, string))))))))))))))(
+ pair(list(string),
+ pair(list(pair(string, 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,
- deps(name).dest_known_theories)))))))))))))
+ (base.global_theories.toList,
+ (base.dest_loaded_theories, base.dest_known_theories)))))))))))))))
})
val env =
@@ -222,7 +224,7 @@
ML_Syntax.print_string0(File.platform_path(output))
if (pide && !Sessions.is_pure(name)) {
- val resources = new Resources(name, deps(parent))
+ val resources = new Resources(deps(parent), default_qualifier = name)
val session = new Session(options, resources)
val handler = new Handler(progress, session, name)
session.init_protocol_handler(handler)
--- a/src/Pure/Tools/ml_process.scala Sat Apr 08 12:47:34 2017 +0200
+++ b/src/Pure/Tools/ml_process.scala Sat Apr 08 20:56:41 2017 +0200
@@ -95,10 +95,15 @@
session_base match {
case None => Nil
case Some(base) =>
- List("Resources.set_session_base {known_theories = " +
+ def print_table(table: List[(String, String)]): String =
ML_Syntax.print_list(
ML_Syntax.print_pair(
- ML_Syntax.print_string, ML_Syntax.print_string))(base.dest_known_theories) + "}")
+ ML_Syntax.print_string, ML_Syntax.print_string))(table)
+ List("Resources.set_session_base {default_qualifier = \"\"" +
+ ", global_theories = " +
+ ML_Syntax.print_list(ML_Syntax.print_string)(base.global_theories.toList) +
+ ", loaded_theories = " + print_table(base.dest_loaded_theories) +
+ ", known_theories = " + print_table(base.dest_known_theories) + "}")
}
// process
--- a/src/Tools/VSCode/src/vscode_resources.scala Sat Apr 08 12:47:34 2017 +0200
+++ b/src/Tools/VSCode/src/vscode_resources.scala Sat Apr 08 20:56:41 2017 +0200
@@ -43,7 +43,7 @@
val options: Options,
session_base: Sessions.Base,
log: Logger = No_Logger)
- extends Resources(session_name = "", session_base, log)
+ extends Resources(session_base, log = log)
{
private val state = Synchronized(VSCode_Resources.State())
--- a/src/Tools/jEdit/src/jedit_resources.scala Sat Apr 08 12:47:34 2017 +0200
+++ b/src/Tools/jEdit/src/jedit_resources.scala Sat Apr 08 20:56:41 2017 +0200
@@ -21,8 +21,7 @@
import org.gjt.sp.jedit.bufferio.BufferIORequest
-class JEdit_Resources(session_base: Sessions.Base)
- extends Resources(session_name = "", session_base)
+class JEdit_Resources(session_base: Sessions.Base) extends Resources(session_base)
{
/* document node name */