# HG changeset patch
# User wenzelm
# Date 1482316865 -3600
# Node ID f9470490e6822d406cd48f7aaa9b18b9d792cac3
# Parent  bad5de3f9554e168cd2c0ad1315f62785aab3c1b
clarified node_name: preserve original uri;

diff -r bad5de3f9554 -r f9470490e682 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)
   }
 }