--- a/src/Pure/ML/ml_process.scala Fri Apr 21 13:51:43 2017 +0200
+++ b/src/Pure/ML/ml_process.scala Fri Apr 21 14:09:03 2017 +0200
@@ -99,8 +99,8 @@
ML_Syntax.print_list(
ML_Syntax.print_pair(
ML_Syntax.print_string, ML_Syntax.print_string))(table)
- List("Resources.init_session_base {default_qualifier = \"\"" +
- ", global_theories = " + print_table(base.global_theories.toList) +
+ List("Resources.init_session_base" +
+ " {global_theories = " + print_table(base.global_theories.toList) +
", loaded_theories = " + print_table(base.loaded_theories.toList) +
", known_theories = " + print_table(base.dest_known_theories) + "}")
}
--- a/src/Pure/PIDE/protocol.ML Fri Apr 21 13:51:43 2017 +0200
+++ b/src/Pure/PIDE/protocol.ML Fri Apr 21 14:09:03 2017 +0200
@@ -19,13 +19,12 @@
val _ =
Isabelle_Process.protocol_command "Prover.session_base"
- (fn [default_qualifier, global_theories_yxml, loaded_theories_yxml, known_theories_yxml] =>
+ (fn [global_theories_yxml, loaded_theories_yxml, known_theories_yxml] =>
let
val decode_table = YXML.parse_body #> let open XML.Decode in list (pair string string) end;
in
Resources.init_session_base
- {default_qualifier = default_qualifier,
- global_theories = decode_table global_theories_yxml,
+ {global_theories = decode_table global_theories_yxml,
loaded_theories = decode_table loaded_theories_yxml,
known_theories = decode_table known_theories_yxml}
end);
--- a/src/Pure/PIDE/protocol.scala Fri Apr 21 13:51:43 2017 +0200
+++ b/src/Pure/PIDE/protocol.scala Fri Apr 21 14:09:03 2017 +0200
@@ -312,7 +312,6 @@
def session_base(resources: Resources): Unit =
protocol_command("Prover.session_base",
- Symbol.encode(resources.default_qualifier),
encode_table(resources.session_base.global_theories.toList),
encode_table(resources.session_base.loaded_theories.toList),
encode_table(resources.session_base.dest_known_theories))
--- a/src/Pure/PIDE/resources.ML Fri Apr 21 13:51:43 2017 +0200
+++ b/src/Pure/PIDE/resources.ML Fri Apr 21 14:09:03 2017 +0200
@@ -6,13 +6,12 @@
signature RESOURCES =
sig
+ val default_qualifier: string
val init_session_base:
- {default_qualifier: string,
- global_theories: (string * string) list,
+ {global_theories: (string * string) list,
loaded_theories: (string * string) list,
known_theories: (string * string) list} -> unit
val finish_session_base: unit -> unit
- val default_qualifier: unit -> string
val global_theory: string -> string option
val loaded_theory: string -> string option
val known_theory: string -> Path.T option
@@ -37,36 +36,32 @@
(* session base *)
+val default_qualifier = "Draft";
+
val empty_session_base =
- {default_qualifier = "Draft",
- global_theories = Symtab.empty: string Symtab.table,
+ {global_theories = Symtab.empty: string Symtab.table,
loaded_theories = Symtab.empty: string Symtab.table,
known_theories = Symtab.empty: Path.T Symtab.table};
val global_session_base =
Synchronized.var "Sessions.base" empty_session_base;
-fun init_session_base {default_qualifier, global_theories, loaded_theories, known_theories} =
+fun init_session_base {global_theories, loaded_theories, known_theories} =
Synchronized.change global_session_base
(fn _ =>
- {default_qualifier =
- if default_qualifier <> "" then default_qualifier
- else #default_qualifier empty_session_base,
- global_theories = Symtab.make global_theories,
+ {global_theories = Symtab.make global_theories,
loaded_theories = Symtab.make loaded_theories,
known_theories = Symtab.make (map (apsnd Path.explode) known_theories)});
fun finish_session_base () =
Synchronized.change global_session_base
(fn {global_theories, loaded_theories, ...} =>
- {default_qualifier = #default_qualifier empty_session_base,
- global_theories = global_theories,
+ {global_theories = global_theories,
loaded_theories = loaded_theories,
known_theories = #known_theories empty_session_base});
fun get_session_base f = f (Synchronized.value global_session_base);
-fun default_qualifier () = get_session_base #default_qualifier;
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;
--- a/src/Pure/PIDE/resources.scala Fri Apr 21 13:51:43 2017 +0200
+++ b/src/Pure/PIDE/resources.scala Fri Apr 21 14:09:03 2017 +0200
@@ -15,7 +15,6 @@
class Resources(
val session_base: Sessions.Base,
- val default_qualifier: String = Sessions.DRAFT,
val log: Logger = No_Logger)
{
val thy_info = new Thy_Info(this)
--- a/src/Pure/Thy/sessions.scala Fri Apr 21 13:51:43 2017 +0200
+++ b/src/Pure/Thy/sessions.scala Fri Apr 21 14:09:03 2017 +0200
@@ -150,7 +150,7 @@
parent_base.copy(known =
Known.make(info.dir, parent_base :: info.imports.map(session_bases(_)), Nil))
- val resources = new Resources(imports_base, default_qualifier = info.theory_qualifier)
+ val resources = new Resources(imports_base)
if (verbose || list_files) {
val groups =
--- a/src/Pure/Thy/thy_info.ML Fri Apr 21 13:51:43 2017 +0200
+++ b/src/Pure/Thy/thy_info.ML Fri Apr 21 14:09:03 2017 +0200
@@ -408,7 +408,7 @@
fun use_thy name =
use_theories
{document = false, symbols = HTML.no_symbols, last_timing = K Time.zeroTime,
- qualifier = Resources.default_qualifier (), master_dir = Path.current}
+ qualifier = Resources.default_qualifier, master_dir = Path.current}
[(name, Position.none)];
--- a/src/Pure/Tools/build.ML Fri Apr 21 13:51:43 2017 +0200
+++ b/src/Pure/Tools/build.ML Fri Apr 21 14:09:03 2017 +0200
@@ -182,8 +182,7 @@
val _ =
Resources.init_session_base
- {default_qualifier = name,
- global_theories = global_theories,
+ {global_theories = global_theories,
loaded_theories = loaded_theories,
known_theories = known_theories};
--- a/src/Pure/Tools/build.scala Fri Apr 21 13:51:43 2017 +0200
+++ b/src/Pure/Tools/build.scala Fri Apr 21 14:09:03 2017 +0200
@@ -223,7 +223,7 @@
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)
+ val resources = new Resources(deps(parent))
val session = new Session(options, resources)
val handler = new Handler(progress, session, name)
session.init_protocol_handler(handler)
--- a/src/Pure/Tools/update_imports.scala Fri Apr 21 13:51:43 2017 +0200
+++ b/src/Pure/Tools/update_imports.scala Fri Apr 21 14:09:03 2017 +0200
@@ -68,7 +68,7 @@
{
val info = full_sessions(session_name)
val session_base = deps(session_name)
- val resources = new Resources(session_base, default_qualifier = info.theory_qualifier)
+ val resources = new Resources(session_base)
val local_theories = session_base.known.theories_local.iterator.map(_._2).toSet
def standard_import(qualifier: String, s: String): String =
--- a/src/Tools/VSCode/src/vscode_resources.scala Fri Apr 21 13:51:43 2017 +0200
+++ b/src/Tools/VSCode/src/vscode_resources.scala Fri Apr 21 14:09:03 2017 +0200
@@ -63,7 +63,7 @@
def node_name(file: JFile): Document.Node.Name =
session_base.known.get_file(file) getOrElse {
val node = file.getPath
- theory_name(default_qualifier, Thy_Header.theory_name(node)) match {
+ theory_name(Sessions.DRAFT, Thy_Header.theory_name(node)) match {
case (true, theory) => Document.Node.Name.loaded_theory(theory)
case (false, theory) =>
val master_dir = if (theory == "") "" else file.getParent
--- a/src/Tools/jEdit/src/jedit_resources.scala Fri Apr 21 13:51:43 2017 +0200
+++ b/src/Tools/jEdit/src/jedit_resources.scala Fri Apr 21 14:09:03 2017 +0200
@@ -32,7 +32,7 @@
known_file(path) getOrElse {
val vfs = VFSManager.getVFSForPath(path)
val node = if (vfs.isInstanceOf[FileVFS]) MiscUtilities.resolveSymlinks(path) else path
- theory_name(default_qualifier, Thy_Header.theory_name(node)) match {
+ theory_name(Sessions.DRAFT, Thy_Header.theory_name(node)) match {
case (true, theory) => Document.Node.Name.loaded_theory(theory)
case (false, theory) =>
val master_dir = if (theory == "") "" else vfs.getParentOfPath(path)