diff -r e6a695d6a6b2 -r 1a9e2a2bf251 src/Pure/PIDE/resources.scala --- a/src/Pure/PIDE/resources.scala Mon Nov 06 16:03:13 2017 +0100 +++ b/src/Pure/PIDE/resources.scala Mon Nov 06 17:24:09 2017 +0100 @@ -19,8 +19,25 @@ { resources => + + /* theory files */ + def thy_path(path: Path): Path = path.ext("thy") + def thy_node_name(qualifier: String, file: JFile, bootstrap: Boolean = false) + : Document.Node.Name = + { + session_base.known.get_file(file, bootstrap) getOrElse { + val node = file.getPath + theory_name(qualifier, Thy_Header.theory_name(node)) match { + case (true, theory) => Document.Node.Name.loaded_theory(theory) + case (false, theory) => + val master_dir = if (theory == "") "" else file.getParent + Document.Node.Name(node, master_dir, theory) + } + } + } + /* file-system operations */