# HG changeset patch # User wenzelm # Date 1491422444 -7200 # Node ID f365f61f2081266a5d00763679ec8ad6cbd41b76 # Parent b5740579cad62284410e31519b8e4b173e9c9f73 uniform import_name, with treatment of global and qualified theories; diff -r b5740579cad6 -r f365f61f2081 src/Pure/PIDE/resources.scala --- a/src/Pure/PIDE/resources.scala Wed Apr 05 11:39:36 2017 +0200 +++ b/src/Pure/PIDE/resources.scala Wed Apr 05 22:00:44 2017 +0200 @@ -67,38 +67,27 @@ } else Nil - def qualify(name: String): String = - if (session_base.global_theories.contains(name) || Long_Name.is_qualified(name)) name - else Long_Name.qualify(session_name, name) - - def init_name(raw_path: Path): Document.Node.Name = + def import_name(dir: String, s: String): Document.Node.Name = { - val path = raw_path.expand - val node = path.implode - val theory = qualify(Thy_Header.thy_name(node).getOrElse("")) - val master_dir = if (theory == "") "" else path.dir.implode - Document.Node.Name(node, master_dir, theory) - } - - def import_name(master: Document.Node.Name, s: String): Document.Node.Name = - { - val theory = Thy_Header.base_name(s) - val is_qualified = Thy_Header.is_base_name(s) && Long_Name.is_qualified(s) + val thy = Thy_Header.base_name(s) + val is_global = session_base.global_theories.contains(thy) + val is_qualified = Long_Name.is_qualified(thy) val known_theory = - session_base.known_theories.get(theory) orElse - (if (is_qualified) session_base.known_theories.get(Long_Name.base_name(theory)) - else session_base.known_theories.get(Long_Name.qualify(session_name, theory))) + session_base.known_theories.get(thy) orElse + (if (is_global) None + else if (is_qualified) session_base.known_theories.get(Long_Name.base_name(thy)) + else session_base.known_theories.get(Long_Name.qualify(session_name, thy))) known_theory match { case Some(name) if session_base.loaded_theory(name) => Document.Node.Name.theory(name.theory) case Some(name) => name - case None if is_qualified => Document.Node.Name.theory(theory) case None => val path = Path.explode(s) - val node = append(master.master_dir, thy_path(path)) - val master_dir = append(master.master_dir, path.dir) - Document.Node.Name(node, master_dir, Long_Name.qualify(session_name, theory)) + val node = append(dir, thy_path(path)) + val master_dir = append(dir, path.dir) + val theory = if (is_global || is_qualified) thy else Long_Name.qualify(session_name, thy) + Document.Node.Name(node, master_dir, theory) } } @@ -126,7 +115,7 @@ Completion.report_names(pos, 1, List((base_name, ("theory", base_name))))) val imports = - header.imports.map({ case (s, pos) => (import_name(node_name, s), pos) }) + header.imports.map({ case (s, pos) => (import_name(node_name.master_dir, s), pos) }) Document.Node.Header(imports, header.keywords, header.abbrevs) } catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) } @@ -143,9 +132,11 @@ def special_header(name: Document.Node.Name): Option[Document.Node.Header] = if (Thy_Header.is_ml_root(name.theory)) - Some(Document.Node.Header(List((import_name(name, Thy_Header.ML_BOOTSTRAP), Position.none)))) + Some(Document.Node.Header( + List((import_name(name.master_dir, Thy_Header.ML_BOOTSTRAP), Position.none)))) else if (Thy_Header.is_bootstrap(name.theory)) - Some(Document.Node.Header(List((import_name(name, Thy_Header.PURE), Position.none)))) + Some(Document.Node.Header( + List((import_name(name.master_dir, Thy_Header.PURE), Position.none)))) else None diff -r b5740579cad6 -r f365f61f2081 src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Wed Apr 05 11:39:36 2017 +0200 +++ b/src/Pure/Thy/sessions.scala Wed Apr 05 22:00:44 2017 +0200 @@ -81,8 +81,7 @@ { val root_theories = info.theories.flatMap({ case (_, thys) => - thys.map(thy => - (resources.init_name(info.dir + resources.thy_path(thy)), info.pos)) + thys.map(thy => (resources.import_name(info.dir.implode, thy), info.pos)) }) val thy_deps = resources.thy_info.dependencies(root_theories) @@ -174,7 +173,7 @@ parent: Option[String], description: String, options: Options, - theories: List[(Options, List[Path])], + theories: List[(Options, List[String])], global_theories: List[String], files: List[Path], document_files: List[(Path, Path)], @@ -389,8 +388,7 @@ val session_options = options ++ entry.options val theories = - entry.theories.map({ case (opts, thys) => - (session_options ++ opts, thys.map(thy => Path.explode(thy._1))) }) + entry.theories.map({ case (opts, thys) => (session_options ++ opts, thys.map(_._1)) }) val global_theories = for { (_, thys) <- entry.theories; (thy, global) <- thys if global } diff -r b5740579cad6 -r f365f61f2081 src/Pure/Thy/thy_header.scala --- a/src/Pure/Thy/thy_header.scala Wed Apr 05 11:39:36 2017 +0200 +++ b/src/Pure/Thy/thy_header.scala Wed Apr 05 22:00:44 2017 +0200 @@ -80,9 +80,6 @@ private val Base_Name = new Regex(""".*?([^/\\:]+)""") private val Thy_Name = new Regex(""".*?([^/\\:]+)\.thy""") - def is_base_name(s: String): Boolean = - s != "" && !s.exists("/\\:".contains(_)) - def base_name(s: String): String = s match { case Base_Name(name) => name case _ => error("Malformed import: " + quote(s)) } diff -r b5740579cad6 -r f365f61f2081 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Wed Apr 05 11:39:36 2017 +0200 +++ b/src/Pure/Tools/build.scala Wed Apr 05 22:00:44 2017 +0200 @@ -204,7 +204,7 @@ pair(list(pair(string, int)), pair(list(properties), pair(bool, pair(bool, pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string, pair(string, pair(string, pair(string, pair(Path.encode, - list(pair(Options.encode, list(Path.encode))))))))))))))( + list(pair(Options.encode, list(string))))))))))))))( (Symbol.codes, (command_timings, (do_output, (verbose, (store.browser_info, (info.document_files, (File.standard_path(graph_file), (parent, (info.chapter, (name, (Path.current,