clarified node_name: preserve original uri;
authorwenzelm
Wed, 21 Dec 2016 11:41:05 +0100
changeset 64640 f9470490e682
parent 64639 bad5de3f9554
child 64641 7b9196394b32
clarified node_name: preserve original uri;
src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Wed Dec 21 11:21:46 2016 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Wed Dec 21 11:41:05 2016 +0100
@@ -34,10 +34,10 @@
 {
   def node_name(uri: String): Document.Node.Name =
   {
-    val file = VSCode_Resources.canonical_file(uri)  // FIXME wellformed!?
-    val node = file.getPath
-    val theory = Thy_Header.thy_name_bootstrap(node).getOrElse("")
-    val master_dir = if (theory == "") "" else file.getParent
-    Document.Node.Name(node, master_dir, theory)
+    val theory = Thy_Header.thy_name(uri).getOrElse("")
+    val master_dir =
+      if (!VSCode_Resources.is_wellformed(uri) || theory == "") ""
+      else VSCode_Resources.canonical_file(uri).getParent
+    Document.Node.Name(uri, master_dir, theory)
   }
 }