# HG changeset patch
# User wenzelm
# Date 1498825605 -7200
# Node ID d4fa51e7c4ffa7dd4782417bcdf5b760f132d865
# Parent  836898197296c15c9f9c1aabf601c3a8f97675cd
retain symlinks in file names from VSCode: relevant for proper file locations in decorations etc.;

diff -r 836898197296 -r d4fa51e7c4ff src/Pure/General/url.scala
--- a/src/Pure/General/url.scala	Fri Jun 30 14:19:37 2017 +0200
+++ b/src/Pure/General/url.scala	Fri Jun 30 14:26:45 2017 +0200
@@ -61,6 +61,9 @@
         false
     }
 
+  def absolute_file(uri: String): JFile = File.absolute(parse_file(uri))
+  def absolute_file_name(uri: String): String = absolute_file(uri).getPath
+
   def canonical_file(uri: String): JFile = File.canonical(parse_file(uri))
   def canonical_file_name(uri: String): String = canonical_file(uri).getPath
 }
diff -r 836898197296 -r d4fa51e7c4ff src/Tools/VSCode/src/protocol.scala
--- a/src/Tools/VSCode/src/protocol.scala	Fri Jun 30 14:19:37 2017 +0200
+++ b/src/Tools/VSCode/src/protocol.scala	Fri Jun 30 14:26:45 2017 +0200
@@ -207,7 +207,7 @@
         uri <- JSON.string(json, "uri")
         range_json <- JSON.value(json, "range")
         range <- Range.unapply(range_json)
-      } yield Line.Node_Range(Url.canonical_file_name(uri), range)
+      } yield Line.Node_Range(Url.absolute_file_name(uri), range)
   }
 
   object TextDocumentPosition
@@ -218,7 +218,7 @@
         uri <- JSON.string(doc, "uri")
         pos_json <- JSON.value(json, "position")
         pos <- Position.unapply(pos_json)
-      } yield Line.Node_Position(Url.canonical_file_name(uri), pos)
+      } yield Line.Node_Position(Url.absolute_file_name(uri), pos)
   }
 
 
@@ -280,7 +280,7 @@
             lang <- JSON.string(doc, "languageId")
             version <- JSON.long(doc, "version")
             text <- JSON.string(doc, "text")
-          } yield (Url.canonical_file(uri), lang, version, text)
+          } yield (Url.absolute_file(uri), lang, version, text)
         case _ => None
       }
   }
@@ -302,7 +302,7 @@
             uri <- JSON.string(doc, "uri")
             version <- JSON.long(doc, "version")
             changes <- JSON.array(params, "contentChanges", unapply_change _)
-          } yield (Url.canonical_file(uri), version, changes)
+          } yield (Url.absolute_file(uri), version, changes)
         case _ => None
       }
   }
@@ -315,7 +315,7 @@
           for {
             doc <- JSON.value(params, "textDocument")
             uri <- JSON.string(doc, "uri")
-          } yield Url.canonical_file(uri)
+          } yield Url.absolute_file(uri)
         case _ => None
       }
   }
@@ -497,7 +497,7 @@
               uri <- JSON.string(params, "uri")
               if Url.is_wellformed_file(uri)
               pos <- Position.unapply(params)
-            } yield (Url.canonical_file(uri), pos)
+            } yield (Url.absolute_file(uri), pos)
           Some(caret)
         case _ => None
       }
@@ -560,7 +560,7 @@
             uri <- JSON.string(params, "uri")
             if Url.is_wellformed_file(uri)
             column <- JSON.int(params, "column")
-          } yield (Url.canonical_file(uri), column)
+          } yield (Url.absolute_file(uri), column)
         case _ => None
       }
   }
diff -r 836898197296 -r d4fa51e7c4ff src/Tools/VSCode/src/vscode_rendering.scala
--- a/src/Tools/VSCode/src/vscode_rendering.scala	Fri Jun 30 14:19:37 2017 +0200
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Fri Jun 30 14:26:45 2017 +0200
@@ -254,7 +254,7 @@
     for {
       platform_path <- resources.source_file(source_name)
       file <-
-        (try { Some(File.canonical(new JFile(platform_path))) }
+        (try { Some(File.absolute(new JFile(platform_path))) }
          catch { case ERROR(_) => None })
     }
     yield {
diff -r 836898197296 -r d4fa51e7c4ff src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Fri Jun 30 14:19:37 2017 +0200
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Fri Jun 30 14:26:45 2017 +0200
@@ -109,7 +109,7 @@
     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 File.canonical_name(new JFile(dir + JFile.separator + File.platform_path(path)))
+    else File.absolute_name(new JFile(dir + JFile.separator + File.platform_path(path)))
   }
 
   def get_models: Map[JFile, Document_Model] = state.value.models