tuned;
authorwenzelm
Wed Apr 12 22:47:21 2017 +0200 (2017-04-12 ago)
changeset 65472f83081bcdd0e
parent 65471 05e5bffcf1d8
child 65473 b47373f52451
tuned;
src/Pure/PIDE/resources.scala
src/Tools/VSCode/src/vscode_resources.scala
src/Tools/jEdit/src/jedit_resources.scala
     1.1 --- a/src/Pure/PIDE/resources.scala	Wed Apr 12 22:32:55 2017 +0200
     1.2 +++ b/src/Pure/PIDE/resources.scala	Wed Apr 12 22:47:21 2017 +0200
     1.3 @@ -70,7 +70,7 @@
     1.4    def theory_qualifier(name: Document.Node.Name): String =
     1.5      session_base.global_theories.getOrElse(name.theory, Long_Name.qualifier(name.theory))
     1.6  
     1.7 -  def theory_name(qualifier: String, theory0: String): (Boolean, String) =
     1.8 +  def loaded_theory_name(qualifier: String, theory0: String): (Boolean, String) =
     1.9      session_base.loaded_theories.get(theory0) match {
    1.10        case Some(theory) => (true, theory)
    1.11        case None =>
    1.12 @@ -82,19 +82,18 @@
    1.13      }
    1.14  
    1.15    def import_name(qualifier: String, dir: String, s: String): Document.Node.Name =
    1.16 -  {
    1.17 -    val (loaded, theory) = theory_name(qualifier, Thy_Header.import_name(s))
    1.18 -    if (loaded) Document.Node.Name.loaded_theory(theory)
    1.19 -    else
    1.20 -      session_base.known_theories.get(theory) match {
    1.21 -        case Some(node_name) => node_name
    1.22 -        case None =>
    1.23 -          val path = Path.explode(s)
    1.24 -          val node = append(dir, thy_path(path))
    1.25 -          val master_dir = append(dir, path.dir)
    1.26 -          Document.Node.Name(node, master_dir, theory)
    1.27 -      }
    1.28 -  }
    1.29 +    loaded_theory_name(qualifier, Thy_Header.import_name(s)) match {
    1.30 +      case (true, theory) => Document.Node.Name.loaded_theory(theory)
    1.31 +      case (false, theory) =>
    1.32 +        session_base.known_theories.get(theory) match {
    1.33 +          case Some(node_name) => node_name
    1.34 +          case None =>
    1.35 +            val path = Path.explode(s)
    1.36 +            val node = append(dir, thy_path(path))
    1.37 +            val master_dir = append(dir, path.dir)
    1.38 +            Document.Node.Name(node, master_dir, theory)
    1.39 +        }
    1.40 +    }
    1.41  
    1.42    def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
    1.43    {
     2.1 --- a/src/Tools/VSCode/src/vscode_resources.scala	Wed Apr 12 22:32:55 2017 +0200
     2.2 +++ b/src/Tools/VSCode/src/vscode_resources.scala	Wed Apr 12 22:47:21 2017 +0200
     2.3 @@ -63,9 +63,12 @@
     2.4    def node_name(file: JFile): Document.Node.Name =
     2.5    {
     2.6      val node = file.getPath
     2.7 -    val (loaded, theory) = theory_name(default_qualifier, Thy_Header.theory_name(node))
     2.8 -    if (loaded) Document.Node.Name.loaded_theory(theory)
     2.9 -    else Document.Node.Name(node, if (theory == "") "" else file.getParent, theory)
    2.10 +    loaded_theory_name(default_qualifier, Thy_Header.theory_name(node)) match {
    2.11 +      case (true, theory) => Document.Node.Name.loaded_theory(theory)
    2.12 +      case (false, theory) =>
    2.13 +        val master_dir = if (theory == "") "" else file.getParent
    2.14 +        Document.Node.Name(node, master_dir, theory)
    2.15 +    }
    2.16    }
    2.17  
    2.18    override def append(dir: String, source_path: Path): String =
     3.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Wed Apr 12 22:32:55 2017 +0200
     3.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Wed Apr 12 22:47:21 2017 +0200
     3.3 @@ -29,9 +29,12 @@
     3.4    {
     3.5      val vfs = VFSManager.getVFSForPath(path)
     3.6      val node = if (vfs.isInstanceOf[FileVFS]) MiscUtilities.resolveSymlinks(path) else path
     3.7 -    val (loaded, theory) = theory_name(default_qualifier, Thy_Header.theory_name(node))
     3.8 -    if (loaded) Document.Node.Name.loaded_theory(theory)
     3.9 -    else Document.Node.Name(node, if (theory == "") "" else vfs.getParentOfPath(path), theory)
    3.10 +    loaded_theory_name(default_qualifier, Thy_Header.theory_name(node)) match {
    3.11 +      case (true, theory) => Document.Node.Name.loaded_theory(theory)
    3.12 +      case (false, theory) =>
    3.13 +        val master_dir = if (theory == "") "" else vfs.getParentOfPath(path)
    3.14 +        Document.Node.Name(node, master_dir, theory)
    3.15 +    }
    3.16    }
    3.17  
    3.18    def node_name(buffer: Buffer): Document.Node.Name =