clarified;
authorwenzelm
Thu Apr 20 10:35:00 2017 +0200 (2017-04-20)
changeset 65520f47bc12b6e8a
parent 65519 d244d8f8e13f
child 65521 e307a781416a
clarified;
src/Pure/Thy/sessions.scala
src/Pure/Tools/build.scala
     1.1 --- a/src/Pure/Thy/sessions.scala	Thu Apr 20 10:30:30 2017 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Thu Apr 20 10:35:00 2017 +0200
     1.3 @@ -150,8 +150,7 @@
     1.4                parent_base.copy(known =
     1.5                  Known.make(info.dir, parent_base :: info.imports.map(session_bases(_)), Nil))
     1.6  
     1.7 -            val resources = new Resources(imports_base,
     1.8 -              default_qualifier = info.theory_qualifier(info.name))
     1.9 +            val resources = new Resources(imports_base, default_qualifier = info.theory_qualifier)
    1.10  
    1.11              if (verbose || list_files) {
    1.12                val groups =
    1.13 @@ -301,9 +300,9 @@
    1.14    {
    1.15      def timeout: Time = Time.seconds(options.real("timeout") * options.real("timeout_scale"))
    1.16  
    1.17 -    def theory_qualifier(default_qualifier: String): String =
    1.18 +    def theory_qualifier: String =
    1.19        options.string("theory_qualifier") match {
    1.20 -        case "" => default_qualifier
    1.21 +        case "" => name
    1.22          case qualifier => qualifier
    1.23        }
    1.24    }
    1.25 @@ -421,7 +420,7 @@
    1.26            thy <- info.global_theories.iterator }
    1.27           yield (thy, info)))({
    1.28              case (global, (thy, info)) =>
    1.29 -              val qualifier = info.theory_qualifier(info.name)
    1.30 +              val qualifier = info.theory_qualifier
    1.31                global.get(thy) match {
    1.32                  case Some(qualifier1) if qualifier != qualifier1 =>
    1.33                    error("Duplicate global theory " + quote(thy) + Position.here(info.pos))
     2.1 --- a/src/Pure/Tools/build.scala	Thu Apr 20 10:30:30 2017 +0200
     2.2 +++ b/src/Pure/Tools/build.scala	Thu Apr 20 10:35:00 2017 +0200
     2.3 @@ -223,8 +223,7 @@
     2.4              ML_Syntax.print_string0(File.platform_path(output))
     2.5  
     2.6          if (pide && !Sessions.is_pure(name)) {
     2.7 -          val resources =
     2.8 -            new Resources(deps(parent), default_qualifier = info.theory_qualifier(name))
     2.9 +          val resources = new Resources(deps(parent), default_qualifier = info.theory_qualifier)
    2.10            val session = new Session(options, resources)
    2.11            val handler = new Handler(progress, session, name)
    2.12            session.init_protocol_handler(handler)