prefer formal name from session context, for proper qualified theory name;
authorwenzelm
Mon Apr 17 21:48:53 2017 +0200 (2017-04-17 ago)
changeset 65501b42743f5b595
parent 65500 a6644e0e8728
child 65502 c05bec5d01ad
prefer formal name from session context, for proper qualified theory name;
src/Tools/VSCode/src/vscode_resources.scala
src/Tools/jEdit/src/jedit_resources.scala
     1.1 --- a/src/Tools/VSCode/src/vscode_resources.scala	Mon Apr 17 21:26:23 2017 +0200
     1.2 +++ b/src/Tools/VSCode/src/vscode_resources.scala	Mon Apr 17 21:48:53 2017 +0200
     1.3 @@ -61,15 +61,15 @@
     1.4    def node_file(name: Document.Node.Name): JFile = new JFile(name.node)
     1.5  
     1.6    def node_name(file: JFile): Document.Node.Name =
     1.7 -  {
     1.8 -    val node = file.getPath
     1.9 -    theory_name(default_qualifier, Thy_Header.theory_name(node)) match {
    1.10 -      case (true, theory) => Document.Node.Name.loaded_theory(theory)
    1.11 -      case (false, theory) =>
    1.12 -        val master_dir = if (theory == "") "" else file.getParent
    1.13 -        Document.Node.Name(node, master_dir, theory)
    1.14 +    session_base.known_file(file) getOrElse {
    1.15 +      val node = file.getPath
    1.16 +      theory_name(default_qualifier, Thy_Header.theory_name(node)) match {
    1.17 +        case (true, theory) => Document.Node.Name.loaded_theory(theory)
    1.18 +        case (false, theory) =>
    1.19 +          val master_dir = if (theory == "") "" else file.getParent
    1.20 +          Document.Node.Name(node, master_dir, theory)
    1.21 +      }
    1.22      }
    1.23 -  }
    1.24  
    1.25    override def append(dir: String, source_path: Path): String =
    1.26    {
     2.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Mon Apr 17 21:26:23 2017 +0200
     2.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Mon Apr 17 21:48:53 2017 +0200
     2.3 @@ -25,17 +25,20 @@
     2.4  {
     2.5    /* document node name */
     2.6  
     2.7 +  def known_file(path: String): Option[Document.Node.Name] =
     2.8 +    JEdit_Lib.check_file(path).flatMap(session_base.known_file(_))
     2.9 +
    2.10    def node_name(path: String): Document.Node.Name =
    2.11 -  {
    2.12 -    val vfs = VFSManager.getVFSForPath(path)
    2.13 -    val node = if (vfs.isInstanceOf[FileVFS]) MiscUtilities.resolveSymlinks(path) else path
    2.14 -    theory_name(default_qualifier, Thy_Header.theory_name(node)) match {
    2.15 -      case (true, theory) => Document.Node.Name.loaded_theory(theory)
    2.16 -      case (false, theory) =>
    2.17 -        val master_dir = if (theory == "") "" else vfs.getParentOfPath(path)
    2.18 -        Document.Node.Name(node, master_dir, theory)
    2.19 +    known_file(path) getOrElse {
    2.20 +      val vfs = VFSManager.getVFSForPath(path)
    2.21 +      val node = if (vfs.isInstanceOf[FileVFS]) MiscUtilities.resolveSymlinks(path) else path
    2.22 +      theory_name(default_qualifier, Thy_Header.theory_name(node)) match {
    2.23 +        case (true, theory) => Document.Node.Name.loaded_theory(theory)
    2.24 +        case (false, theory) =>
    2.25 +          val master_dir = if (theory == "") "" else vfs.getParentOfPath(path)
    2.26 +          Document.Node.Name(node, master_dir, theory)
    2.27 +      }
    2.28      }
    2.29 -  }
    2.30  
    2.31    def node_name(buffer: Buffer): Document.Node.Name =
    2.32      node_name(JEdit_Lib.buffer_name(buffer))