theory qualifier is always session name (see also 31e8a86971a8);
authorwenzelm
Sat Oct 07 20:31:01 2017 +0200 (3 months ago)
changeset 66780bf54ca580bf2
parent 66779 8645d56f96e1
child 66781 dac4cfbfede8
child 66783 bbe87f1b5e5d
theory qualifier is always session name (see also 31e8a86971a8);
etc/options
src/Pure/Thy/sessions.scala
src/Pure/Tools/imports.scala
     1.1 --- a/etc/options	Sat Oct 07 20:20:03 2017 +0200
     1.2 +++ b/etc/options	Sat Oct 07 20:31:01 2017 +0200
     1.3 @@ -113,9 +113,6 @@
     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/Pure/Thy/sessions.scala	Sat Oct 07 20:20:03 2017 +0200
     2.2 +++ b/src/Pure/Thy/sessions.scala	Sat Oct 07 20:31:01 2017 +0200
     2.3 @@ -224,7 +224,7 @@
     2.4              val thy_deps =
     2.5                resources.thy_info.dependencies(
     2.6                  for { (_, thys) <- info.theories; (thy, pos) <- thys }
     2.7 -                yield (resources.import_name(info.theory_qualifier, info.dir.implode, thy), pos))
     2.8 +                yield (resources.import_name(info.name, info.dir.implode, thy), pos))
     2.9  
    2.10              val overall_syntax = thy_deps.overall_syntax
    2.11  
    2.12 @@ -261,7 +261,7 @@
    2.13                def node(name: Document.Node.Name): Graph_Display.Node =
    2.14                {
    2.15                  val qualifier = resources.theory_qualifier(name)
    2.16 -                if (qualifier == info.theory_qualifier)
    2.17 +                if (qualifier == info.name)
    2.18                    Graph_Display.Node(name.theory_base_name, "theory." + name.theory)
    2.19                  else session_node(qualifier)
    2.20                }
    2.21 @@ -370,12 +370,6 @@
    2.22      meta_digest: SHA1.Digest)
    2.23    {
    2.24      def timeout: Time = Time.seconds(options.real("timeout") * options.real("timeout_scale"))
    2.25 -
    2.26 -    def theory_qualifier: String =
    2.27 -      options.string("theory_qualifier") match {
    2.28 -        case "" => name
    2.29 -        case qualifier => qualifier
    2.30 -      }
    2.31    }
    2.32  
    2.33    object Selection
    2.34 @@ -496,7 +490,7 @@
    2.35            thy <- info.global_theories.iterator }
    2.36           yield (thy, info)))({
    2.37              case (global, (thy, info)) =>
    2.38 -              val qualifier = info.theory_qualifier
    2.39 +              val qualifier = info.name
    2.40                global.get(thy) match {
    2.41                  case Some(qualifier1) if qualifier != qualifier1 =>
    2.42                    error("Duplicate global theory " + quote(thy) + Position.here(info.pos))
     3.1 --- a/src/Pure/Tools/imports.scala	Sat Oct 07 20:20:03 2017 +0200
     3.2 +++ b/src/Pure/Tools/imports.scala	Sat Oct 07 20:31:01 2017 +0200
     3.3 @@ -104,7 +104,7 @@
     3.4          val extra_imports =
     3.5            (for {
     3.6              (_, a) <- session_resources.session_base.known.theories.iterator
     3.7 -            if session_resources.theory_qualifier(a) == info.theory_qualifier
     3.8 +            if session_resources.theory_qualifier(a) == info.name
     3.9              b <- deps.all_known.get_file(a.path.file)
    3.10              qualifier = session_resources.theory_qualifier(b)
    3.11              if !declared_imports.contains(qualifier)
    3.12 @@ -146,14 +146,13 @@
    3.13            val updates_root =
    3.14              for {
    3.15                (_, pos) <- info.theories.flatMap(_._2)
    3.16 -              upd <- update_name(root_keywords, pos,
    3.17 -                standard_import(info.theory_qualifier, info.dir.implode, _))
    3.18 +              upd <- update_name(root_keywords, pos, standard_import(info.name, info.dir.implode, _))
    3.19              } yield upd
    3.20  
    3.21            val updates_theories =
    3.22              for {
    3.23                (_, name) <- session_base.known.theories_local.toList
    3.24 -              if session_resources.theory_qualifier(name) == info.theory_qualifier
    3.25 +              if session_resources.theory_qualifier(name) == info.name
    3.26                (_, pos) <- session_resources.check_thy(name, Token.Pos.file(name.node)).imports
    3.27                upd <- update_name(session_base.overall_syntax.keywords, pos,
    3.28                  standard_import(session_resources.theory_qualifier(name), name.master_dir, _))