--- a/src/Pure/PIDE/resources.ML Mon Apr 10 13:30:55 2017 +0200
+++ b/src/Pure/PIDE/resources.ML Mon Apr 10 16:43:12 2017 +0200
@@ -8,12 +8,12 @@
sig
val set_session_base:
{default_qualifier: string,
- global_theories: string list,
+ global_theories: (string * 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 global_theory: string -> string option
val loaded_theory: string -> Path.T option
val known_theory: string -> Path.T option
val master_directory: theory -> Path.T
@@ -42,7 +42,7 @@
val init_session_base =
{default_qualifier = "Draft",
- global_theories = Symtab.make_set [],
+ global_theories = Symtab.empty: string Symtab.table,
loaded_theories = Symtab.empty: Path.T Symtab.table,
known_theories = Symtab.empty: Path.T Symtab.table};
@@ -55,7 +55,7 @@
{default_qualifier =
if default_qualifier <> "" then default_qualifier
else #default_qualifier init_session_base,
- global_theories = Symtab.make_set global_theories,
+ global_theories = Symtab.make global_theories,
loaded_theories = Symtab.make (map (apsnd Path.explode) loaded_theories),
known_theories = Symtab.make (map (apsnd Path.explode) known_theories)});
@@ -65,7 +65,7 @@
fun get_session_base f = f (Synchronized.value global_session_base);
fun default_qualifier () = get_session_base #default_qualifier;
-fun global_theory a = Symtab.defined (get_session_base #global_theories) a;
+fun global_theory a = Symtab.lookup (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;
@@ -104,13 +104,15 @@
val thy_path = Path.ext "thy";
fun theory_qualifier theory =
- Long_Name.qualifier theory;
+ (case global_theory theory of
+ SOME qualifier => qualifier
+ | NONE => Long_Name.qualifier theory);
fun import_name qualifier dir s =
let
val theory0 = Thy_Header.import_name s;
val theory =
- if Long_Name.is_qualified theory0 orelse global_theory theory0
+ if Long_Name.is_qualified theory0 orelse is_some (global_theory theory0)
orelse true (* FIXME *) then theory0
else Long_Name.qualify qualifier theory0;
val node_name =
--- a/src/Pure/PIDE/resources.scala Mon Apr 10 13:30:55 2017 +0200
+++ b/src/Pure/PIDE/resources.scala Mon Apr 10 16:43:12 2017 +0200
@@ -68,13 +68,13 @@
else Nil
def theory_qualifier(name: Document.Node.Name): String =
- Long_Name.qualifier(name.theory)
+ session_base.global_theories.getOrElse(name.theory, Long_Name.qualifier(name.theory))
def import_name(qualifier: String, dir: String, s: String): Document.Node.Name =
{
val theory0 = Thy_Header.import_name(s)
val theory =
- if (Long_Name.is_qualified(theory0) || session_base.global_theories.contains(theory0)
+ if (Long_Name.is_qualified(theory0) || session_base.global_theories.isDefinedAt(theory0)
|| true /* FIXME */) theory0
else theory0 // FIXME Long_Name.qualify(qualifier, theory0)
--- a/src/Pure/Thy/sessions.scala Mon Apr 10 13:30:55 2017 +0200
+++ b/src/Pure/Thy/sessions.scala Mon Apr 10 16:43:12 2017 +0200
@@ -49,7 +49,7 @@
}
sealed case class Base(
- global_theories: Set[String] = Set.empty,
+ global_theories: Map[String, String] = Map.empty,
loaded_theories: Map[String, Document.Node.Name] = Map.empty,
known_theories: Map[String, Document.Node.Name] = Map.empty,
keywords: Thy_Header.Keywords = Nil,
@@ -85,7 +85,7 @@
verbose: Boolean = false,
list_files: Boolean = false,
check_keywords: Set[String] = Set.empty,
- global_theories: Set[String] = Set.empty): Deps =
+ global_theories: Map[String, String] = Map.empty): Deps =
{
Deps((Map.empty[String, Base] /: sessions.imports_topological_order)({
case (sessions, (session_name, info)) =>
@@ -98,7 +98,7 @@
case Some(parent) => sessions(parent)
}
val resources = new Resources(parent_base,
- default_qualifier = info.theory_qualifier getOrElse session_name)
+ default_qualifier = info.theory_qualifier(session_name))
if (verbose || list_files) {
val groups =
@@ -211,10 +211,10 @@
{
def timeout: Time = Time.seconds(options.real("timeout") * options.real("timeout_scale"))
- def theory_qualifier: Option[String] =
+ def theory_qualifier(default_qualifier: String): String =
options.string("theory_qualifier") match {
- case "" => None
- case qualifier => Some(qualifier)
+ case "" => default_qualifier
+ case qualifier => qualifier
}
}
@@ -324,17 +324,19 @@
def get(name: String): Option[Info] =
if (imports_graph.defined(name)) Some(imports_graph.get_node(name)) else None
- def global_theories: Set[String] =
- (Set.empty[String] /:
+ def global_theories: Map[String, String] =
+ (Map.empty[String, String] /:
(for {
- (_, (info, _)) <- imports_graph.iterator
- thy <- info.global_theories.iterator }
- yield (thy, info.pos)))(
- { case (set, (thy, pos)) =>
- if (set.contains(thy))
- error("Duplicate declaration of global theory " + quote(thy) + Position.here(pos))
- else set + thy
- })
+ (session_name, (info, _)) <- imports_graph.iterator
+ thy <- info.global_theories.iterator } yield (thy, session_name, info)))({
+ case (global, (thy, session_name, info)) =>
+ val qualifier = info.theory_qualifier(session_name)
+ global.get(thy) match {
+ case Some(qualifier1) if qualifier != qualifier1 =>
+ error("Duplicate global theory " + quote(thy) + Position.here(info.pos))
+ case _ => global + (thy -> qualifier)
+ }
+ })
def selection(select: Selection): (List[String], T) =
{
--- a/src/Pure/Tools/build.ML Mon Apr 10 13:30:55 2017 +0200
+++ b/src/Pure/Tools/build.ML Mon Apr 10 16:43:12 2017 +0200
@@ -146,7 +146,7 @@
name: string,
master_dir: Path.T,
theories: (Options.T * (string * Position.T) list) list,
- global_theories: string list,
+ global_theories: (string * string) list,
loaded_theories: (string * string) list,
known_theories: (string * string) list};
@@ -160,7 +160,7 @@
(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))))))
- (pair (list string)
+ (pair (list (pair string string))
(pair (list (pair string string)) (list (pair string string)))))))))))))))
(YXML.parse_body yxml);
in
--- a/src/Pure/Tools/build.scala Mon Apr 10 13:30:55 2017 +0200
+++ b/src/Pure/Tools/build.scala Mon Apr 10 16:43:12 2017 +0200
@@ -205,7 +205,7 @@
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))),
- pair(list(string),
+ pair(list(pair(string, 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),
@@ -224,8 +224,8 @@
ML_Syntax.print_string0(File.platform_path(output))
if (pide && !Sessions.is_pure(name)) {
- val resources = new Resources(deps(parent),
- default_qualifier = info.theory_qualifier getOrElse name)
+ val resources =
+ new Resources(deps(parent), default_qualifier = info.theory_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 Mon Apr 10 13:30:55 2017 +0200
+++ b/src/Pure/Tools/ml_process.scala Mon Apr 10 16:43:12 2017 +0200
@@ -100,8 +100,7 @@
ML_Syntax.print_pair(
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) +
+ ", global_theories = " + print_table(base.global_theories.toList) +
", loaded_theories = " + print_table(base.dest_loaded_theories) +
", known_theories = " + print_table(base.dest_known_theories) + "}")
}