# HG changeset patch
# User wenzelm
# Date 1507401061 -7200
# Node ID bf54ca580bf2bf464222eec3fa9ea2d66c466b36
# Parent  8645d56f96e16b9c21f793a260cec95c754b61b5
theory qualifier is always session name (see also 31e8a86971a8);

diff -r 8645d56f96e1 -r bf54ca580bf2 etc/options
--- a/etc/options	Sat Oct 07 20:20:03 2017 +0200
+++ b/etc/options	Sat Oct 07 20:31:01 2017 +0200
@@ -113,9 +113,6 @@
 option profiling : string = ""
   -- "ML profiling (possible values: time, allocations)"
 
-option theory_qualifier : string = ""
-  -- "explicit theory qualifier for special sessions (default: session name)"
-
 
 section "ML System"
 
diff -r 8645d56f96e1 -r bf54ca580bf2 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Sat Oct 07 20:20:03 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Sat Oct 07 20:31:01 2017 +0200
@@ -224,7 +224,7 @@
             val thy_deps =
               resources.thy_info.dependencies(
                 for { (_, thys) <- info.theories; (thy, pos) <- thys }
-                yield (resources.import_name(info.theory_qualifier, info.dir.implode, thy), pos))
+                yield (resources.import_name(info.name, info.dir.implode, thy), pos))
 
             val overall_syntax = thy_deps.overall_syntax
 
@@ -261,7 +261,7 @@
               def node(name: Document.Node.Name): Graph_Display.Node =
               {
                 val qualifier = resources.theory_qualifier(name)
-                if (qualifier == info.theory_qualifier)
+                if (qualifier == info.name)
                   Graph_Display.Node(name.theory_base_name, "theory." + name.theory)
                 else session_node(qualifier)
               }
@@ -370,12 +370,6 @@
     meta_digest: SHA1.Digest)
   {
     def timeout: Time = Time.seconds(options.real("timeout") * options.real("timeout_scale"))
-
-    def theory_qualifier: String =
-      options.string("theory_qualifier") match {
-        case "" => name
-        case qualifier => qualifier
-      }
   }
 
   object Selection
@@ -496,7 +490,7 @@
           thy <- info.global_theories.iterator }
          yield (thy, info)))({
             case (global, (thy, info)) =>
-              val qualifier = info.theory_qualifier
+              val qualifier = info.name
               global.get(thy) match {
                 case Some(qualifier1) if qualifier != qualifier1 =>
                   error("Duplicate global theory " + quote(thy) + Position.here(info.pos))
diff -r 8645d56f96e1 -r bf54ca580bf2 src/Pure/Tools/imports.scala
--- a/src/Pure/Tools/imports.scala	Sat Oct 07 20:20:03 2017 +0200
+++ b/src/Pure/Tools/imports.scala	Sat Oct 07 20:31:01 2017 +0200
@@ -104,7 +104,7 @@
         val extra_imports =
           (for {
             (_, a) <- session_resources.session_base.known.theories.iterator
-            if session_resources.theory_qualifier(a) == info.theory_qualifier
+            if session_resources.theory_qualifier(a) == info.name
             b <- deps.all_known.get_file(a.path.file)
             qualifier = session_resources.theory_qualifier(b)
             if !declared_imports.contains(qualifier)
@@ -146,14 +146,13 @@
           val updates_root =
             for {
               (_, pos) <- info.theories.flatMap(_._2)
-              upd <- update_name(root_keywords, pos,
-                standard_import(info.theory_qualifier, info.dir.implode, _))
+              upd <- update_name(root_keywords, pos, standard_import(info.name, info.dir.implode, _))
             } yield upd
 
           val updates_theories =
             for {
               (_, name) <- session_base.known.theories_local.toList
-              if session_resources.theory_qualifier(name) == info.theory_qualifier
+              if session_resources.theory_qualifier(name) == info.name
               (_, pos) <- session_resources.check_thy(name, Token.Pos.file(name.node)).imports
               upd <- update_name(session_base.overall_syntax.keywords, pos,
                 standard_import(session_resources.theory_qualifier(name), name.master_dir, _))