# HG changeset patch
# User wenzelm
# Date 1491683792 -7200
# Node ID e9e7f5f5794ca1f84a9e84d7d15588efc667dfce
# Parent  1f5821b1974153e30878eaa857152cd0e16076ae
more qualifier treatment, but in the end it is still ignored;

diff -r 1f5821b19741 -r e9e7f5f5794c src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Sat Apr 08 21:35:04 2017 +0200
+++ b/src/Pure/PIDE/document.ML	Sat Apr 08 22:36:32 2017 +0200
@@ -177,9 +177,6 @@
     SOME eval => Command.eval_finished eval
   | NONE => false);
 
-fun loaded_theory name =
-  get_first Thy_Info.lookup_theory [name, Long_Name.base_name name];
-
 fun get_node nodes name = String_Graph.get_node nodes name
   handle String_Graph.UNDEF _ => empty_node;
 fun default_node name = String_Graph.default_node (name, empty_node);
@@ -463,7 +460,7 @@
       val delay_request' = Event_Timer.future (Time.now () + delay);
 
       fun finished_import (name, (node, _)) =
-        finished_result node orelse is_some (loaded_theory name);
+        finished_result node orelse is_some (Thy_Info.lookup_theory name);
 
       val nodes = nodes_of (the_version state version_id);
       val required = make_required nodes;
@@ -530,7 +527,7 @@
         handle ERROR msg => (Output.error_message msg; NONE);
     val parents_reports =
       imports |> map_filter (fn (import, pos) =>
-        (case loaded_theory import of
+        (case Thy_Info.lookup_theory import of
           NONE =>
             maybe_end_theory pos
               (case get_result (snd (the (AList.lookup (op =) deps import))) of
@@ -554,7 +551,7 @@
   else NONE;
 
 fun check_theory full name node =
-  is_some (loaded_theory name) orelse
+  is_some (Thy_Info.lookup_theory name) orelse
   null (#errors (get_header node)) andalso (not full orelse is_some (get_result node));
 
 fun last_common keywords state node_required node0 node =
diff -r 1f5821b19741 -r e9e7f5f5794c src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Sat Apr 08 21:35:04 2017 +0200
+++ b/src/Pure/PIDE/document.scala	Sat Apr 08 22:36:32 2017 +0200
@@ -117,7 +117,6 @@
       def loaded_theory: Name = Name(theory, "", theory)
       def is_theory: Boolean = theory.nonEmpty
 
-      def theory_qualifier: String = Long_Name.qualifier(theory)
       def theory_base_name: String = Long_Name.base_name(theory)
 
       override def toString: String = if (is_theory) theory else node
diff -r 1f5821b19741 -r e9e7f5f5794c src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Sat Apr 08 21:35:04 2017 +0200
+++ b/src/Pure/PIDE/protocol.scala	Sat Apr 08 22:36:32 2017 +0200
@@ -359,14 +359,13 @@
           { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) },
           { case Document.Node.Deps(header) =>
               val master_dir = File.standard_url(name.master_dir)
-              val theory = name.theory_base_name  // FIXME
               val imports = header.imports.map({ case (a, _) => a.node })
               val keywords =
                 header.keywords.map({ case (a, Keyword.Spec(b, c, d)) => (a, ((b, c), d)) })
               (Nil,
                 pair(string, pair(string, pair(list(string), pair(list(pair(string,
                     pair(pair(string, list(string)), list(string)))), list(string)))))(
-                (master_dir, (theory, (imports, (keywords, header.errors)))))) },
+                (master_dir, (name.theory, (imports, (keywords, header.errors)))))) },
           { case Document.Node.Perspective(a, b, c) =>
               (bool_atom(a) :: b.commands.map(cmd => long_atom(cmd.id)),
                 list(pair(id, pair(string, list(string))))(c.dest)) }))
diff -r 1f5821b19741 -r e9e7f5f5794c src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Sat Apr 08 21:35:04 2017 +0200
+++ b/src/Pure/PIDE/resources.ML	Sat Apr 08 22:36:32 2017 +0200
@@ -19,7 +19,8 @@
   val master_directory: theory -> Path.T
   val imports_of: theory -> (string * Position.T) list
   val thy_path: Path.T -> Path.T
-  val import_name: Path.T -> Path.T -> {node_name: Path.T, theory_name: string}
+  val theory_qualifier: string -> string
+  val import_name: string -> Path.T -> Path.T -> {node_name: Path.T, theory_name: string}
   val check_thy: Path.T -> string ->
    {master: Path.T * SHA1.digest, text: string, theory_pos: Position.T,
     imports: (string * Position.T) list, keywords: Thy_Header.keywords}
@@ -39,7 +40,7 @@
 (* session base *)
 
 val init_session_base =
-  {default_qualifier = "",
+  {default_qualifier = "Draft",
    global_theories = Symtab.make_set [],
    loaded_theories = Symtab.empty: Path.T Symtab.table,
    known_theories = Symtab.empty: Path.T Symtab.table};
@@ -50,7 +51,9 @@
 fun set_session_base {default_qualifier, global_theories, loaded_theories, known_theories} =
   Synchronized.change global_session_base
     (fn _ =>
-      {default_qualifier = default_qualifier,
+      {default_qualifier =
+        if default_qualifier <> "" then default_qualifier
+        else #default_qualifier init_session_base,
        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)});
@@ -99,12 +102,16 @@
 
 val thy_path = Path.ext "thy";
 
-fun import_name dir path =
+fun theory_qualifier theory =
+  Long_Name.qualifier theory;
+
+fun import_name qualifier dir path =
   let
     val theory0 = Path.implode (Path.base path);
     val theory =
-      if Long_Name.is_qualified theory0 orelse global_theory theory0 then theory0
-      else Long_Name.qualify (default_qualifier ()) theory0;
+      if Long_Name.is_qualified theory0 orelse global_theory theory0
+        orelse true (* FIXME *) then theory0
+      else Long_Name.qualify qualifier theory0;
     val node_name =
       the (get_first (fn e => e ())
         [fn () => loaded_theory theory,
diff -r 1f5821b19741 -r e9e7f5f5794c src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Sat Apr 08 21:35:04 2017 +0200
+++ b/src/Pure/PIDE/resources.scala	Sat Apr 08 22:36:32 2017 +0200
@@ -15,7 +15,7 @@
 
 class Resources(
   val session_base: Sessions.Base,
-  val default_qualifier: String = "",
+  val default_qualifier: String = Sessions.DRAFT,
   val log: Logger = No_Logger)
 {
   val thy_info = new Thy_Info(this)
@@ -67,12 +67,16 @@
     }
     else Nil
 
-  def import_name(dir: String, s: String): Document.Node.Name =
+  def theory_qualifier(name: Document.Node.Name): String =
+    Long_Name.qualifier(name.theory)
+
+  def import_name(qualifier: String, dir: String, s: String): Document.Node.Name =
   {
     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(default_qualifier, theory0)
+      if (Long_Name.is_qualified(theory0) || session_base.global_theories.contains(theory0)
+        || true /* FIXME */) theory0
+      else theory0 // FIXME Long_Name.qualify(qualifier, theory0)
 
     session_base.loaded_theories.get(theory) orElse
     session_base.loaded_theories.get(theory0) orElse
@@ -109,7 +113,8 @@
             Completion.report_names(pos, 1, List((base_name, ("theory", base_name)))))
 
         val imports =
-          header.imports.map({ case (s, pos) => (import_name(node_name.master_dir, s), pos) })
+          header.imports.map({ case (s, pos) =>
+            (import_name(theory_qualifier(node_name), node_name.master_dir, s), pos) })
         Document.Node.Header(imports, header.keywords, header.abbrevs)
       }
       catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) }
@@ -125,13 +130,20 @@
   /* special header */
 
   def special_header(name: Document.Node.Name): Option[Document.Node.Header] =
-    if (Thy_Header.is_ml_root(name.theory))
-      Some(Document.Node.Header(
-        List((import_name(name.master_dir, Thy_Header.ML_BOOTSTRAP), Position.none))))
-    else if (Thy_Header.is_bootstrap(name.theory))
-      Some(Document.Node.Header(
-        List((import_name(name.master_dir, Thy_Header.PURE), Position.none))))
-    else None
+  {
+    val qualifier = theory_qualifier(name)
+    val dir = name.master_dir
+
+    val imports =
+      if (Thy_Header.is_ml_root(name.theory))
+        List(import_name(qualifier, dir, Thy_Header.ML_BOOTSTRAP))
+      else if (Thy_Header.is_bootstrap(name.theory))
+        List(import_name(qualifier, dir, Thy_Header.PURE))
+      else Nil
+
+    if (imports.isEmpty) None
+    else Some(Document.Node.Header(imports.map((_, Position.none))))
+  }
 
 
   /* blobs */
diff -r 1f5821b19741 -r e9e7f5f5794c src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Sat Apr 08 21:35:04 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Sat Apr 08 22:36:32 2017 +0200
@@ -19,6 +19,8 @@
 {
   /* base info and source dependencies */
 
+  val DRAFT = "Draft"
+
   def is_pure(name: String): Boolean = name == Thy_Header.PURE
 
   object Base
@@ -108,7 +110,8 @@
           {
             val root_theories =
               info.theories.flatMap({ case (_, thys) =>
-                thys.map(thy => (resources.import_name(info.dir.implode, thy), info.pos))
+                thys.map(thy =>
+                  (resources.import_name(session_name, info.dir.implode, thy), info.pos))
               })
             val thy_deps = resources.thy_info.dependencies(root_theories)
 
@@ -450,7 +453,7 @@
         try {
           val name = entry.name
 
-          if (name == "") error("Bad session name")
+          if (name == "" || name == DRAFT) error("Bad session name")
           if (is_pure(name) && entry.parent.isDefined) error("Illegal parent session")
           if (!is_pure(name) && !entry.parent.isDefined) error("Missing parent session")
 
diff -r 1f5821b19741 -r e9e7f5f5794c src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Sat Apr 08 21:35:04 2017 +0200
+++ b/src/Pure/Thy/thy_info.ML	Sat Apr 08 22:36:32 2017 +0200
@@ -17,6 +17,7 @@
     {document: bool,
      symbols: HTML.symbols,
      last_timing: Toplevel.transition -> Time.time,
+     qualifier: string,
      master_dir: Path.T} -> (string * Position.T) list -> unit
   val use_thy: string -> unit
   val script_thy: Position.T -> string -> theory -> theory
@@ -285,12 +286,13 @@
 
 in
 
-fun require_thys document symbols last_timing initiators dir strs tasks =
-      fold_map (require_thy document symbols last_timing initiators dir) strs tasks |>> forall I
-and require_thy document symbols last_timing initiators dir (str, require_pos) tasks =
+fun require_thys document symbols last_timing initiators qualifier dir strs tasks =
+      fold_map (require_thy document symbols last_timing initiators qualifier dir) strs tasks
+      |>> forall I
+and require_thy document symbols last_timing initiators qualifier dir (str, require_pos) tasks =
   let
     val path = Path.expand (Path.explode str);
-    val {node_name, theory_name} = Resources.import_name dir path;
+    val {node_name, theory_name} = Resources.import_name qualifier dir path;
     fun check_entry (Task (node_name', _, _)) =
           if op = (apply2 File.platform_path (node_name, node_name'))
           then ()
@@ -317,6 +319,7 @@
           val parents = map (base_name o #1) imports;
           val (parents_current, tasks') =
             require_thys document symbols last_timing (theory_name :: initiators)
+              (Resources.theory_qualifier theory_name)
               (Path.append dir (master_dir (Option.map #1 deps))) imports tasks;
 
           val all_current = current andalso parents_current;
@@ -342,14 +345,16 @@
 
 (* use theories *)
 
-fun use_theories {document, symbols, last_timing, master_dir} imports =
-  schedule_tasks
-    (snd (require_thys document symbols last_timing [] master_dir imports String_Graph.empty));
+fun use_theories {document, symbols, last_timing, qualifier, master_dir} imports =
+  let
+    val (_, tasks) =
+      require_thys document symbols last_timing [] qualifier master_dir imports String_Graph.empty;
+  in schedule_tasks tasks end;
 
 fun use_thy name =
   use_theories
     {document = false, symbols = HTML.no_symbols, last_timing = K Time.zeroTime,
-      master_dir = Path.current}
+     qualifier = Resources.default_qualifier (), master_dir = Path.current}
     [(name, Position.none)];
 
 
diff -r 1f5821b19741 -r e9e7f5f5794c src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Sat Apr 08 21:35:04 2017 +0200
+++ b/src/Pure/Tools/build.ML	Sat Apr 08 22:36:32 2017 +0200
@@ -101,7 +101,7 @@
 
 (* build theories *)
 
-fun build_theories symbols last_timing master_dir (options, thys) =
+fun build_theories symbols last_timing qualifier master_dir (options, thys) =
   let
     val condition = space_explode "," (Options.string options "condition");
     val conds = filter_out (can getenv_strict) condition;
@@ -115,6 +115,7 @@
           document = Present.document_enabled (Options.string options "document"),
           symbols = symbols,
           last_timing = last_timing,
+          qualifier = qualifier,
           master_dir = master_dir}
         |>
           (case Options.string options "profiling" of
@@ -180,7 +181,7 @@
 
     val _ =
       Resources.set_session_base
-        {default_qualifier = "" (* FIXME *),
+        {default_qualifier = name,
          global_theories = global_theories,
          loaded_theories = loaded_theories,
          known_theories = known_theories};
@@ -204,7 +205,7 @@
 
     val res1 =
       theories |>
-        (List.app (build_theories symbols last_timing master_dir)
+        (List.app (build_theories symbols last_timing name master_dir)
           |> session_timing name verbose
           |> Exn.capture);
     val res2 = Exn.capture Session.finish ();