uniform import_name, with treatment of global and qualified theories;
authorwenzelm
Wed Apr 05 22:00:44 2017 +0200 (2017-04-05)
changeset 65392f365f61f2081
parent 65391 b5740579cad6
child 65393 079a6f850c02
uniform import_name, with treatment of global and qualified theories;
src/Pure/PIDE/resources.scala
src/Pure/Thy/sessions.scala
src/Pure/Thy/thy_header.scala
src/Pure/Tools/build.scala
     1.1 --- a/src/Pure/PIDE/resources.scala	Wed Apr 05 11:39:36 2017 +0200
     1.2 +++ b/src/Pure/PIDE/resources.scala	Wed Apr 05 22:00:44 2017 +0200
     1.3 @@ -67,38 +67,27 @@
     1.4      }
     1.5      else Nil
     1.6  
     1.7 -  def qualify(name: String): String =
     1.8 -    if (session_base.global_theories.contains(name) || Long_Name.is_qualified(name)) name
     1.9 -    else Long_Name.qualify(session_name, name)
    1.10 -
    1.11 -  def init_name(raw_path: Path): Document.Node.Name =
    1.12 +  def import_name(dir: String, s: String): Document.Node.Name =
    1.13    {
    1.14 -    val path = raw_path.expand
    1.15 -    val node = path.implode
    1.16 -    val theory = qualify(Thy_Header.thy_name(node).getOrElse(""))
    1.17 -    val master_dir = if (theory == "") "" else path.dir.implode
    1.18 -    Document.Node.Name(node, master_dir, theory)
    1.19 -  }
    1.20 -
    1.21 -  def import_name(master: Document.Node.Name, s: String): Document.Node.Name =
    1.22 -  {
    1.23 -    val theory = Thy_Header.base_name(s)
    1.24 -    val is_qualified = Thy_Header.is_base_name(s) && Long_Name.is_qualified(s)
    1.25 +    val thy = Thy_Header.base_name(s)
    1.26 +    val is_global = session_base.global_theories.contains(thy)
    1.27 +    val is_qualified = Long_Name.is_qualified(thy)
    1.28  
    1.29      val known_theory =
    1.30 -      session_base.known_theories.get(theory) orElse
    1.31 -      (if (is_qualified) session_base.known_theories.get(Long_Name.base_name(theory))
    1.32 -       else session_base.known_theories.get(Long_Name.qualify(session_name, theory)))
    1.33 +      session_base.known_theories.get(thy) orElse
    1.34 +      (if (is_global) None
    1.35 +       else if (is_qualified) session_base.known_theories.get(Long_Name.base_name(thy))
    1.36 +       else session_base.known_theories.get(Long_Name.qualify(session_name, thy)))
    1.37  
    1.38      known_theory match {
    1.39        case Some(name) if session_base.loaded_theory(name) => Document.Node.Name.theory(name.theory)
    1.40        case Some(name) => name
    1.41 -      case None if is_qualified => Document.Node.Name.theory(theory)
    1.42        case None =>
    1.43          val path = Path.explode(s)
    1.44 -        val node = append(master.master_dir, thy_path(path))
    1.45 -        val master_dir = append(master.master_dir, path.dir)
    1.46 -        Document.Node.Name(node, master_dir, Long_Name.qualify(session_name, theory))
    1.47 +        val node = append(dir, thy_path(path))
    1.48 +        val master_dir = append(dir, path.dir)
    1.49 +        val theory = if (is_global || is_qualified) thy else Long_Name.qualify(session_name, thy)
    1.50 +        Document.Node.Name(node, master_dir, theory)
    1.51      }
    1.52    }
    1.53  
    1.54 @@ -126,7 +115,7 @@
    1.55              Completion.report_names(pos, 1, List((base_name, ("theory", base_name)))))
    1.56  
    1.57          val imports =
    1.58 -          header.imports.map({ case (s, pos) => (import_name(node_name, s), pos) })
    1.59 +          header.imports.map({ case (s, pos) => (import_name(node_name.master_dir, s), pos) })
    1.60          Document.Node.Header(imports, header.keywords, header.abbrevs)
    1.61        }
    1.62        catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) }
    1.63 @@ -143,9 +132,11 @@
    1.64  
    1.65    def special_header(name: Document.Node.Name): Option[Document.Node.Header] =
    1.66      if (Thy_Header.is_ml_root(name.theory))
    1.67 -      Some(Document.Node.Header(List((import_name(name, Thy_Header.ML_BOOTSTRAP), Position.none))))
    1.68 +      Some(Document.Node.Header(
    1.69 +        List((import_name(name.master_dir, Thy_Header.ML_BOOTSTRAP), Position.none))))
    1.70      else if (Thy_Header.is_bootstrap(name.theory))
    1.71 -      Some(Document.Node.Header(List((import_name(name, Thy_Header.PURE), Position.none))))
    1.72 +      Some(Document.Node.Header(
    1.73 +        List((import_name(name.master_dir, Thy_Header.PURE), Position.none))))
    1.74      else None
    1.75  
    1.76  
     2.1 --- a/src/Pure/Thy/sessions.scala	Wed Apr 05 11:39:36 2017 +0200
     2.2 +++ b/src/Pure/Thy/sessions.scala	Wed Apr 05 22:00:44 2017 +0200
     2.3 @@ -81,8 +81,7 @@
     2.4              {
     2.5                val root_theories =
     2.6                  info.theories.flatMap({ case (_, thys) =>
     2.7 -                  thys.map(thy =>
     2.8 -                    (resources.init_name(info.dir + resources.thy_path(thy)), info.pos))
     2.9 +                  thys.map(thy => (resources.import_name(info.dir.implode, thy), info.pos))
    2.10                  })
    2.11                val thy_deps = resources.thy_info.dependencies(root_theories)
    2.12  
    2.13 @@ -174,7 +173,7 @@
    2.14      parent: Option[String],
    2.15      description: String,
    2.16      options: Options,
    2.17 -    theories: List[(Options, List[Path])],
    2.18 +    theories: List[(Options, List[String])],
    2.19      global_theories: List[String],
    2.20      files: List[Path],
    2.21      document_files: List[(Path, Path)],
    2.22 @@ -389,8 +388,7 @@
    2.23            val session_options = options ++ entry.options
    2.24  
    2.25            val theories =
    2.26 -            entry.theories.map({ case (opts, thys) =>
    2.27 -              (session_options ++ opts, thys.map(thy => Path.explode(thy._1))) })
    2.28 +            entry.theories.map({ case (opts, thys) => (session_options ++ opts, thys.map(_._1)) })
    2.29  
    2.30            val global_theories =
    2.31              for { (_, thys) <- entry.theories; (thy, global) <- thys if global }
     3.1 --- a/src/Pure/Thy/thy_header.scala	Wed Apr 05 11:39:36 2017 +0200
     3.2 +++ b/src/Pure/Thy/thy_header.scala	Wed Apr 05 22:00:44 2017 +0200
     3.3 @@ -80,9 +80,6 @@
     3.4    private val Base_Name = new Regex(""".*?([^/\\:]+)""")
     3.5    private val Thy_Name = new Regex(""".*?([^/\\:]+)\.thy""")
     3.6  
     3.7 -  def is_base_name(s: String): Boolean =
     3.8 -    s != "" && !s.exists("/\\:".contains(_))
     3.9 -
    3.10    def base_name(s: String): String =
    3.11      s match { case Base_Name(name) => name case _ => error("Malformed import: " + quote(s)) }
    3.12  
     4.1 --- a/src/Pure/Tools/build.scala	Wed Apr 05 11:39:36 2017 +0200
     4.2 +++ b/src/Pure/Tools/build.scala	Wed Apr 05 22:00:44 2017 +0200
     4.3 @@ -204,7 +204,7 @@
     4.4                pair(list(pair(string, int)), pair(list(properties), pair(bool, pair(bool,
     4.5                  pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string,
     4.6                  pair(string, pair(string, pair(string, pair(Path.encode,
     4.7 -                list(pair(Options.encode, list(Path.encode))))))))))))))(
     4.8 +                list(pair(Options.encode, list(string))))))))))))))(
     4.9                (Symbol.codes, (command_timings, (do_output, (verbose,
    4.10                  (store.browser_info, (info.document_files, (File.standard_path(graph_file),
    4.11                  (parent, (info.chapter, (name, (Path.current,