# HG changeset patch
# User wenzelm
# Date 1488578652 -3600
# Node ID ed2e33653438c6e37caba2fe6d70aae8bdd73dcf
# Parent  27d376c33c021a621c8076938f9ad5f9ce113ac2
more robust Uri comparison, notably on Windows;

diff -r 27d376c33c02 -r ed2e33653438 src/Tools/VSCode/extension/src/decorations.ts
--- a/src/Tools/VSCode/extension/src/decorations.ts	Fri Mar 03 21:56:52 2017 +0100
+++ b/src/Tools/VSCode/extension/src/decorations.ts	Fri Mar 03 23:04:12 2017 +0100
@@ -44,9 +44,10 @@
 {
   let typ = types[decoration.type]
   if (typ) {
+    let uri = Uri.parse(decoration.uri).toString()
     let editor =
       vscode.window.visibleTextEditors.find(
-        function (editor) { return decoration.uri == editor.document.uri.toString() })
+        function (editor) { return uri == editor.document.uri.toString() })
     if (editor) editor.setDecorations(typ, decoration.content)
   }
 }
\ No newline at end of file