# HG changeset patch
# User wenzelm
# Date 1491823855 -7200
# Node ID 31e8a86971a88bd11ebfd3010e9bd6aae4f25986
# Parent  ff09d29498b0922b7d56486c9304bf6a5d9ebe1d
explicit theory qualifier for session "HOL-Proofs": its theory name space overlaps with session "HOL", even for further imports;

diff -r ff09d29498b0 -r 31e8a86971a8 etc/options
--- a/etc/options	Mon Apr 10 13:19:24 2017 +0200
+++ b/etc/options	Mon Apr 10 13:30:55 2017 +0200
@@ -113,6 +113,9 @@
 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 ff09d29498b0 -r 31e8a86971a8 src/HOL/ROOT
--- a/src/HOL/ROOT	Mon Apr 10 13:19:24 2017 +0200
+++ b/src/HOL/ROOT	Mon Apr 10 13:30:55 2017 +0200
@@ -18,7 +18,8 @@
   description {*
     HOL-Main with explicit proof terms.
   *}
-  options [document = false, quick_and_dirty = false, record_proofs = 2, parallel_proofs = 0]
+  options [document = false, theory_qualifier = "HOL",
+    quick_and_dirty = false, record_proofs = 2, parallel_proofs = 0]
   theories "~~/src/HOL/Library/Old_Datatype"
   files
     "Tools/Quickcheck/Narrowing_Engine.hs"
diff -r ff09d29498b0 -r 31e8a86971a8 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Mon Apr 10 13:19:24 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Mon Apr 10 13:30:55 2017 +0200
@@ -97,7 +97,8 @@
               case None => Base.bootstrap
               case Some(parent) => sessions(parent)
             }
-          val resources = new Resources(parent_base, default_qualifier = session_name)
+          val resources = new Resources(parent_base,
+            default_qualifier = info.theory_qualifier getOrElse session_name)
 
           if (verbose || list_files) {
             val groups =
@@ -209,6 +210,12 @@
     meta_digest: SHA1.Digest)
   {
     def timeout: Time = Time.seconds(options.real("timeout") * options.real("timeout_scale"))
+
+    def theory_qualifier: Option[String] =
+      options.string("theory_qualifier") match {
+        case "" => None
+        case qualifier => Some(qualifier)
+      }
   }
 
   object Selection
diff -r ff09d29498b0 -r 31e8a86971a8 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Mon Apr 10 13:19:24 2017 +0200
+++ b/src/Pure/Tools/build.scala	Mon Apr 10 13:30:55 2017 +0200
@@ -224,7 +224,8 @@
             ML_Syntax.print_string0(File.platform_path(output))
 
         if (pide && !Sessions.is_pure(name)) {
-          val resources = new Resources(deps(parent), default_qualifier = name)
+          val resources = new Resources(deps(parent),
+            default_qualifier = info.theory_qualifier getOrElse name)
           val session = new Session(options, resources)
           val handler = new Handler(progress, session, name)
           session.init_protocol_handler(handler)