# HG changeset patch
# User wenzelm
# Date 1492776543 -7200
# Node ID febfd9f78bd408c617dd90d1c3a05d52e1ac2be7
# Parent  24544e3f183d31a57c01e72ee65ac45a1cc96125
eliminated default_qualifier: just a constant;

diff -r 24544e3f183d -r febfd9f78bd4 src/Pure/ML/ml_process.scala
--- 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) + "}")
       }
diff -r 24544e3f183d -r febfd9f78bd4 src/Pure/PIDE/protocol.ML
--- 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);
diff -r 24544e3f183d -r febfd9f78bd4 src/Pure/PIDE/protocol.scala
--- 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))
diff -r 24544e3f183d -r febfd9f78bd4 src/Pure/PIDE/resources.ML
--- 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;
diff -r 24544e3f183d -r febfd9f78bd4 src/Pure/PIDE/resources.scala
--- 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)
diff -r 24544e3f183d -r febfd9f78bd4 src/Pure/Thy/sessions.scala
--- 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 =
diff -r 24544e3f183d -r febfd9f78bd4 src/Pure/Thy/thy_info.ML
--- 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)];
 
 
diff -r 24544e3f183d -r febfd9f78bd4 src/Pure/Tools/build.ML
--- 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};
 
diff -r 24544e3f183d -r febfd9f78bd4 src/Pure/Tools/build.scala
--- 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)
diff -r 24544e3f183d -r febfd9f78bd4 src/Pure/Tools/update_imports.scala
--- 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 =
diff -r 24544e3f183d -r febfd9f78bd4 src/Tools/VSCode/src/vscode_resources.scala
--- 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
diff -r 24544e3f183d -r febfd9f78bd4 src/Tools/jEdit/src/jedit_resources.scala
--- 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)