src/Pure/Thy/sessions.scala
changeset 66780 bf54ca580bf2
parent 66770 122df1fde073
child 66818 5bc903a60932
     1.1 --- a/src/Pure/Thy/sessions.scala	Fri Oct 06 17:13:57 2017 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Sat Oct 07 20:31:01 2017 +0200
     1.3 @@ -224,7 +224,7 @@
     1.4              val thy_deps =
     1.5                resources.thy_info.dependencies(
     1.6                  for { (_, thys) <- info.theories; (thy, pos) <- thys }
     1.7 -                yield (resources.import_name(info.theory_qualifier, info.dir.implode, thy), pos))
     1.8 +                yield (resources.import_name(info.name, info.dir.implode, thy), pos))
     1.9  
    1.10              val overall_syntax = thy_deps.overall_syntax
    1.11  
    1.12 @@ -261,7 +261,7 @@
    1.13                def node(name: Document.Node.Name): Graph_Display.Node =
    1.14                {
    1.15                  val qualifier = resources.theory_qualifier(name)
    1.16 -                if (qualifier == info.theory_qualifier)
    1.17 +                if (qualifier == info.name)
    1.18                    Graph_Display.Node(name.theory_base_name, "theory." + name.theory)
    1.19                  else session_node(qualifier)
    1.20                }
    1.21 @@ -370,12 +370,6 @@
    1.22      meta_digest: SHA1.Digest)
    1.23    {
    1.24      def timeout: Time = Time.seconds(options.real("timeout") * options.real("timeout_scale"))
    1.25 -
    1.26 -    def theory_qualifier: String =
    1.27 -      options.string("theory_qualifier") match {
    1.28 -        case "" => name
    1.29 -        case qualifier => qualifier
    1.30 -      }
    1.31    }
    1.32  
    1.33    object Selection
    1.34 @@ -496,7 +490,7 @@
    1.35            thy <- info.global_theories.iterator }
    1.36           yield (thy, info)))({
    1.37              case (global, (thy, info)) =>
    1.38 -              val qualifier = info.theory_qualifier
    1.39 +              val qualifier = info.name
    1.40                global.get(thy) match {
    1.41                  case Some(qualifier1) if qualifier != qualifier1 =>
    1.42                    error("Duplicate global theory " + quote(thy) + Position.here(info.pos))