explicit theory qualifier for session "HOL-Proofs": its theory name space overlaps with session "HOL", even for further imports;
authorwenzelm
Mon Apr 10 13:30:55 2017 +0200 (2017-04-10)
changeset 6545631e8a86971a8
parent 65455 ff09d29498b0
child 65457 2bf0d2fcd506
explicit theory qualifier for session "HOL-Proofs": its theory name space overlaps with session "HOL", even for further imports;
etc/options
src/HOL/ROOT
src/Pure/Thy/sessions.scala
src/Pure/Tools/build.scala
     1.1 --- a/etc/options	Mon Apr 10 13:19:24 2017 +0200
     1.2 +++ b/etc/options	Mon Apr 10 13:30:55 2017 +0200
     1.3 @@ -113,6 +113,9 @@
     1.4  option profiling : string = ""
     1.5    -- "ML profiling (possible values: time, allocations)"
     1.6  
     1.7 +option theory_qualifier : string = ""
     1.8 +  -- "explicit theory qualifier for special sessions (default: session name)"
     1.9 +
    1.10  
    1.11  section "ML System"
    1.12  
     2.1 --- a/src/HOL/ROOT	Mon Apr 10 13:19:24 2017 +0200
     2.2 +++ b/src/HOL/ROOT	Mon Apr 10 13:30:55 2017 +0200
     2.3 @@ -18,7 +18,8 @@
     2.4    description {*
     2.5      HOL-Main with explicit proof terms.
     2.6    *}
     2.7 -  options [document = false, quick_and_dirty = false, record_proofs = 2, parallel_proofs = 0]
     2.8 +  options [document = false, theory_qualifier = "HOL",
     2.9 +    quick_and_dirty = false, record_proofs = 2, parallel_proofs = 0]
    2.10    theories "~~/src/HOL/Library/Old_Datatype"
    2.11    files
    2.12      "Tools/Quickcheck/Narrowing_Engine.hs"
     3.1 --- a/src/Pure/Thy/sessions.scala	Mon Apr 10 13:19:24 2017 +0200
     3.2 +++ b/src/Pure/Thy/sessions.scala	Mon Apr 10 13:30:55 2017 +0200
     3.3 @@ -97,7 +97,8 @@
     3.4                case None => Base.bootstrap
     3.5                case Some(parent) => sessions(parent)
     3.6              }
     3.7 -          val resources = new Resources(parent_base, default_qualifier = session_name)
     3.8 +          val resources = new Resources(parent_base,
     3.9 +            default_qualifier = info.theory_qualifier getOrElse session_name)
    3.10  
    3.11            if (verbose || list_files) {
    3.12              val groups =
    3.13 @@ -209,6 +210,12 @@
    3.14      meta_digest: SHA1.Digest)
    3.15    {
    3.16      def timeout: Time = Time.seconds(options.real("timeout") * options.real("timeout_scale"))
    3.17 +
    3.18 +    def theory_qualifier: Option[String] =
    3.19 +      options.string("theory_qualifier") match {
    3.20 +        case "" => None
    3.21 +        case qualifier => Some(qualifier)
    3.22 +      }
    3.23    }
    3.24  
    3.25    object Selection
     4.1 --- a/src/Pure/Tools/build.scala	Mon Apr 10 13:19:24 2017 +0200
     4.2 +++ b/src/Pure/Tools/build.scala	Mon Apr 10 13:30:55 2017 +0200
     4.3 @@ -224,7 +224,8 @@
     4.4              ML_Syntax.print_string0(File.platform_path(output))
     4.5  
     4.6          if (pide && !Sessions.is_pure(name)) {
     4.7 -          val resources = new Resources(deps(parent), default_qualifier = name)
     4.8 +          val resources = new Resources(deps(parent),
     4.9 +            default_qualifier = info.theory_qualifier getOrElse name)
    4.10            val session = new Session(options, resources)
    4.11            val handler = new Handler(progress, session, name)
    4.12            session.init_protocol_handler(handler)