# HG changeset patch # User wenzelm # Date 1492029175 -7200 # Node ID 05e5bffcf1d88f64becd43b7fa270aa997846817 # Parent a0f49174dbebf5ac97b1c51aef5add51311798bf clarified loaded_theories: map to qualified theory name; proper theory_name for PIDE editors; diff -r a0f49174dbeb -r 05e5bffcf1d8 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Wed Apr 12 21:13:43 2017 +0200 +++ b/src/Pure/PIDE/document.scala Wed Apr 12 22:32:55 2017 +0200 @@ -99,6 +99,8 @@ { val empty = Name("") + def loaded_theory(theory: String): Name = Name(theory, "", theory) + object Ordering extends scala.math.Ordering[Name] { def compare(name1: Name, name2: Name): Int = name1.node compare name2.node @@ -114,7 +116,6 @@ case _ => false } - def loaded_theory: Name = Name(theory, "", theory) def is_theory: Boolean = theory.nonEmpty def theory_base_name: String = Long_Name.base_name(theory) diff -r a0f49174dbeb -r 05e5bffcf1d8 src/Pure/PIDE/protocol.scala --- a/src/Pure/PIDE/protocol.scala Wed Apr 12 21:13:43 2017 +0200 +++ b/src/Pure/PIDE/protocol.scala Wed Apr 12 22:32:55 2017 +0200 @@ -314,7 +314,7 @@ protocol_command("Prover.session_base", Symbol.encode(resources.default_qualifier), encode_table(resources.session_base.global_theories.toList), - encode_table(resources.session_base.dest_loaded_theories), + encode_table(resources.session_base.loaded_theories.toList), encode_table(resources.session_base.dest_known_theories)) diff -r a0f49174dbeb -r 05e5bffcf1d8 src/Pure/PIDE/resources.ML --- a/src/Pure/PIDE/resources.ML Wed Apr 12 21:13:43 2017 +0200 +++ b/src/Pure/PIDE/resources.ML Wed Apr 12 22:32:55 2017 +0200 @@ -14,7 +14,7 @@ val reset_session_base: unit -> unit val default_qualifier: unit -> string val global_theory: string -> string option - val loaded_theory: string -> Path.T option + val loaded_theory: string -> string option val known_theory: string -> Path.T option val master_directory: theory -> Path.T val imports_of: theory -> (string * Position.T) list @@ -43,7 +43,7 @@ val init_session_base = {default_qualifier = "Draft", global_theories = Symtab.empty: string Symtab.table, - loaded_theories = Symtab.empty: Path.T Symtab.table, + loaded_theories = Symtab.empty: string Symtab.table, known_theories = Symtab.empty: Path.T Symtab.table}; val global_session_base = @@ -56,7 +56,7 @@ if default_qualifier <> "" then default_qualifier else #default_qualifier init_session_base, global_theories = Symtab.make global_theories, - loaded_theories = Symtab.make (map (apsnd Path.explode) loaded_theories), + loaded_theories = Symtab.make loaded_theories, known_theories = Symtab.make (map (apsnd Path.explode) known_theories)}); fun reset_session_base () = @@ -108,20 +108,24 @@ SOME qualifier => qualifier | NONE => Long_Name.qualifier theory); +fun theory_name qualifier theory0 = + (case loaded_theory theory0 of + SOME theory => (true, theory) + | NONE => + (false, + if Long_Name.is_qualified theory0 orelse is_some (global_theory theory0) + orelse true (* FIXME *) then theory0 + else Long_Name.qualify qualifier theory0)); + fun import_name qualifier dir s = let - val theory0 = Thy_Header.import_name s; - val theory = - if Long_Name.is_qualified theory0 orelse is_some (global_theory theory0) - orelse true (* FIXME *) then theory0 - else Long_Name.qualify qualifier theory0; + val (loaded, theory) = theory_name qualifier (Thy_Header.import_name s); val node_name = - the (get_first (fn e => e ()) - [fn () => loaded_theory theory, - fn () => loaded_theory theory0, - fn () => known_theory theory, - fn () => known_theory theory0, - fn () => SOME (File.full_path dir (thy_path (Path.expand (Path.explode s))))]) + if loaded then Path.basic theory + else + (case known_theory theory of + SOME node_name => node_name + | NONE => File.full_path dir (thy_path (Path.expand (Path.explode s)))); in {node_name = node_name, master_dir = Path.dir node_name, theory_name = theory} end; fun check_file dir file = File.check_file (File.full_path dir file); diff -r a0f49174dbeb -r 05e5bffcf1d8 src/Pure/PIDE/resources.scala --- a/src/Pure/PIDE/resources.scala Wed Apr 12 21:13:43 2017 +0200 +++ b/src/Pure/PIDE/resources.scala Wed Apr 12 22:32:55 2017 +0200 @@ -70,23 +70,30 @@ def theory_qualifier(name: Document.Node.Name): String = session_base.global_theories.getOrElse(name.theory, Long_Name.qualifier(name.theory)) + def theory_name(qualifier: String, theory0: String): (Boolean, String) = + session_base.loaded_theories.get(theory0) match { + case Some(theory) => (true, theory) + case None => + val theory = + if (Long_Name.is_qualified(theory0) || session_base.global_theories.isDefinedAt(theory0) + || true /* FIXME */) theory0 + else Long_Name.qualify(qualifier, theory0) + (false, theory) + } + def import_name(qualifier: String, dir: String, s: String): Document.Node.Name = { - val theory0 = Thy_Header.import_name(s) - val theory = - if (Long_Name.is_qualified(theory0) || session_base.global_theories.isDefinedAt(theory0) - || true /* FIXME */) theory0 - else Long_Name.qualify(qualifier, theory0) - - session_base.loaded_theories.get(theory) orElse - session_base.loaded_theories.get(theory0) orElse - session_base.known_theories.get(theory) orElse - session_base.known_theories.get(theory0) getOrElse { - val path = Path.explode(s) - val node = append(dir, thy_path(path)) - val master_dir = append(dir, path.dir) - Document.Node.Name(node, master_dir, theory) - } + val (loaded, theory) = theory_name(qualifier, Thy_Header.import_name(s)) + if (loaded) Document.Node.Name.loaded_theory(theory) + else + session_base.known_theories.get(theory) match { + case Some(node_name) => node_name + case None => + val path = Path.explode(s) + val node = append(dir, thy_path(path)) + val master_dir = append(dir, path.dir) + Document.Node.Name(node, master_dir, theory) + } } def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A = diff -r a0f49174dbeb -r 05e5bffcf1d8 src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Wed Apr 12 21:13:43 2017 +0200 +++ b/src/Pure/Thy/sessions.scala Wed Apr 12 22:32:55 2017 +0200 @@ -85,7 +85,7 @@ sealed case class Base( global_theories: Map[String, String] = Map.empty, - loaded_theories: Map[String, Document.Node.Name] = Map.empty, + loaded_theories: Map[String, String] = Map.empty, known_theories: Map[String, Document.Node.Name] = Map.empty, known_theories_local: Map[String, Document.Node.Name] = Map.empty, known_files: Map[JFile, List[Document.Node.Name]] = Map.empty, @@ -96,8 +96,6 @@ { def platform_path: Base = copy( - loaded_theories = - for ((a, b) <- loaded_theories) yield (a, b.map(File.platform_path(_))), known_theories = for ((a, b) <- known_theories) yield (a, b.map(File.platform_path(_))), known_theories_local = @@ -108,10 +106,6 @@ def loaded_theory(name: Document.Node.Name): Boolean = loaded_theories.isDefinedAt(name.theory) - def dest_loaded_theories: List[(String, String)] = - for ((theory, node_name) <- loaded_theories.toList) - yield (theory, node_name.node) - def dest_known_theories: List[(String, String)] = for ((theory, node_name) <- known_theories.toList) yield (theory, node_name.node) diff -r a0f49174dbeb -r 05e5bffcf1d8 src/Pure/Thy/thy_info.scala --- a/src/Pure/Thy/thy_info.scala Wed Apr 12 21:13:43 2017 +0200 +++ b/src/Pure/Thy/thy_info.scala Wed Apr 12 22:32:55 2017 +0200 @@ -80,12 +80,12 @@ lazy val syntax: Outer_Syntax = resources.session_base.syntax.add_keywords(keywords).add_abbrevs(abbrevs) - def loaded_theories: Map[String, Document.Node.Name] = + def loaded_theories: Map[String, String] = (resources.session_base.loaded_theories /: rev_deps) { case (loaded, dep) => - val name = dep.name.loaded_theory - loaded + (name.theory -> name) + - (name.theory_base_name -> name) // legacy + val name = dep.name + loaded + (name.theory -> name.theory) + + (name.theory_base_name -> name.theory) // legacy } def loaded_files: List[Path] = diff -r a0f49174dbeb -r 05e5bffcf1d8 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Wed Apr 12 21:13:43 2017 +0200 +++ b/src/Pure/Tools/build.scala Wed Apr 12 22:32:55 2017 +0200 @@ -205,14 +205,14 @@ pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string, pair(string, pair(string, pair(string, pair(Path.encode, pair(list(pair(Options.encode, list(string))), - pair(list(pair(string, string)), - pair(list(pair(string, string)), list(pair(string, string))))))))))))))))( + pair(list(pair(string, string)), pair(list(pair(string, string)), + list(pair(string, 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, (info.theories, - (base.global_theories.toList, - (base.dest_loaded_theories, base.dest_known_theories))))))))))))))) + (base.global_theories.toList, (base.loaded_theories.toList, + base.dest_known_theories))))))))))))))) }) val env = diff -r a0f49174dbeb -r 05e5bffcf1d8 src/Pure/Tools/ml_process.scala --- a/src/Pure/Tools/ml_process.scala Wed Apr 12 21:13:43 2017 +0200 +++ b/src/Pure/Tools/ml_process.scala Wed Apr 12 22:32:55 2017 +0200 @@ -101,7 +101,7 @@ ML_Syntax.print_string, ML_Syntax.print_string))(table) List("Resources.set_session_base {default_qualifier = \"\"" + ", global_theories = " + print_table(base.global_theories.toList) + - ", loaded_theories = " + print_table(base.dest_loaded_theories) + + ", loaded_theories = " + print_table(base.loaded_theories.toList) + ", known_theories = " + print_table(base.dest_known_theories) + "}") } diff -r a0f49174dbeb -r 05e5bffcf1d8 src/Tools/VSCode/src/vscode_resources.scala --- a/src/Tools/VSCode/src/vscode_resources.scala Wed Apr 12 21:13:43 2017 +0200 +++ b/src/Tools/VSCode/src/vscode_resources.scala Wed Apr 12 22:32:55 2017 +0200 @@ -63,9 +63,9 @@ def node_name(file: JFile): Document.Node.Name = { val node = file.getPath - val theory = Thy_Header.theory_name(node) - val master_dir = if (theory == "") "" else file.getParent - Document.Node.Name(node, master_dir, theory) + val (loaded, theory) = theory_name(default_qualifier, Thy_Header.theory_name(node)) + if (loaded) Document.Node.Name.loaded_theory(theory) + else Document.Node.Name(node, if (theory == "") "" else file.getParent, theory) } override def append(dir: String, source_path: Path): String = diff -r a0f49174dbeb -r 05e5bffcf1d8 src/Tools/jEdit/src/jedit_resources.scala --- a/src/Tools/jEdit/src/jedit_resources.scala Wed Apr 12 21:13:43 2017 +0200 +++ b/src/Tools/jEdit/src/jedit_resources.scala Wed Apr 12 22:32:55 2017 +0200 @@ -29,9 +29,9 @@ { val vfs = VFSManager.getVFSForPath(path) val node = if (vfs.isInstanceOf[FileVFS]) MiscUtilities.resolveSymlinks(path) else path - val theory = Thy_Header.theory_name(node) - val master_dir = if (theory == "") "" else vfs.getParentOfPath(path) - Document.Node.Name(node, master_dir, theory) + val (loaded, theory) = theory_name(default_qualifier, Thy_Header.theory_name(node)) + if (loaded) Document.Node.Name.loaded_theory(theory) + else Document.Node.Name(node, if (theory == "") "" else vfs.getParentOfPath(path), theory) } def node_name(buffer: Buffer): Document.Node.Name =