clarified Document.Node.Name (again): canonical platform file;
identify document models by native java.io.File;

--- a/src/Pure/General/url.scala	Wed Jan 04 15:20:54 2017 +0100
+++ b/src/Pure/General/url.scala	Wed Jan 04 19:42:08 2017 +0100
@@ -52,8 +52,8 @@
 
   /* file URIs */
 
-  def print_file(file: JFile): String =
-    file.toPath.toAbsolutePath.toUri.normalize.toString
+  def print_file(file: JFile): String = file.toPath.toAbsolutePath.toUri.normalize.toString
+  def print_file_name(name: String): String = print_file(new JFile(name))
 
   def parse_file(uri: String): JFile = Paths.get(new URI(uri)).toFile
 
@@ -61,6 +61,6 @@
     try { parse_file(uri); true }
     catch { case _: URISyntaxException | _: IllegalArgumentException => false }
 
-  def normalize_file(uri: String): String =
-    if (is_wellformed_file(uri)) print_file(parse_file(uri)) else uri
+  def canonical_file(uri: String): JFile = parse_file(uri).getCanonicalFile
+  def canonical_file_name(uri: String): String = canonical_file(uri).getPath
 }

--- a/src/Pure/Thy/thy_header.scala	Wed Jan 04 15:20:54 2017 +0100
+++ b/src/Pure/Thy/thy_header.scala	Wed Jan 04 19:42:08 2017 +0100
@@ -77,13 +77,9 @@
   val ml_roots = List("ROOT0.ML" -> "ML_Root0", "ROOT.ML" -> ML_ROOT)
   val bootstrap_thys = List(PURE, ML_BOOTSTRAP).map(a => a -> ("Bootstrap_" + a))
 
-  private val Dir_Name = new Regex("""(.*?)[^/\\:]+""")
   private val Base_Name = new Regex(""".*?([^/\\:]+)""")
   private val Thy_Name = new Regex(""".*?([^/\\:]+)\.thy""")
 
-  def dir_name(s: String): String =
-    s match { case Dir_Name(name) => name case _ => "" }
-
   def base_name(s: String): String =
     s match { case Base_Name(name) => name case _ => error("Malformed import: " + quote(s)) }
 

--- a/src/Tools/VSCode/src/channel.scala	Wed Jan 04 15:20:54 2017 +0100
+++ b/src/Tools/VSCode/src/channel.scala	Wed Jan 04 19:42:08 2017 +0100
@@ -9,7 +9,7 @@
 
 import isabelle._
 
-import java.io.{InputStream, OutputStream, FileOutputStream, ByteArrayOutputStream}
+import java.io.{InputStream, OutputStream, FileOutputStream, ByteArrayOutputStream, File => JFile}
 
 import scala.collection.mutable
 
@@ -111,6 +111,6 @@
 
   /* diagnostics */
 
-  def diagnostics(uri: String, diagnostics: List[Protocol.Diagnostic]): Unit =
-    write(Protocol.PublishDiagnostics(uri, diagnostics))
+  def diagnostics(file: JFile, diagnostics: List[Protocol.Diagnostic]): Unit =
+    write(Protocol.PublishDiagnostics(file, diagnostics))
 }

--- a/src/Tools/VSCode/src/document_model.scala	Wed Jan 04 15:20:54 2017 +0100
+++ b/src/Tools/VSCode/src/document_model.scala	Wed Jan 04 19:42:08 2017 +0100
@@ -16,10 +16,9 @@
 
 object Document_Model
 {
-  def init(session: Session, uri: String): Document_Model =
+  def init(session: Session, node_name: Document.Node.Name): Document_Model =
   {
     val resources = session.resources.asInstanceOf[VSCode_Resources]
-    val node_name = resources.node_name(uri)
     val doc = Line.Document("", resources.text_length)
     Document_Model(session, node_name, doc)
   }
@@ -39,22 +38,13 @@
 
   override def toString: String = node_name.toString
 
-  def uri: String = node_name.node
   def is_theory: Boolean = node_name.is_theory
 
 
   /* external file */
 
-  val file: JFile = Url.parse_file(uri).getCanonicalFile
-
   def external(b: Boolean): Document_Model = copy(external_file = b)
 
-  def register(watcher: File_Watcher)
-  {
-    val dir = file.getParentFile
-    if (dir != null && dir.isDirectory) watcher.register(dir)
-  }
-
 
   /* header */
 
@@ -94,13 +84,6 @@
     }
   }
 
-  def update_file: Option[Document_Model] =
-    if (external_file) {
-      try { update_text(File.read(file)) }
-      catch { case ERROR(_) => None }
-    }
-    else None
-
   def flush_edits: Option[(List[Document.Edit_Text], Document_Model)] =
   {
     val perspective = node_perspective

--- a/src/Tools/VSCode/src/protocol.scala	Wed Jan 04 15:20:54 2017 +0100
+++ b/src/Tools/VSCode/src/protocol.scala	Wed Jan 04 19:42:08 2017 +0100
@@ -11,6 +11,9 @@
 import isabelle._
 
 
+import java.io.{File => JFile}
+
+
 object Protocol
 {
   /* abstract message */
@@ -180,14 +183,14 @@
   object Location
   {
     def apply(loc: Line.Node_Range): JSON.T =
-      Map("uri" -> loc.name, "range" -> Range(loc.range))
+      Map("uri" -> Url.print_file_name(loc.name), "range" -> Range(loc.range))
 
     def unapply(json: JSON.T): Option[Line.Node_Range] =
       for {
         uri <- JSON.string(json, "uri")
         range_json <- JSON.value(json, "range")
         range <- Range.unapply(range_json)
-      } yield Line.Node_Range(uri, range)
+      } yield Line.Node_Range(Url.canonical_file_name(uri), range)
   }
 
   object TextDocumentPosition
@@ -198,7 +201,7 @@
         uri <- JSON.string(doc, "uri")
         pos_json <- JSON.value(json, "position")
         pos <- Position.unapply(pos_json)
-      } yield Line.Node_Position(uri, pos)
+      } yield Line.Node_Position(Url.canonical_file_name(uri), pos)
   }
 
 
@@ -224,7 +227,7 @@
 
   object DidOpenTextDocument
   {
-    def unapply(json: JSON.T): Option[(String, String, Long, String)] =
+    def unapply(json: JSON.T): Option[(JFile, String, Long, String)] =
       json match {
         case Notification("textDocument/didOpen", Some(params)) =>
           for {
@@ -233,7 +236,7 @@
             lang <- JSON.string(doc, "languageId")
             version <- JSON.long(doc, "version")
             text <- JSON.string(doc, "text")
-          } yield (uri, lang, version, text)
+          } yield (Url.canonical_file(uri), lang, version, text)
         case _ => None
       }
   }
@@ -259,7 +262,7 @@
 
   object DidChangeTextDocument
   {
-    def unapply(json: JSON.T): Option[(String, Long, List[TextDocumentContentChange])] =
+    def unapply(json: JSON.T): Option[(JFile, Long, List[TextDocumentContentChange])] =
       json match {
         case Notification("textDocument/didChange", Some(params)) =>
           for {
@@ -267,20 +270,20 @@
             uri <- JSON.string(doc, "uri")
             version <- JSON.long(doc, "version")
             changes <- JSON.array(params, "contentChanges", TextDocumentContentChange.unapply _)
-          } yield (uri, version, changes)
+          } yield (Url.canonical_file(uri), version, changes)
         case _ => None
       }
   }
 
   class TextDocumentNotification(name: String)
   {
-    def unapply(json: JSON.T): Option[String] =
+    def unapply(json: JSON.T): Option[JFile] =
       json match {
         case Notification(method, Some(params)) if method == name =>
           for {
             doc <- JSON.value(params, "textDocument")
             uri <- JSON.string(doc, "uri")
-          } yield uri
+          } yield Url.canonical_file(uri)
         case _ => None
       }
   }
@@ -363,8 +366,8 @@
 
   object PublishDiagnostics
   {
-    def apply(uri: String, diagnostics: List[Diagnostic]): JSON.T =
+    def apply(file: JFile, diagnostics: List[Diagnostic]): JSON.T =
       Notification("textDocument/publishDiagnostics",
-        Map("uri" -> uri, "diagnostics" -> diagnostics.map(_.json)))
+        Map("uri" -> Url.print_file(file), "diagnostics" -> diagnostics.map(_.json)))
   }
 }

--- a/src/Tools/VSCode/src/server.scala	Wed Jan 04 15:20:54 2017 +0100
+++ b/src/Tools/VSCode/src/server.scala	Wed Jan 04 19:42:08 2017 +0100
@@ -102,7 +102,7 @@
 
   def rendering_offset(node_pos: Line.Node_Position): Option[(VSCode_Rendering, Text.Offset)] =
     for {
-      model <- resources.get_model(node_pos.name)
+      model <- resources.get_model(new JFile(node_pos.name))
       rendering = model.rendering()
       offset <- model.doc.offset(node_pos.pos)
     } yield (rendering, offset)
@@ -124,18 +124,19 @@
   private def sync_documents(changed: Set[JFile]): Unit =
     if (resources.sync_models(changed)) delay_input.invoke()
 
-  private def update_document(uri: String, text: String)
+  private def update_document(file: JFile, text: String)
   {
-    resources.update_model(session, uri, text)
+    resources.update_model(session, file, text)
     delay_input.invoke()
   }
 
-  private def close_document(uri: String)
+  private def close_document(file: JFile)
   {
-    resources.close_model(uri) match {
+    resources.close_model(file) match {
       case Some(model) =>
-        model.register(watcher)
-        sync_documents(Set(model.file))
+        val dir = file.getParentFile
+        if (dir != null && dir.isDirectory) watcher.register(dir)
+        sync_documents(Set(file))
       case None =>
     }
   }
@@ -153,7 +154,7 @@
   private val prover_output =
     Session.Consumer[Session.Commands_Changed](getClass.getName) {
       case changed if changed.nodes.nonEmpty =>
-        resources.update_output(changed.nodes.toList.map(_.node))
+        resources.update_output(changed.nodes.toList.map(resources.node_file(_)))
         delay_output.invoke()
       case _ =>
     }

--- a/src/Tools/VSCode/src/vscode_rendering.scala	Wed Jan 04 15:20:54 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Wed Jan 04 19:42:08 2017 +0100
@@ -84,11 +84,11 @@
       if Path.is_wellformed(name)
     }
     yield {
-      val file = Path.explode(name).file
+      val path = Path.explode(name)
       val opt_text =
-        try { Some(File.read(file)) } // FIXME content from resources/models
+        try { Some(File.read(path)) } // FIXME content from resources/models
         catch { case ERROR(_) => None }
-      Line.Node_Range(Url.print_file(file),
+      Line.Node_Range(File.platform_path(path),
         opt_text match {
           case Some(text) if range.start > 0 =>
             val chunk = Symbol.Text_Chunk(text)

--- a/src/Tools/VSCode/src/vscode_resources.scala	Wed Jan 04 15:20:54 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Wed Jan 04 19:42:08 2017 +0100
@@ -19,9 +19,9 @@
   /* internal state */
 
   sealed case class State(
-    models: Map[String, Document_Model] = Map.empty,
-    pending_input: Set[String] = Set.empty,
-    pending_output: Set[String] = Set.empty)
+    models: Map[JFile, Document_Model] = Map.empty,
+    pending_input: Set[JFile] = Set.empty,
+    pending_output: Set[JFile] = Set.empty)
 }
 
 class VSCode_Resources(
@@ -38,63 +38,65 @@
 
   /* document node name */
 
-  def node_name(uri: String): Document.Node.Name =
+  def node_file(name: Document.Node.Name): JFile = new JFile(name.node)
+
+  def node_name(file: JFile): Document.Node.Name =
   {
-    val theory = Thy_Header.thy_name_bootstrap(uri).getOrElse("")
-    val master_dir =
-      if (!Url.is_wellformed_file(uri) || theory == "") ""
-      else Thy_Header.dir_name(uri)
-    Document.Node.Name(uri, master_dir, theory)
+    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)
   }
 
   override def append(dir: String, source_path: Path): String =
   {
     val path = source_path.expand
-    if (dir == "" || path.is_absolute) Url.print_file(path.file)
+    if (dir == "" || path.is_absolute) File.platform_path(path)
     else if (path.is_current) dir
-    else Url.normalize_file(dir + "/" + path.implode)
+    else if (path.is_basic && !dir.endsWith("/") && !dir.endsWith(JFile.separator))
+      dir + JFile.separator + File.platform_path(path)
+    else if (path.is_basic) dir + File.platform_path(path)
+    else new JFile(dir + JFile.separator + File.platform_path(path)).getCanonicalPath
   }
 
   override def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
   {
-    val uri = name.node
-    get_model(uri) match {
+    val file = node_file(name)
+    get_model(file) match {
       case Some(model) =>
-        val reader = new CharSequenceReader(model.doc.make_text)
-        f(reader)
-
-      case None =>
-        val file = Url.parse_file(uri)
-        if (!file.isFile) error("No such file: " + quote(file.toString))
-
+        f(new CharSequenceReader(model.doc.make_text))
+      case None if file.isFile =>
         val reader = Scan.byte_reader(file)
         try { f(reader) } finally { reader.close }
+      case None =>
+        error("No such file: " + quote(file.toString))
     }
   }
 
 
   /* document models */
 
-  def get_model(uri: String): Option[Document_Model] = state.value.models.get(uri)
+  def get_model(file: JFile): Option[Document_Model] = state.value.models.get(file)
+  def get_model(name: Document.Node.Name): Option[Document_Model] = get_model(node_file(name))
 
-  def update_model(session: Session, uri: String, text: String)
+  def update_model(session: Session, file: JFile, text: String)
   {
     state.change(st =>
       {
-        val model = st.models.getOrElse(uri, Document_Model.init(session, uri))
+        val model = st.models.getOrElse(file, Document_Model.init(session, node_name(file)))
         val model1 = (model.update_text(text) getOrElse model).external(false)
         st.copy(
-          models = st.models + (uri -> model1),
-          pending_input = st.pending_input + uri)
+          models = st.models + (file -> model1),
+          pending_input = st.pending_input + file)
       })
   }
 
-  def close_model(uri: String): Option[Document_Model] =
+  def close_model(file: JFile): Option[Document_Model] =
     state.change_result(st =>
-      st.models.get(uri) match {
+      st.models.get(file) match {
         case None => (None, st)
         case Some(model) =>
-          (Some(model), st.copy(models = st.models + (uri -> model.external(true))))
+          (Some(model), st.copy(models = st.models + (file -> model.external(true))))
       })
 
   def sync_models(changed_files: Set[JFile]): Boolean =
@@ -102,10 +104,12 @@
       {
         val changed_models =
           (for {
-            (uri, model) <- st.models.iterator
-            if changed_files(model.file)
-            model1 <- model.update_file
-          } yield (uri, model1)).toList
+            (file, model) <- st.models.iterator
+            if changed_files(file) && model.external_file
+            model1 <-
+              (try { model.update_text(File.read(file)) }
+               catch { case ERROR(_) => None })
+          } yield (file, model1)).toList
         if (changed_models.isEmpty) (false, st)
         else (true,
           st.copy(
@@ -129,16 +133,16 @@
         val loaded_models =
           (for {
             dep <- thy_info.dependencies("", thys).deps.iterator
-            uri = dep.name.node
-            if !st.models.isDefinedAt(uri)
+            file = node_file(dep.name)
+            if !st.models.isDefinedAt(file)
             text <-
-              try { Some(File.read(Url.parse_file(uri))) }
+              try { Some(File.read(file)) }
               catch { case ERROR(_) => None }
           }
           yield {
-            val model = Document_Model.init(session, uri)
+            val model = Document_Model.init(session, node_name(file))
             val model1 = (model.update_text(text) getOrElse model).external(true)
-            (uri, model1)
+            (file, model1)
           }).toList
 
         if (loaded_models.isEmpty) (false, st)
@@ -159,14 +163,14 @@
       {
         val changed_models =
           (for {
-            uri <- st.pending_input.iterator
-            model <- st.models.get(uri)
-            res <- model.flush_edits
-          } yield res).toList
+            file <- st.pending_input.iterator
+            model <- st.models.get(file)
+            (edits, model1) <- model.flush_edits
+          } yield (edits, (file, model1))).toList
 
         session.update(Document.Blobs.empty, changed_models.flatMap(_._1))
         st.copy(
-          models = (st.models /: changed_models) { case (ms, (_, m)) => ms + (m.uri -> m) },
+          models = (st.models /: changed_models.iterator.map(_._2))(_ + _),
           pending_input = Set.empty)
       })
   }
@@ -174,7 +178,7 @@
 
   /* pending output */
 
-  def update_output(changed_nodes: List[String]): Unit =
+  def update_output(changed_nodes: List[JFile]): Unit =
     state.change(st => st.copy(pending_output = st.pending_output ++ changed_nodes))
 
   def flush_output(channel: Channel)
@@ -183,16 +187,16 @@
       {
         val changed_iterator =
           for {
-            uri <- st.pending_output.iterator
-            model <- st.models.get(uri)
+            file <- st.pending_output.iterator
+            model <- st.models.get(file)
             rendering = model.rendering()
             (diagnostics, model1) <- model.publish_diagnostics(rendering)
           } yield {
-            channel.diagnostics(model1.uri, rendering.diagnostics_output(diagnostics))
-            model1
+            channel.diagnostics(file, rendering.diagnostics_output(diagnostics))
+            (file, model1)
           }
         st.copy(
-          models = (st.models /: changed_iterator) { case (ms, m) => ms + (m.uri -> m) },
+          models = (st.models /: changed_iterator)(_ + _),
           pending_output = Set.empty)
       }
     )