proper imports_resources for import_name: avoid self-referential name resolution;
authorwenzelm
Fri Apr 21 18:51:24 2017 +0200 (2017-04-21)
changeset 655402b73ed8bf4d9
parent 65539 dbcd9b3e1b49
child 65541 ae09b9f5980b
proper imports_resources for import_name: avoid self-referential name resolution;
src/Pure/Thy/sessions.scala
src/Pure/Tools/update_imports.scala
     1.1 --- a/src/Pure/Thy/sessions.scala	Fri Apr 21 17:34:13 2017 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Fri Apr 21 18:51:24 2017 +0200
     1.3 @@ -98,6 +98,7 @@
     1.4    }
     1.5  
     1.6    sealed case class Base(
     1.7 +    imports: Option[Base] = None,
     1.8      global_theories: Map[String, String] = Map.empty,
     1.9      loaded_theories: Map[String, String] = Map.empty,
    1.10      known: Known = Known.empty,
    1.11 @@ -106,6 +107,8 @@
    1.12      sources: List[(Path, SHA1.Digest)] = Nil,
    1.13      session_graph: Graph_Display.Graph = Graph_Display.empty_graph)
    1.14    {
    1.15 +    def get_imports: Base = imports getOrElse Base.bootstrap(global_theories)
    1.16 +
    1.17      def platform_path: Base = copy(known = known.platform_path)
    1.18  
    1.19      def loaded_theory(name: Document.Node.Name): Boolean =
    1.20 @@ -237,7 +240,8 @@
    1.21              }
    1.22  
    1.23              val base =
    1.24 -              Base(global_theories = global_theories,
    1.25 +              Base(imports = Some(imports_base),
    1.26 +                global_theories = global_theories,
    1.27                  loaded_theories = thy_deps.loaded_theories,
    1.28                  known = Known.make(info.dir, List(imports_base), thy_deps.deps.map(_.name)),
    1.29                  keywords = thy_deps.keywords,
     2.1 --- a/src/Pure/Tools/update_imports.scala	Fri Apr 21 17:34:13 2017 +0200
     2.2 +++ b/src/Pure/Tools/update_imports.scala	Fri Apr 21 18:51:24 2017 +0200
     2.3 @@ -68,22 +68,24 @@
     2.4      {
     2.5        val info = full_sessions(session_name)
     2.6        val session_base = deps(session_name)
     2.7 -      val resources = new Resources(session_base)
     2.8 +      val session_resources = new Resources(session_base)
     2.9 +      val imports_resources = new Resources(session_base.get_imports)
    2.10 +
    2.11        val local_theories =
    2.12          (for {
    2.13            (_, name) <- session_base.known.theories_local.iterator
    2.14 -          if resources.theory_qualifier(name) == info.theory_qualifier
    2.15 +          if session_resources.theory_qualifier(name) == info.theory_qualifier
    2.16          } yield name).toSet
    2.17  
    2.18        def standard_import(qualifier: String, dir: String, s: String): String =
    2.19        {
    2.20 -        val name = resources.import_name(qualifier, dir, s)
    2.21 +        val name = imports_resources.import_name(qualifier, dir, s)
    2.22          val s1 =
    2.23            if (!local_theories.contains(name)) s
    2.24 -          else if (resources.theory_qualifier(name) != qualifier) name.theory
    2.25 +          else if (session_resources.theory_qualifier(name) != qualifier) name.theory
    2.26            else if (Thy_Header.is_base_name(s)) name.theory_base_name
    2.27            else s
    2.28 -        val name1 = resources.import_name(qualifier, dir, s1)
    2.29 +        val name1 = imports_resources.import_name(qualifier, dir, s1)
    2.30          if (name == name1) s1 else s
    2.31        }
    2.32  
    2.33 @@ -97,9 +99,9 @@
    2.34        val updates_theories =
    2.35          for {
    2.36            (_, name) <- session_base.known.theories_local.toList
    2.37 -          (_, pos) <- resources.check_thy(name, Token.Pos.file(name.node)).imports
    2.38 +          (_, pos) <- session_resources.check_thy(name, Token.Pos.file(name.node)).imports
    2.39            upd <- update_name(session_base.syntax.keywords, pos,
    2.40 -            standard_import(resources.theory_qualifier(name), name.master_dir, _))
    2.41 +            standard_import(session_resources.theory_qualifier(name), name.master_dir, _))
    2.42          } yield upd
    2.43  
    2.44        updates_root ::: updates_theories