# HG changeset patch
# User wenzelm
# Date 1506604292 -7200
# Node ID 4c98c929a12a0aae8787e7fa2872192ca4a58e33
# Parent  80fa1401cf76ba1f14c2144253b8485f1bb7e277
session-qualified theory names are mandatory;

diff -r 80fa1401cf76 -r 4c98c929a12a NEWS
--- a/NEWS	Thu Sep 28 11:53:55 2017 +0200
+++ b/NEWS	Thu Sep 28 15:11:32 2017 +0200
@@ -7,6 +7,14 @@
 New in this Isabelle version
 ----------------------------
 
+*** General ***
+
+* Session-qualified theory names are mandatory: it is no longer possible
+to refer to unqualified theories from the parent session.
+INCOMPATIBILITY for old developments that have not been updated to
+Isabelle2017 yet (using the "isabelle imports" tool).
+
+
 *** HOL ***
 
 * SMT module:
diff -r 80fa1401cf76 -r 4c98c929a12a src/Pure/ML/ml_process.scala
--- a/src/Pure/ML/ml_process.scala	Thu Sep 28 11:53:55 2017 +0200
+++ b/src/Pure/ML/ml_process.scala	Thu Sep 28 15:11:32 2017 +0200
@@ -99,9 +99,11 @@
             ML_Syntax.print_list(
               ML_Syntax.print_pair(
                 ML_Syntax.print_string, ML_Syntax.print_string))(table)
+          def print_list(list: List[String]): String =
+            ML_Syntax.print_list(ML_Syntax.print_string)(list)
           List("Resources.init_session_base" +
             " {global_theories = " + print_table(base.global_theories.toList) +
-            ", loaded_theories = " + print_table(base.loaded_theories.toList) +
+            ", loaded_theories = " + print_list(base.loaded_theories.toList) +
             ", known_theories = " + print_table(base.dest_known_theories) + "}")
       }
 
diff -r 80fa1401cf76 -r 4c98c929a12a src/Pure/PIDE/protocol.ML
--- a/src/Pure/PIDE/protocol.ML	Thu Sep 28 11:53:55 2017 +0200
+++ b/src/Pure/PIDE/protocol.ML	Thu Sep 28 15:11:32 2017 +0200
@@ -22,10 +22,11 @@
     (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;
+        val decode_list = YXML.parse_body #> let open XML.Decode in list string end;
       in
         Resources.init_session_base
           {global_theories = decode_table global_theories_yxml,
-           loaded_theories = decode_table loaded_theories_yxml,
+           loaded_theories = decode_list loaded_theories_yxml,
            known_theories = decode_table known_theories_yxml}
       end);
 
diff -r 80fa1401cf76 -r 4c98c929a12a src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Thu Sep 28 11:53:55 2017 +0200
+++ b/src/Pure/PIDE/protocol.scala	Thu Sep 28 15:11:32 2017 +0200
@@ -316,12 +316,18 @@
     Symbol.encode_yxml(list(pair(string, string))(table))
   }
 
+  private def encode_list(lst: List[String]): String =
+  {
+    import XML.Encode._
+    Symbol.encode_yxml(list(string)(lst))
+  }
+
   def session_base(resources: Resources)
   {
     val base = resources.session_base.standard_path
     protocol_command("Prover.session_base",
       encode_table(base.global_theories.toList),
-      encode_table(base.loaded_theories.toList),
+      encode_list(base.loaded_theories.toList),
       encode_table(base.dest_known_theories))
   }
 
diff -r 80fa1401cf76 -r 4c98c929a12a src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Thu Sep 28 11:53:55 2017 +0200
+++ b/src/Pure/PIDE/resources.ML	Thu Sep 28 15:11:32 2017 +0200
@@ -9,11 +9,11 @@
   val default_qualifier: string
   val init_session_base:
     {global_theories: (string * string) list,
-     loaded_theories: (string * string) list,
+     loaded_theories: string list,
      known_theories: (string * string) list} -> unit
   val finish_session_base: unit -> unit
   val global_theory: string -> string option
-  val loaded_theory: string -> string option
+  val loaded_theory: string -> bool
   val known_theory: string -> Path.T option
   val master_directory: theory -> Path.T
   val imports_of: theory -> (string * Position.T) list
@@ -39,7 +39,7 @@
 
 val empty_session_base =
   {global_theories = Symtab.empty: string Symtab.table,
-   loaded_theories = Symtab.empty: string Symtab.table,
+   loaded_theories = Symtab.empty: unit Symtab.table,
    known_theories = Symtab.empty: Path.T Symtab.table};
 
 val global_session_base =
@@ -49,7 +49,7 @@
   Synchronized.change global_session_base
     (fn _ =>
       {global_theories = Symtab.make global_theories,
-       loaded_theories = Symtab.make loaded_theories,
+       loaded_theories = Symtab.make_set loaded_theories,
        known_theories = Symtab.make (map (apsnd Path.explode) known_theories)});
 
 fun finish_session_base () =
@@ -62,7 +62,7 @@
 fun get_session_base f = f (Synchronized.value global_session_base);
 
 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 loaded_theory a = Symtab.defined (get_session_base #loaded_theories) a;
 fun known_theory a = Symtab.lookup (get_session_base #known_theories) a;
 
 
@@ -107,15 +107,14 @@
     SOME qualifier => qualifier
   | NONE => Long_Name.qualifier theory);
 
-fun theory_name qualifier theory0 =
-  (case loaded_theory theory0 of
-    SOME theory => (true, theory)
-  | NONE =>
-      let val theory =
-        if Long_Name.is_qualified theory0 orelse is_some (global_theory theory0)
-        then theory0
-        else Long_Name.qualify qualifier theory0
-      in (false, theory) end);
+fun theory_name qualifier theory =
+  if loaded_theory theory then (true, theory)
+  else
+    let val theory' =
+      if Long_Name.is_qualified theory orelse is_some (global_theory theory)
+      then theory
+      else Long_Name.qualify qualifier theory
+    in (false, theory') end;
 
 fun import_name qualifier dir s =
   (case theory_name qualifier (Thy_Header.import_name s) of
diff -r 80fa1401cf76 -r 4c98c929a12a src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Thu Sep 28 11:53:55 2017 +0200
+++ b/src/Pure/PIDE/resources.scala	Thu Sep 28 15:11:32 2017 +0200
@@ -88,15 +88,14 @@
   def theory_qualifier(name: Document.Node.Name): String =
     session_base.global_theories.getOrElse(name.theory, Long_Name.qualifier(name.theory))
 
-  def theory_name(qualifier: String, theory0: String): (Boolean, String) =
-    session_base.loaded_theories.get(theory0) match {
-      case Some(theory) => (true, theory)
-      case None =>
-        val theory =
-          if (Long_Name.is_qualified(theory0) || session_base.global_theories.isDefinedAt(theory0))
-            theory0
-          else Long_Name.qualify(qualifier, theory0)
-        (false, theory)
+  def theory_name(qualifier: String, theory: String): (Boolean, String) =
+    if (session_base.loaded_theory(theory)) (true, theory)
+    else {
+      val theory1 =
+        if (Long_Name.is_qualified(theory) || session_base.global_theories.isDefinedAt(theory))
+          theory
+        else Long_Name.qualify(qualifier, theory)
+      (false, theory1)
     }
 
   def import_name(qualifier: String, dir: String, s: String): Document.Node.Name =
diff -r 80fa1401cf76 -r 4c98c929a12a src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Thu Sep 28 11:53:55 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Thu Sep 28 15:11:32 2017 +0200
@@ -115,7 +115,7 @@
   sealed case class Base(
     pos: Position.T = Position.none,
     global_theories: Map[String, String] = Map.empty,
-    loaded_theories: Map[String, String] = Map.empty,
+    loaded_theories: Set[String] = Set.empty,
     known: Known = Known.empty,
     keywords: Thy_Header.Keywords = Nil,
     syntax: Outer_Syntax = Outer_Syntax.empty,
@@ -127,8 +127,8 @@
     def platform_path: Base = copy(known = known.platform_path)
     def standard_path: Base = copy(known = known.standard_path)
 
-    def loaded_theory(name: Document.Node.Name): Boolean =
-      loaded_theories.isDefinedAt(name.theory)
+    def loaded_theory(name: String): Boolean = loaded_theories.contains(name)
+    def loaded_theory(name: Document.Node.Name): Boolean = loaded_theory(name.theory)
 
     def known_theory(name: String): Option[Document.Node.Name] =
       known.theories.get(name)
diff -r 80fa1401cf76 -r 4c98c929a12a src/Pure/Thy/thy_info.scala
--- a/src/Pure/Thy/thy_info.scala	Thu Sep 28 11:53:55 2017 +0200
+++ b/src/Pure/Thy/thy_info.scala	Thu Sep 28 15:11:32 2017 +0200
@@ -61,13 +61,8 @@
     lazy val syntax: Outer_Syntax =
       resources.session_base.syntax.add_keywords(keywords).add_abbrevs(abbrevs)
 
-    def loaded_theories: Map[String, String] =
-      (resources.session_base.loaded_theories /: rev_deps) {
-        case (loaded, dep) =>
-          val name = dep.name
-          loaded + (name.theory -> name.theory) +
-            (name.theory_base_name -> name.theory)  // legacy
-      }
+    def loaded_theories: Set[String] =
+      resources.session_base.loaded_theories ++ rev_deps.map(dep => dep.name.theory)
 
     def loaded_files: List[(String, List[Path])] =
     {
diff -r 80fa1401cf76 -r 4c98c929a12a src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Thu Sep 28 11:53:55 2017 +0200
+++ b/src/Pure/Tools/build.ML	Thu Sep 28 15:11:32 2017 +0200
@@ -147,7 +147,7 @@
   master_dir: Path.T,
   theories: (Options.T * (string * Position.T) list) list,
   global_theories: (string * string) list,
-  loaded_theories: (string * string) list,
+  loaded_theories: string list,
   known_theories: (string * string) list};
 
 fun decode_args yxml =
@@ -162,7 +162,7 @@
           (pair string
             (pair (((list (pair Options.decode (list (pair string position))))))
               (pair (list (pair string string))
-                (pair (list (pair string string)) (list (pair string string)))))))))))))))
+                (pair (list string) (list (pair string string)))))))))))))))
       (YXML.parse_body yxml);
   in
     Args {symbol_codes = symbol_codes, command_timings = command_timings, do_output = do_output,
diff -r 80fa1401cf76 -r 4c98c929a12a src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Thu Sep 28 11:53:55 2017 +0200
+++ b/src/Pure/Tools/build.scala	Thu Sep 28 15:11:32 2017 +0200
@@ -209,7 +209,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(pair(string, properties)))),
-                pair(list(pair(string, string)), pair(list(pair(string, string)),
+                pair(list(pair(string, string)), pair(list(string),
                 list(pair(string, string))))))))))))))))(
               (Symbol.codes, (command_timings, (do_output, (verbose,
                 (store.browser_info, (info.document_files, (File.standard_path(graph_file),