# 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)