more explicit lookup of loaded_theories: base names allowed here;
authorwenzelm
Fri Apr 07 16:34:14 2017 +0200 (2017-04-07)
changeset 65429fcff401fb609
parent 65428 f8dd71a0791a
child 65430 4433d189a77d
more explicit lookup of loaded_theories: base names allowed here;
no base names for known_theories;
src/Pure/PIDE/resources.scala
src/Pure/Thy/sessions.scala
src/Pure/Thy/thy_info.scala
     1.1 --- a/src/Pure/PIDE/resources.scala	Fri Apr 07 15:53:06 2017 +0200
     1.2 +++ b/src/Pure/PIDE/resources.scala	Fri Apr 07 16:34:14 2017 +0200
     1.3 @@ -74,15 +74,14 @@
     1.4        if (Long_Name.is_qualified(theory0) || session_base.global_theories.contains(theory0)) theory0
     1.5        else Long_Name.qualify(session_name, theory0)
     1.6  
     1.7 -    session_base.known_theories.get(theory) orElse session_base.known_theories.get(theory0) match
     1.8 -    {
     1.9 -      case Some(name) =>
    1.10 -        if (session_base.loaded_theory(name)) name.loaded_theory else name
    1.11 -      case None =>
    1.12 -        val path = Path.explode(s)
    1.13 -        val node = append(dir, thy_path(path))
    1.14 -        val master_dir = append(dir, path.dir)
    1.15 -        Document.Node.Name(node, master_dir, theory)
    1.16 +    session_base.loaded_theories.get(theory) orElse
    1.17 +    session_base.loaded_theories.get(theory0) orElse
    1.18 +    session_base.known_theories.get(theory) orElse
    1.19 +    session_base.known_theories.get(theory0) getOrElse {
    1.20 +      val path = Path.explode(s)
    1.21 +      val node = append(dir, thy_path(path))
    1.22 +      val master_dir = append(dir, path.dir)
    1.23 +      Document.Node.Name(node, master_dir, theory)
    1.24      }
    1.25    }
    1.26  
     2.1 --- a/src/Pure/Thy/sessions.scala	Fri Apr 07 15:53:06 2017 +0200
     2.2 +++ b/src/Pure/Thy/sessions.scala	Fri Apr 07 16:34:14 2017 +0200
     2.3 @@ -40,9 +40,7 @@
     2.4            known.get(name.theory) match {
     2.5              case Some(name1) if name != name1 =>
     2.6                error("Duplicate theory " + quote(name.node) + " vs. " + quote(name1.node))
     2.7 -            case _ =>
     2.8 -              known + (name.theory -> name) +
     2.9 -                (Long_Name.base_name(name.theory) -> name)  // legacy
    2.10 +            case _ => known + (name.theory -> name)
    2.11            }
    2.12          })
    2.13      }
    2.14 @@ -50,7 +48,7 @@
    2.15  
    2.16    sealed case class Base(
    2.17      global_theories: Set[String] = Set.empty,
    2.18 -    loaded_theories: Set[String] = Set.empty,
    2.19 +    loaded_theories: Map[String, Document.Node.Name] = Map.empty,
    2.20      known_theories: Map[String, Document.Node.Name] = Map.empty,
    2.21      keywords: Thy_Header.Keywords = Nil,
    2.22      syntax: Outer_Syntax = Outer_Syntax.empty,
    2.23 @@ -58,7 +56,7 @@
    2.24      session_graph: Graph_Display.Graph = Graph_Display.empty_graph)
    2.25    {
    2.26      def loaded_theory(name: Document.Node.Name): Boolean =
    2.27 -      loaded_theories.contains(name.theory)
    2.28 +      loaded_theories.isDefinedAt(name.theory)
    2.29    }
    2.30  
    2.31    sealed case class Deps(sessions: Map[String, Base])
     3.1 --- a/src/Pure/Thy/thy_info.scala	Fri Apr 07 15:53:06 2017 +0200
     3.2 +++ b/src/Pure/Thy/thy_info.scala	Fri Apr 07 16:34:14 2017 +0200
     3.3 @@ -67,7 +67,7 @@
     3.4        val import_errors =
     3.5          (for {
     3.6            (theory, imports) <- seen_theory.iterator_list
     3.7 -          if !resources.session_base.loaded_theories(theory)
     3.8 +          if !resources.session_base.loaded_theories.isDefinedAt(theory)
     3.9            if imports.length > 1
    3.10          } yield {
    3.11            "Incoherent imports for theory " + quote(theory) + ":\n" +
    3.12 @@ -80,11 +80,12 @@
    3.13      lazy val syntax: Outer_Syntax =
    3.14        resources.session_base.syntax.add_keywords(keywords).add_abbrevs(abbrevs)
    3.15  
    3.16 -    def loaded_theories: Set[String] =
    3.17 +    def loaded_theories: Map[String, Document.Node.Name] =
    3.18        (resources.session_base.loaded_theories /: rev_deps) {
    3.19          case (loaded, dep) =>
    3.20 -          loaded + dep.name.theory +
    3.21 -            Long_Name.base_name(dep.name.theory)  // legacy
    3.22 +          val name = dep.name.loaded_theory
    3.23 +          loaded + (name.theory -> name) +
    3.24 +            (Long_Name.base_name(name.theory) -> name)  // legacy
    3.25        }
    3.26  
    3.27      def loaded_files: List[Path] =