# HG changeset patch
# User wenzelm
# Date 1483473791 -3600
# Node ID 34ef44748370029f501bb0cc432f0daaabfeeb48
# Parent  3b33d2fc5fc01a66d96f0d914168f0061bb89e8e# Parent  f5c4ffdb1124a03bc65dc78f1760592d320ec321
merged

diff -r 3b33d2fc5fc0 -r 34ef44748370 src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Tue Jan 03 16:48:49 2017 +0000
+++ b/src/Pure/General/file.scala	Tue Jan 03 21:03:11 2017 +0100
@@ -33,7 +33,7 @@
     if (Platform.is_windows) {
       val Platform_Root = new Regex("(?i)" +
         Pattern.quote(Isabelle_System.cygwin_root()) + """(?:\\+|\z)(.*)""")
-      val Drive = new Regex("""([a-zA-Z]):\\*(.*)""")
+      val Drive = new Regex("""\\?([a-zA-Z]):\\*(.*)""")
 
       platform_path.replace('/', '\\') match {
         case Platform_Root(rest) => "/" + rest.replace('\\', '/')
@@ -48,6 +48,7 @@
   def standard_path(file: JFile): String = standard_path(file.getPath)
 
   def path(file: JFile): Path = Path.explode(standard_path(file))
+  def pwd(): Path = path(Path.current.file.toPath.toAbsolutePath.toFile)
 
   def standard_url(name: String): String =
     try {
diff -r 3b33d2fc5fc0 -r 34ef44748370 src/Pure/General/json.scala
--- a/src/Pure/General/json.scala	Tue Jan 03 16:48:49 2017 +0000
+++ b/src/Pure/General/json.scala	Tue Jan 03 21:03:11 2017 +0100
@@ -32,7 +32,19 @@
       def string(s: String)
       {
         result += '"'
-        result ++= scala.util.parsing.json.JSONFormat.quoteString(s)
+        result ++=
+          s.iterator.map {
+            case '"'  => "\\\""
+            case '\\' => "\\\\"
+            case '\b' => "\\b"
+            case '\f' => "\\f"
+            case '\n' => "\\n"
+            case '\r' => "\\r"
+            case '\t' => "\\t"
+            case c =>
+              if (c <= '\u001f' || c >= '\u007f' && c <= '\u009f') "\\u%04x".format(c.toInt)
+              else c
+          }.mkString
         result += '"'
       }
 
diff -r 3b33d2fc5fc0 -r 34ef44748370 src/Pure/General/url.scala
--- a/src/Pure/General/url.scala	Tue Jan 03 16:48:49 2017 +0000
+++ b/src/Pure/General/url.scala	Tue Jan 03 21:03:11 2017 +0100
@@ -57,6 +57,19 @@
     try { file(uri); true }
     catch { case _: URISyntaxException | _: IllegalArgumentException => false }
 
+  def normalize_file(uri: String): String =
+    if (is_wellformed_file(uri)) {
+      val uri1 = new URI(uri).normalize.toASCIIString
+      if (uri1.startsWith("file://")) uri1
+      else {
+        Library.try_unprefix("file:/", uri1) match {
+          case Some(p) => "file:///" + p
+          case None => uri1
+        }
+      }
+    }
+    else uri
+
   def platform_file(path: Path): String =
   {
     val path1 = path.expand
@@ -68,8 +81,6 @@
     if (name.startsWith("file://")) name
     else {
       val s = name.replaceAll(" ", "%20")
-      if (!Platform.is_windows) "file://" + s
-      else if (s.startsWith("\\\\")) "file:" + s.replace('\\', '/')
-      else "file:///" + s.replace('\\', '/')
+      "file://" + (if (Platform.is_windows) s.replace('\\', '/') else s)
     }
 }
diff -r 3b33d2fc5fc0 -r 34ef44748370 src/Pure/PIDE/line.scala
--- a/src/Pure/PIDE/line.scala	Tue Jan 03 16:48:49 2017 +0000
+++ b/src/Pure/PIDE/line.scala	Tue Jan 03 21:03:11 2017 +0100
@@ -125,8 +125,7 @@
       val c = pos.column
       if (0 <= l && l < lines.length) {
         val line_offset =
-          if (l == 0) 0
-          else (0 /: lines.iterator.take(l - 1)) { case (n, line) => n + text_length(line.text) + 1 }
+          (0 /: lines.iterator.take(l)) { case (n, line) => n + text_length(line.text) + 1 }
         text_length.offset(lines(l).text, c).map(line_offset + _)
       }
       else None
diff -r 3b33d2fc5fc0 -r 34ef44748370 src/Pure/PIDE/rendering.scala
--- a/src/Pure/PIDE/rendering.scala	Tue Jan 03 16:48:49 2017 +0000
+++ b/src/Pure/PIDE/rendering.scala	Tue Jan 03 21:03:11 2017 +0100
@@ -58,6 +58,8 @@
 
   private def pretty_typing(kind: String, body: XML.Body): XML.Tree =
     Pretty.block(XML.Text(kind) :: Pretty.brk(1) :: body)
+
+  val caret_focus_elements = Markup.Elements(Markup.ENTITY)
 }
 
 abstract class Rendering(
@@ -162,4 +164,53 @@
         Some(Text.Info(r, all_tips))
     }
   }
+
+
+  /* caret focus */
+
+  private def entity_focus(range: Text.Range,
+    check: (Boolean, Long) => Boolean = (is_def: Boolean, i: Long) => is_def): Set[Long] =
+  {
+    val results =
+      snapshot.cumulate[Set[Long]](range, Set.empty, Rendering.caret_focus_elements, _ =>
+          {
+            case (serials, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
+              props match {
+                case Markup.Entity.Def(i) if check(true, i) => Some(serials + i)
+                case Markup.Entity.Ref(i) if check(false, i) => Some(serials + i)
+                case _ => None
+              }
+            case _ => None
+          })
+    (Set.empty[Long] /: results){ case (s1, Text.Info(_, s2)) => s1 ++ s2 }
+  }
+
+  def caret_focus(caret_range: Text.Range, visible_range: Text.Range): Set[Long] =
+  {
+    val focus_defs = entity_focus(caret_range)
+    if (focus_defs.nonEmpty) focus_defs
+    else {
+      val visible_defs = entity_focus(visible_range)
+      entity_focus(caret_range, (is_def: Boolean, i: Long) => !is_def && visible_defs.contains(i))
+    }
+  }
+
+  def caret_focus_ranges(caret_range: Text.Range, visible_range: Text.Range): List[Text.Range] =
+  {
+    val focus = caret_focus(caret_range, visible_range)
+    if (focus.nonEmpty) {
+      val results =
+        snapshot.cumulate[Boolean](visible_range, false, Rendering.caret_focus_elements, _ =>
+          {
+            case (_, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
+              props match {
+                case Markup.Entity.Def(i) if focus(i) => Some(true)
+                case Markup.Entity.Ref(i) if focus(i) => Some(true)
+                case _ => None
+              }
+          })
+      for (info <- results if info.info) yield info.range
+    }
+    else Nil
+  }
 }
diff -r 3b33d2fc5fc0 -r 34ef44748370 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Tue Jan 03 16:48:49 2017 +0000
+++ b/src/Pure/PIDE/resources.scala	Tue Jan 03 21:03:11 2017 +0100
@@ -48,10 +48,6 @@
     if (Path.is_valid(raw_name)) append(dir, Path.explode(raw_name))
     else raw_name
 
-  def append_file_url(dir: String, raw_name: String): String =
-    if (Path.is_valid(raw_name)) "file://" + append(dir, Path.explode(raw_name))
-    else raw_name
-
 
 
   /* source files of Isabelle/ML bootstrap */
diff -r 3b33d2fc5fc0 -r 34ef44748370 src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Tue Jan 03 16:48:49 2017 +0000
+++ b/src/Pure/Thy/thy_header.scala	Tue Jan 03 21:03:11 2017 +0100
@@ -77,9 +77,13 @@
   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)) }
 
diff -r 3b33d2fc5fc0 -r 34ef44748370 src/Tools/VSCode/extension/isabelle-language.json
--- a/src/Tools/VSCode/extension/isabelle-language.json	Tue Jan 03 16:48:49 2017 +0000
+++ b/src/Tools/VSCode/extension/isabelle-language.json	Tue Jan 03 21:03:11 2017 +0100
@@ -1,18 +1,48 @@
 {
-    "brackets": [
-        ["(", ")"],
-        ["[", "]"],
-        ["{", "}"],
-        ["«", "»"],
-        ["‹", "›"],
-        ["⟨", "⟩"],
-        ["⌈", "⌉"],
-        ["⌊", "⌋"],
-        ["⦇", "⦈"],
-        ["⟦", "⟧"],
-        ["⦃", "⦄"]
-    ],
-    "comments": {
-        "blockComment": [ "(*", "*)" ]
-    }
+  "comments": {
+    "blockComment": ["(*", "*)"]
+  },
+  "brackets": [
+    ["(", ")"],
+    ["[", "]"],
+    ["{", "}"],
+    ["«", "»"],
+    ["‹", "›"],
+    ["⟨", "⟩"],
+    ["⌈", "⌉"],
+    ["⌊", "⌋"],
+    ["⦇", "⦈"],
+    ["⟦", "⟧"],
+    ["⦃", "⦄"]
+  ],
+  "autoClosingPairs": [
+    { "open": "(", "close": ")" },
+    { "open": "[", "close": "]" },
+    { "open": "{", "close": "}" },
+    { "open": "«", "close": "»" },
+    { "open": "‹", "close": "›" },
+    { "open": "⟨", "close": "⟩" },
+    { "open": "⌈", "close": "⌉" },
+    { "open": "⌊", "close": "⌋" },
+    { "open": "⦇", "close": "⦈" },
+    { "open": "⟦", "close": "⟧" },
+    { "open": "⦃", "close": "⦄" },
+    { "open": "`", "close": "`", "notIn": ["string"] },
+    { "open": "\"", "close": "\"", "notIn": ["string"] }
+  ],
+  "surroundingPairs": [
+    ["(", ")"],
+    ["[", "]"],
+    ["{", "}"],
+    ["«", "»"],
+    ["‹", "›"],
+    ["⟨", "⟩"],
+    ["⌈", "⌉"],
+    ["⌊", "⌋"],
+    ["⦇", "⦈"],
+    ["⟦", "⟧"],
+    ["⦃", "⦄"],
+    ["`", "`"],
+    ["\"", "\""]
+  ]
 }
diff -r 3b33d2fc5fc0 -r 34ef44748370 src/Tools/VSCode/extension/isabelle-ml-language.json
--- a/src/Tools/VSCode/extension/isabelle-ml-language.json	Tue Jan 03 16:48:49 2017 +0000
+++ b/src/Tools/VSCode/extension/isabelle-ml-language.json	Tue Jan 03 21:03:11 2017 +0100
@@ -1,18 +1,18 @@
 {
+  "comments": {
+    "blockComment": [ "(*", "*)" ]
+  },
+  "brackets": [
+    ["(", ")"],
+    ["[", "]"],
+    ["{", "}"]
+  ],
   "autoClosingPairs": [
     { "open": "{", "close": "}" },
     { "open": "[", "close": "]" },
     { "open": "(", "close": ")" },
     { "open": "\"", "close": "\"", "notIn": [ "string" ] }
   ],
-  "brackets": [
-    ["(", ")"],
-    ["[", "]"],
-    ["{", "}"]
-  ],
-  "comments": {
-    "blockComment": [ "(*", "*)" ]
-  },
   "surroundingPairs": [
     [ "{", "}" ],
     [ "[", "]" ],
diff -r 3b33d2fc5fc0 -r 34ef44748370 src/Tools/VSCode/src/protocol.scala
--- a/src/Tools/VSCode/src/protocol.scala	Tue Jan 03 16:48:49 2017 +0000
+++ b/src/Tools/VSCode/src/protocol.scala	Tue Jan 03 21:03:11 2017 +0100
@@ -138,7 +138,8 @@
       Map(
         "textDocumentSync" -> 1,
         "hoverProvider" -> true,
-        "definitionProvider" -> true)
+        "definitionProvider" -> true,
+        "documentHighlightProvider" -> true)
   }
 
   object Shutdown extends Request0("shutdown")
@@ -315,6 +316,31 @@
   }
 
 
+  /* document highlights request */
+
+  object DocumentHighlight
+  {
+    def text(range: Line.Range): DocumentHighlight = DocumentHighlight(range, Some(1))
+    def read(range: Line.Range): DocumentHighlight = DocumentHighlight(range, Some(2))
+    def write(range: Line.Range): DocumentHighlight = DocumentHighlight(range, Some(3))
+  }
+
+  sealed case class DocumentHighlight(range: Line.Range, kind: Option[Int] = None)
+  {
+    def json: JSON.T =
+      kind match {
+        case None => Map("range" -> Range(range))
+        case Some(k) => Map("range" -> Range(range), "kind" -> k)
+      }
+  }
+
+  object DocumentHighlights extends RequestTextDocumentPosition("textDocument/documentHighlight")
+  {
+    def reply(id: Id, result: List[DocumentHighlight]): JSON.T =
+      ResponseMessage(id, Some(result.map(_.json)))
+  }
+
+
   /* diagnostics */
 
   sealed case class Diagnostic(range: Line.Range, message: String,
@@ -329,10 +355,10 @@
 
   object DiagnosticSeverity
   {
-    val Error = 0
-    val Warning = 1
-    val Information = 2
-    val Hint = 3
+    val Error = 1
+    val Warning = 2
+    val Information = 3
+    val Hint = 4
   }
 
   object PublishDiagnostics
diff -r 3b33d2fc5fc0 -r 34ef44748370 src/Tools/VSCode/src/server.scala
--- a/src/Tools/VSCode/src/server.scala	Tue Jan 03 16:48:49 2017 +0000
+++ b/src/Tools/VSCode/src/server.scala	Tue Jan 03 21:03:11 2017 +0100
@@ -303,6 +303,21 @@
   }
 
 
+  /* document highlights */
+
+  def document_highlights(id: Protocol.Id, node_pos: Line.Node_Position)
+  {
+    val result =
+      (for ((rendering, offset) <- rendering_offset(node_pos))
+        yield {
+          val doc = rendering.model.doc
+          rendering.caret_focus_ranges(Text.Range(offset, offset + 1), doc.full_range)
+            .map(r => Protocol.DocumentHighlight.text(doc.range(r)))
+        }) getOrElse Nil
+    channel.write(Protocol.DocumentHighlights.reply(id, result))
+  }
+
+
   /* main loop */
 
   def start()
@@ -324,6 +339,7 @@
             close_document(uri)
           case Protocol.Hover(id, node_pos) => hover(id, node_pos)
           case Protocol.GotoDefinition(id, node_pos) => goto_definition(id, node_pos)
+          case Protocol.DocumentHighlights(id, node_pos) => document_highlights(id, node_pos)
           case _ => log("### IGNORED")
         }
       }
diff -r 3b33d2fc5fc0 -r 34ef44748370 src/Tools/VSCode/src/vscode_rendering.scala
--- a/src/Tools/VSCode/src/vscode_rendering.scala	Tue Jan 03 16:48:49 2017 +0000
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Tue Jan 03 21:03:11 2017 +0100
@@ -16,7 +16,7 @@
 
   private val message_severity =
     Map(
-      Markup.WRITELN -> Protocol.DiagnosticSeverity.Hint,
+      Markup.WRITELN -> Protocol.DiagnosticSeverity.Information,
       Markup.INFORMATION -> Protocol.DiagnosticSeverity.Information,
       Markup.WARNING -> Protocol.DiagnosticSeverity.Warning,
       Markup.LEGACY -> Protocol.DiagnosticSeverity.Warning,
@@ -126,7 +126,7 @@
       range, Nil, VSCode_Rendering.hyperlink_elements, _ =>
         {
           case (links, Text.Info(_, XML.Elem(Markup.Path(name), _))) =>
-            val file = resources.append_file_url(snapshot.node_name.master_dir, name)
+            val file = resources.append_file(snapshot.node_name.master_dir, name)
             Some(Line.Node_Range(file) :: links)
 
           case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
diff -r 3b33d2fc5fc0 -r 34ef44748370 src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Tue Jan 03 16:48:49 2017 +0000
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Tue Jan 03 21:03:11 2017 +0100
@@ -43,16 +43,17 @@
     val theory = Thy_Header.thy_name_bootstrap(uri).getOrElse("")
     val master_dir =
       if (!Url.is_wellformed_file(uri) || theory == "") ""
-      else Url.file(uri).getCanonicalFile.getParent
+      else Thy_Header.dir_name(uri)
     Document.Node.Name(uri, master_dir, theory)
   }
 
-  override def import_name(qualifier: String, master: Document.Node.Name, s: String)
-    : Document.Node.Name =
+  override def append(dir: String, source_path: Path): String =
   {
-    val name = super.import_name(qualifier, master, s)
-    if (name.node.startsWith("file://") || name.node.forall(c => c != '/' && c != '\\')) name
-    else name.copy(node = "file://" + name.node)
+    val path = source_path.expand
+    if (path.is_absolute) Url.platform_file(path)
+    else if (dir == "") Url.platform_file(File.pwd() + path)
+    else if (path.is_current) dir
+    else Url.normalize_file(dir + "/" + path.implode)
   }
 
   override def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
diff -r 3b33d2fc5fc0 -r 34ef44748370 src/Tools/jEdit/src/jedit_rendering.scala
--- a/src/Tools/jEdit/src/jedit_rendering.scala	Tue Jan 03 16:48:49 2017 +0000
+++ b/src/Tools/jEdit/src/jedit_rendering.scala	Tue Jan 03 21:03:11 2017 +0100
@@ -127,8 +127,6 @@
 
   private val breakpoint_elements = Markup.Elements(Markup.ML_BREAKPOINT)
 
-  private val caret_focus_elements = Markup.Elements(Markup.ENTITY)
-
   private val highlight_elements =
     Markup.Elements(Markup.EXPRESSION, Markup.CITATION, Markup.LANGUAGE, Markup.ML_TYPING,
       Markup.TOKEN_RANGE, Markup.ENTITY, Markup.PATH, Markup.DOC, Markup.URL, Markup.SORTING,
@@ -367,54 +365,8 @@
 
   /* caret focus */
 
-  def entity_focus(range: Text.Range,
-    check: (Boolean, Long) => Boolean = (is_def: Boolean, i: Long) => is_def): Set[Long] =
-  {
-    val results =
-      snapshot.cumulate[Set[Long]](range, Set.empty, JEdit_Rendering.caret_focus_elements, _ =>
-          {
-            case (serials, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
-              props match {
-                case Markup.Entity.Def(i) if check(true, i) => Some(serials + i)
-                case Markup.Entity.Ref(i) if check(false, i) => Some(serials + i)
-                case _ => None
-              }
-            case _ => None
-          })
-    (Set.empty[Long] /: results){ case (s1, Text.Info(_, s2)) => s1 ++ s2 }
-  }
-
-  def caret_focus(caret_range: Text.Range, visible_range: Text.Range): Set[Long] =
-  {
-    val focus_defs = entity_focus(caret_range)
-    if (focus_defs.nonEmpty) focus_defs
-    else {
-      val visible_defs = entity_focus(visible_range)
-      entity_focus(caret_range, (is_def: Boolean, i: Long) => !is_def && visible_defs.contains(i))
-    }
-  }
-
-  def caret_focus_ranges(caret_range: Text.Range, visible_range: Text.Range): List[Text.Range] =
-  {
-    val focus = caret_focus(caret_range, visible_range)
-    if (focus.nonEmpty) {
-      val results =
-        snapshot.cumulate[Boolean](visible_range, false, JEdit_Rendering.caret_focus_elements, _ =>
-          {
-            case (_, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
-              props match {
-                case Markup.Entity.Def(i) if focus(i) => Some(true)
-                case Markup.Entity.Ref(i) if focus(i) => Some(true)
-                case _ => None
-              }
-          })
-      for (info <- results if info.info) yield info.range
-    }
-    else Nil
-  }
-
   def entity_ref(range: Text.Range, focus: Set[Long]): List[Text.Info[Color]] =
-    snapshot.select(range, JEdit_Rendering.caret_focus_elements, _ =>
+    snapshot.select(range, Rendering.caret_focus_elements, _ =>
       {
         case Text.Info(_, XML.Elem(Markup(Markup.ENTITY, Markup.Entity.Ref(i)), _)) if focus(i) =>
           Some(entity_ref_color)