clarified loaded_theories: map to qualified theory name;
authorwenzelm
Wed Apr 12 22:32:55 2017 +0200 (2017-04-12 ago)
changeset 6547105e5bffcf1d8
parent 65470 a0f49174dbeb
child 65472 f83081bcdd0e
clarified loaded_theories: map to qualified theory name;
proper theory_name for PIDE editors;
src/Pure/PIDE/document.scala
src/Pure/PIDE/protocol.scala
src/Pure/PIDE/resources.ML
src/Pure/PIDE/resources.scala
src/Pure/Thy/sessions.scala
src/Pure/Thy/thy_info.scala
src/Pure/Tools/build.scala
src/Pure/Tools/ml_process.scala
src/Tools/VSCode/src/vscode_resources.scala
src/Tools/jEdit/src/jedit_resources.scala
     1.1 --- a/src/Pure/PIDE/document.scala	Wed Apr 12 21:13:43 2017 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Wed Apr 12 22:32:55 2017 +0200
     1.3 @@ -99,6 +99,8 @@
     1.4      {
     1.5        val empty = Name("")
     1.6  
     1.7 +      def loaded_theory(theory: String): Name = Name(theory, "", theory)
     1.8 +
     1.9        object Ordering extends scala.math.Ordering[Name]
    1.10        {
    1.11          def compare(name1: Name, name2: Name): Int = name1.node compare name2.node
    1.12 @@ -114,7 +116,6 @@
    1.13            case _ => false
    1.14          }
    1.15  
    1.16 -      def loaded_theory: Name = Name(theory, "", theory)
    1.17        def is_theory: Boolean = theory.nonEmpty
    1.18  
    1.19        def theory_base_name: String = Long_Name.base_name(theory)
     2.1 --- a/src/Pure/PIDE/protocol.scala	Wed Apr 12 21:13:43 2017 +0200
     2.2 +++ b/src/Pure/PIDE/protocol.scala	Wed Apr 12 22:32:55 2017 +0200
     2.3 @@ -314,7 +314,7 @@
     2.4      protocol_command("Prover.session_base",
     2.5        Symbol.encode(resources.default_qualifier),
     2.6        encode_table(resources.session_base.global_theories.toList),
     2.7 -      encode_table(resources.session_base.dest_loaded_theories),
     2.8 +      encode_table(resources.session_base.loaded_theories.toList),
     2.9        encode_table(resources.session_base.dest_known_theories))
    2.10  
    2.11  
     3.1 --- a/src/Pure/PIDE/resources.ML	Wed Apr 12 21:13:43 2017 +0200
     3.2 +++ b/src/Pure/PIDE/resources.ML	Wed Apr 12 22:32:55 2017 +0200
     3.3 @@ -14,7 +14,7 @@
     3.4    val reset_session_base: unit -> unit
     3.5    val default_qualifier: unit -> string
     3.6    val global_theory: string -> string option
     3.7 -  val loaded_theory: string -> Path.T option
     3.8 +  val loaded_theory: string -> string option
     3.9    val known_theory: string -> Path.T option
    3.10    val master_directory: theory -> Path.T
    3.11    val imports_of: theory -> (string * Position.T) list
    3.12 @@ -43,7 +43,7 @@
    3.13  val init_session_base =
    3.14    {default_qualifier = "Draft",
    3.15     global_theories = Symtab.empty: string Symtab.table,
    3.16 -   loaded_theories = Symtab.empty: Path.T Symtab.table,
    3.17 +   loaded_theories = Symtab.empty: string Symtab.table,
    3.18     known_theories = Symtab.empty: Path.T Symtab.table};
    3.19  
    3.20  val global_session_base =
    3.21 @@ -56,7 +56,7 @@
    3.22          if default_qualifier <> "" then default_qualifier
    3.23          else #default_qualifier init_session_base,
    3.24         global_theories = Symtab.make global_theories,
    3.25 -       loaded_theories = Symtab.make (map (apsnd Path.explode) loaded_theories),
    3.26 +       loaded_theories = Symtab.make loaded_theories,
    3.27         known_theories = Symtab.make (map (apsnd Path.explode) known_theories)});
    3.28  
    3.29  fun reset_session_base () =
    3.30 @@ -108,20 +108,24 @@
    3.31      SOME qualifier => qualifier
    3.32    | NONE => Long_Name.qualifier theory);
    3.33  
    3.34 +fun theory_name qualifier theory0 =
    3.35 +  (case loaded_theory theory0 of
    3.36 +    SOME theory => (true, theory)
    3.37 +  | NONE =>
    3.38 +      (false,
    3.39 +        if Long_Name.is_qualified theory0 orelse is_some (global_theory theory0)
    3.40 +          orelse true (* FIXME *) then theory0
    3.41 +        else Long_Name.qualify qualifier theory0));
    3.42 +
    3.43  fun import_name qualifier dir s =
    3.44    let
    3.45 -    val theory0 = Thy_Header.import_name s;
    3.46 -    val theory =
    3.47 -      if Long_Name.is_qualified theory0 orelse is_some (global_theory theory0)
    3.48 -        orelse true (* FIXME *) then theory0
    3.49 -      else Long_Name.qualify qualifier theory0;
    3.50 +    val (loaded, theory) = theory_name qualifier (Thy_Header.import_name s);
    3.51      val node_name =
    3.52 -      the (get_first (fn e => e ())
    3.53 -        [fn () => loaded_theory theory,
    3.54 -         fn () => loaded_theory theory0,
    3.55 -         fn () => known_theory theory,
    3.56 -         fn () => known_theory theory0,
    3.57 -         fn () => SOME (File.full_path dir (thy_path (Path.expand (Path.explode s))))])
    3.58 +      if loaded then Path.basic theory
    3.59 +      else
    3.60 +        (case known_theory theory of
    3.61 +          SOME node_name => node_name
    3.62 +        | NONE => File.full_path dir (thy_path (Path.expand (Path.explode s))));
    3.63    in {node_name = node_name, master_dir = Path.dir node_name, theory_name = theory} end;
    3.64  
    3.65  fun check_file dir file = File.check_file (File.full_path dir file);
     4.1 --- a/src/Pure/PIDE/resources.scala	Wed Apr 12 21:13:43 2017 +0200
     4.2 +++ b/src/Pure/PIDE/resources.scala	Wed Apr 12 22:32:55 2017 +0200
     4.3 @@ -70,23 +70,30 @@
     4.4    def theory_qualifier(name: Document.Node.Name): String =
     4.5      session_base.global_theories.getOrElse(name.theory, Long_Name.qualifier(name.theory))
     4.6  
     4.7 +  def theory_name(qualifier: String, theory0: String): (Boolean, String) =
     4.8 +    session_base.loaded_theories.get(theory0) match {
     4.9 +      case Some(theory) => (true, theory)
    4.10 +      case None =>
    4.11 +        val theory =
    4.12 +          if (Long_Name.is_qualified(theory0) || session_base.global_theories.isDefinedAt(theory0)
    4.13 +              || true /* FIXME */) theory0
    4.14 +          else Long_Name.qualify(qualifier, theory0)
    4.15 +        (false, theory)
    4.16 +    }
    4.17 +
    4.18    def import_name(qualifier: String, dir: String, s: String): Document.Node.Name =
    4.19    {
    4.20 -    val theory0 = Thy_Header.import_name(s)
    4.21 -    val theory =
    4.22 -      if (Long_Name.is_qualified(theory0) || session_base.global_theories.isDefinedAt(theory0)
    4.23 -        || true /* FIXME */) theory0
    4.24 -      else Long_Name.qualify(qualifier, theory0)
    4.25 -
    4.26 -    session_base.loaded_theories.get(theory) orElse
    4.27 -    session_base.loaded_theories.get(theory0) orElse
    4.28 -    session_base.known_theories.get(theory) orElse
    4.29 -    session_base.known_theories.get(theory0) getOrElse {
    4.30 -      val path = Path.explode(s)
    4.31 -      val node = append(dir, thy_path(path))
    4.32 -      val master_dir = append(dir, path.dir)
    4.33 -      Document.Node.Name(node, master_dir, theory)
    4.34 -    }
    4.35 +    val (loaded, theory) = theory_name(qualifier, Thy_Header.import_name(s))
    4.36 +    if (loaded) Document.Node.Name.loaded_theory(theory)
    4.37 +    else
    4.38 +      session_base.known_theories.get(theory) match {
    4.39 +        case Some(node_name) => node_name
    4.40 +        case None =>
    4.41 +          val path = Path.explode(s)
    4.42 +          val node = append(dir, thy_path(path))
    4.43 +          val master_dir = append(dir, path.dir)
    4.44 +          Document.Node.Name(node, master_dir, theory)
    4.45 +      }
    4.46    }
    4.47  
    4.48    def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
     5.1 --- a/src/Pure/Thy/sessions.scala	Wed Apr 12 21:13:43 2017 +0200
     5.2 +++ b/src/Pure/Thy/sessions.scala	Wed Apr 12 22:32:55 2017 +0200
     5.3 @@ -85,7 +85,7 @@
     5.4  
     5.5    sealed case class Base(
     5.6      global_theories: Map[String, String] = Map.empty,
     5.7 -    loaded_theories: Map[String, Document.Node.Name] = Map.empty,
     5.8 +    loaded_theories: Map[String, String] = Map.empty,
     5.9      known_theories: Map[String, Document.Node.Name] = Map.empty,
    5.10      known_theories_local: Map[String, Document.Node.Name] = Map.empty,
    5.11      known_files: Map[JFile, List[Document.Node.Name]] = Map.empty,
    5.12 @@ -96,8 +96,6 @@
    5.13    {
    5.14      def platform_path: Base =
    5.15        copy(
    5.16 -        loaded_theories =
    5.17 -          for ((a, b) <- loaded_theories) yield (a, b.map(File.platform_path(_))),
    5.18          known_theories =
    5.19            for ((a, b) <- known_theories) yield (a, b.map(File.platform_path(_))),
    5.20          known_theories_local =
    5.21 @@ -108,10 +106,6 @@
    5.22      def loaded_theory(name: Document.Node.Name): Boolean =
    5.23        loaded_theories.isDefinedAt(name.theory)
    5.24  
    5.25 -    def dest_loaded_theories: List[(String, String)] =
    5.26 -      for ((theory, node_name) <- loaded_theories.toList)
    5.27 -        yield (theory, node_name.node)
    5.28 -
    5.29      def dest_known_theories: List[(String, String)] =
    5.30        for ((theory, node_name) <- known_theories.toList)
    5.31          yield (theory, node_name.node)
     6.1 --- a/src/Pure/Thy/thy_info.scala	Wed Apr 12 21:13:43 2017 +0200
     6.2 +++ b/src/Pure/Thy/thy_info.scala	Wed Apr 12 22:32:55 2017 +0200
     6.3 @@ -80,12 +80,12 @@
     6.4      lazy val syntax: Outer_Syntax =
     6.5        resources.session_base.syntax.add_keywords(keywords).add_abbrevs(abbrevs)
     6.6  
     6.7 -    def loaded_theories: Map[String, Document.Node.Name] =
     6.8 +    def loaded_theories: Map[String, String] =
     6.9        (resources.session_base.loaded_theories /: rev_deps) {
    6.10          case (loaded, dep) =>
    6.11 -          val name = dep.name.loaded_theory
    6.12 -          loaded + (name.theory -> name) +
    6.13 -            (name.theory_base_name -> name)  // legacy
    6.14 +          val name = dep.name
    6.15 +          loaded + (name.theory -> name.theory) +
    6.16 +            (name.theory_base_name -> name.theory)  // legacy
    6.17        }
    6.18  
    6.19      def loaded_files: List[Path] =
     7.1 --- a/src/Pure/Tools/build.scala	Wed Apr 12 21:13:43 2017 +0200
     7.2 +++ b/src/Pure/Tools/build.scala	Wed Apr 12 22:32:55 2017 +0200
     7.3 @@ -205,14 +205,14 @@
     7.4                  pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string,
     7.5                  pair(string, pair(string, pair(string, pair(Path.encode,
     7.6                  pair(list(pair(Options.encode, list(string))),
     7.7 -                pair(list(pair(string, string)),
     7.8 -                pair(list(pair(string, string)), list(pair(string, string))))))))))))))))(
     7.9 +                pair(list(pair(string, string)), pair(list(pair(string, string)),
    7.10 +                list(pair(string, string))))))))))))))))(
    7.11                (Symbol.codes, (command_timings, (do_output, (verbose,
    7.12                  (store.browser_info, (info.document_files, (File.standard_path(graph_file),
    7.13                  (parent, (info.chapter, (name, (Path.current,
    7.14                  (info.theories,
    7.15 -                (base.global_theories.toList,
    7.16 -                (base.dest_loaded_theories, base.dest_known_theories)))))))))))))))
    7.17 +                (base.global_theories.toList, (base.loaded_theories.toList,
    7.18 +                base.dest_known_theories)))))))))))))))
    7.19              })
    7.20  
    7.21          val env =
     8.1 --- a/src/Pure/Tools/ml_process.scala	Wed Apr 12 21:13:43 2017 +0200
     8.2 +++ b/src/Pure/Tools/ml_process.scala	Wed Apr 12 22:32:55 2017 +0200
     8.3 @@ -101,7 +101,7 @@
     8.4                  ML_Syntax.print_string, ML_Syntax.print_string))(table)
     8.5            List("Resources.set_session_base {default_qualifier = \"\"" +
     8.6              ", global_theories = " + print_table(base.global_theories.toList) +
     8.7 -            ", loaded_theories = " + print_table(base.dest_loaded_theories) +
     8.8 +            ", loaded_theories = " + print_table(base.loaded_theories.toList) +
     8.9              ", known_theories = " + print_table(base.dest_known_theories) + "}")
    8.10        }
    8.11  
     9.1 --- a/src/Tools/VSCode/src/vscode_resources.scala	Wed Apr 12 21:13:43 2017 +0200
     9.2 +++ b/src/Tools/VSCode/src/vscode_resources.scala	Wed Apr 12 22:32:55 2017 +0200
     9.3 @@ -63,9 +63,9 @@
     9.4    def node_name(file: JFile): Document.Node.Name =
     9.5    {
     9.6      val node = file.getPath
     9.7 -    val theory = Thy_Header.theory_name(node)
     9.8 -    val master_dir = if (theory == "") "" else file.getParent
     9.9 -    Document.Node.Name(node, master_dir, theory)
    9.10 +    val (loaded, theory) = theory_name(default_qualifier, Thy_Header.theory_name(node))
    9.11 +    if (loaded) Document.Node.Name.loaded_theory(theory)
    9.12 +    else Document.Node.Name(node, if (theory == "") "" else file.getParent, theory)
    9.13    }
    9.14  
    9.15    override def append(dir: String, source_path: Path): String =
    10.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Wed Apr 12 21:13:43 2017 +0200
    10.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Wed Apr 12 22:32:55 2017 +0200
    10.3 @@ -29,9 +29,9 @@
    10.4    {
    10.5      val vfs = VFSManager.getVFSForPath(path)
    10.6      val node = if (vfs.isInstanceOf[FileVFS]) MiscUtilities.resolveSymlinks(path) else path
    10.7 -    val theory = Thy_Header.theory_name(node)
    10.8 -    val master_dir = if (theory == "") "" else vfs.getParentOfPath(path)
    10.9 -    Document.Node.Name(node, master_dir, theory)
   10.10 +    val (loaded, theory) = theory_name(default_qualifier, Thy_Header.theory_name(node))
   10.11 +    if (loaded) Document.Node.Name.loaded_theory(theory)
   10.12 +    else Document.Node.Name(node, if (theory == "") "" else vfs.getParentOfPath(path), theory)
   10.13    }
   10.14  
   10.15    def node_name(buffer: Buffer): Document.Node.Name =