clarified modules;
authorwenzelm
Thu Oct 05 16:33:36 2017 +0200 (20 months ago)
changeset 66767294c2e9a689e
parent 66766 19f8385ddfd3
child 66768 f27488f47a47
clarified modules;
src/Pure/PIDE/resources.scala
src/Pure/Tools/imports.scala
     1.1 --- a/src/Pure/PIDE/resources.scala	Thu Oct 05 14:58:04 2017 +0200
     1.2 +++ b/src/Pure/PIDE/resources.scala	Thu Oct 05 16:33:36 2017 +0200
     1.3 @@ -115,6 +115,25 @@
     1.4    def import_name(name: Document.Node.Name, s: String): Document.Node.Name =
     1.5      import_name(theory_qualifier(name), name.master_dir, s)
     1.6  
     1.7 +  def standard_import(session_resources: Resources,
     1.8 +    qualifier: String, dir: String, s: String): String =
     1.9 +  {
    1.10 +    val name = import_name(qualifier, dir, s)
    1.11 +    val s1 =
    1.12 +      if (session_base.loaded_theory(name)) name.theory
    1.13 +      else {
    1.14 +        session_base.known.get_file(name.path.file) match {
    1.15 +          case Some(name1) if session_resources.theory_qualifier(name1) != qualifier =>
    1.16 +            name1.theory
    1.17 +          case Some(name1) if Thy_Header.is_base_name(s) =>
    1.18 +            name1.theory_base_name
    1.19 +          case _ => s
    1.20 +        }
    1.21 +      }
    1.22 +    val name2 = import_name(qualifier, dir, s1)
    1.23 +    if (name.node == name2.node) s1 else s
    1.24 +  }
    1.25 +
    1.26    def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
    1.27    {
    1.28      val path = File.check_file(name.path)
     2.1 --- a/src/Pure/Tools/imports.scala	Thu Oct 05 14:58:04 2017 +0200
     2.2 +++ b/src/Pure/Tools/imports.scala	Thu Oct 05 16:33:36 2017 +0200
     2.3 @@ -141,22 +141,7 @@
     2.4            val imports_resources = new Resources(imports_base)
     2.5  
     2.6            def standard_import(qualifier: String, dir: String, s: String): String =
     2.7 -          {
     2.8 -            val name = imports_resources.import_name(qualifier, dir, s)
     2.9 -            val s1 =
    2.10 -              if (imports_base.loaded_theory(name)) name.theory
    2.11 -              else {
    2.12 -                imports_base.known.get_file(name.path.file) match {
    2.13 -                  case Some(name1) if session_resources.theory_qualifier(name1) != qualifier =>
    2.14 -                    name1.theory
    2.15 -                  case Some(name1) if Thy_Header.is_base_name(s) =>
    2.16 -                    name1.theory_base_name
    2.17 -                  case _ => s
    2.18 -                }
    2.19 -              }
    2.20 -            val name2 = imports_resources.import_name(qualifier, dir, s1)
    2.21 -            if (name.node == name2.node) s1 else s
    2.22 -          }
    2.23 +            imports_resources.standard_import(session_resources, qualifier, dir, s)
    2.24  
    2.25            val updates_root =
    2.26              for {