# HG changeset patch
# User wenzelm
# Date 1482355658 -3600
# Node ID d67c3094a0c2c47cebb1ed45bc09159b2bc5237c
# Parent  5d7f741aaccb88f6c35b77286eb6401923b875f5
tuned signature -- more explicit types;

diff -r 5d7f741aaccb -r d67c3094a0c2 src/Pure/PIDE/line.scala
--- a/src/Pure/PIDE/line.scala	Wed Dec 21 21:18:37 2016 +0100
+++ b/src/Pure/PIDE/line.scala	Wed Dec 21 22:27:38 2016 +0100
@@ -60,6 +60,12 @@
   }
 
 
+  /* positions within document node */
+
+  sealed case class Position_Node(pos: Position, name: String)
+  sealed case class Range_Node(range: Range, name: String)
+
+
   /* document with newline as separator (not terminator) */
 
   object Document
diff -r 5d7f741aaccb -r d67c3094a0c2 src/Tools/VSCode/src/document_model.scala
--- a/src/Tools/VSCode/src/document_model.scala	Wed Dec 21 21:18:37 2016 +0100
+++ b/src/Tools/VSCode/src/document_model.scala	Wed Dec 21 22:27:38 2016 +0100
@@ -57,5 +57,5 @@
   def snapshot(): Document.Snapshot = session.snapshot(node_name, text_edits)
 
   def rendering(options: Options): VSCode_Rendering =
-    new VSCode_Rendering(snapshot(), options, session.resources)
+    new VSCode_Rendering(this, snapshot(), options, session.resources)
 }
diff -r 5d7f741aaccb -r d67c3094a0c2 src/Tools/VSCode/src/protocol.scala
--- a/src/Tools/VSCode/src/protocol.scala	Wed Dec 21 21:18:37 2016 +0100
+++ b/src/Tools/VSCode/src/protocol.scala	Wed Dec 21 22:27:38 2016 +0100
@@ -82,10 +82,10 @@
 
   class RequestTextDocumentPosition(name: String)
   {
-    def unapply(json: JSON.T): Option[(Id, String, Line.Position)] =
+    def unapply(json: JSON.T): Option[(Id, Line.Position_Node)] =
       json match {
-        case RequestMessage(id, method, Some(TextDocumentPosition(uri, pos))) if method == name =>
-          Some((id, uri, pos))
+        case RequestMessage(id, method, Some(TextDocumentPosition(pos_node))) if method == name =>
+          Some((id, pos_node))
         case _ => None
       }
   }
@@ -178,26 +178,26 @@
 
   object Location
   {
-    def apply(uri: String, range: Line.Range): JSON.T =
-      Map("uri" -> uri, "range" -> Range(range))
+    def apply(loc: Line.Range_Node): JSON.T =
+      Map("uri" -> loc.name, "range" -> Range(loc.range))
 
-    def unapply(json: JSON.T): Option[(String, Line.Range)] =
+    def unapply(json: JSON.T): Option[Line.Range_Node] =
       for {
         uri <- JSON.string(json, "uri")
         range_json <- JSON.value(json, "range")
         range <- Range.unapply(range_json)
-      } yield (uri, range)
+      } yield Line.Range_Node(range, uri)
   }
 
   object TextDocumentPosition
   {
-    def unapply(json: JSON.T): Option[(String, Line.Position)] =
+    def unapply(json: JSON.T): Option[Line.Position_Node] =
       for {
         doc <- JSON.value(json, "textDocument")
         uri <- JSON.string(doc, "uri")
         pos_json <- JSON.value(json, "position")
         pos <- Position.unapply(pos_json)
-      } yield (uri, pos)
+      } yield Line.Position_Node(pos, uri)
   }
 
 
@@ -308,7 +308,7 @@
 
   object GotoDefinition extends RequestTextDocumentPosition("textDocument/definition")
   {
-    def reply(id: Id, result: List[(String, Line.Range)]): JSON.T =
-      ResponseMessage(id, Some(result.map({ case (uri, range) => Location.apply(uri, range) })))
+    def reply(id: Id, result: List[Line.Range_Node]): JSON.T =
+      ResponseMessage(id, Some(result.map(Location.apply(_))))
   }
 }
diff -r 5d7f741aaccb -r d67c3094a0c2 src/Tools/VSCode/src/server.scala
--- a/src/Tools/VSCode/src/server.scala	Wed Dec 21 21:18:37 2016 +0100
+++ b/src/Tools/VSCode/src/server.scala	Wed Dec 21 22:27:38 2016 +0100
@@ -106,6 +106,13 @@
   def session: Session = state.value.session getOrElse error("Session inactive")
   def resources: VSCode_Resources = session.resources.asInstanceOf[VSCode_Resources]
 
+  def rendering_offset(pos_node: Line.Position_Node): Option[(VSCode_Rendering, Text.Offset)] =
+    for {
+      model <- state.value.models.get(pos_node.name)
+      rendering = model.rendering(options)
+      offset <- model.doc.offset(pos_node.pos, text_length)
+    } yield (rendering, offset)
+
 
   /* init and exit */
 
@@ -216,17 +223,16 @@
 
   /* hover */
 
-  def hover(id: Protocol.Id, uri: String, pos: Line.Position)
+  def hover(id: Protocol.Id, pos_node: Line.Position_Node)
   {
     val result =
       for {
-        model <- state.value.models.get(uri)
-        rendering = model.rendering(options)
-        offset <- model.doc.offset(pos, text_length)
+        (rendering, offset) <- rendering_offset(pos_node)
         info <- rendering.tooltip(Text.Range(offset, offset + 1))
       } yield {
-        val start = model.doc.position(info.range.start, text_length)
-        val stop = model.doc.position(info.range.stop, text_length)
+        val doc = rendering.model.doc
+        val start = doc.position(info.range.start, text_length)
+        val stop = doc.position(info.range.stop, text_length)
         val s = Pretty.string_of(info.info, margin = rendering.tooltip_margin)
         (Line.Range(start, stop), List("```\n" + s + "\n```"))  // FIXME proper content format
       }
@@ -236,15 +242,11 @@
 
   /* goto definition */
 
-  def goto_definition(id: Protocol.Id, uri: String, pos: Line.Position)
+  def goto_definition(id: Protocol.Id, pos_node: Line.Position_Node)
   {
     val result =
-      (for {
-        model <- state.value.models.get(uri)
-        rendering = model.rendering(options)
-        offset <- model.doc.offset(pos, text_length)
-      } yield rendering.hyperlinks(Text.Range(offset, offset + 1))) getOrElse Nil
-    channel.log("hyperlinks = " + result)
+      (for ((rendering, offset) <- rendering_offset(pos_node))
+        yield rendering.hyperlinks(Text.Range(offset, offset + 1))) getOrElse Nil
     channel.write(Protocol.GotoDefinition.reply(id, result))
   }
 
@@ -268,8 +270,8 @@
             update_document(uri, text)
           case Protocol.DidCloseTextDocument(uri) => channel.log("CLOSE " + uri)
           case Protocol.DidSaveTextDocument(uri) => channel.log("SAVE " + uri)
-          case Protocol.Hover(id, uri, pos) => hover(id, uri, pos)
-          case Protocol.GotoDefinition(id, uri, pos) => goto_definition(id, uri, pos)
+          case Protocol.Hover(id, pos_node) => hover(id, pos_node)
+          case Protocol.GotoDefinition(id, pos_node) => goto_definition(id, pos_node)
           case _ => channel.log("### IGNORED")
         }
       }
diff -r 5d7f741aaccb -r d67c3094a0c2 src/Tools/VSCode/src/vscode_rendering.scala
--- a/src/Tools/VSCode/src/vscode_rendering.scala	Wed Dec 21 21:18:37 2016 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Wed Dec 21 22:27:38 2016 +0100
@@ -16,7 +16,11 @@
     Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.URL)
 }
 
-class VSCode_Rendering(snapshot: Document.Snapshot, options: Options, resources: Resources)
+class VSCode_Rendering(
+    val model: Document_Model,
+    snapshot: Document.Snapshot,
+    options: Options,
+    resources: Resources)
   extends Rendering(snapshot, options, resources)
 {
   /* tooltips */
@@ -27,13 +31,13 @@
 
   /* hyperlinks */
 
-  def hyperlinks(range: Text.Range): List[(String, Line.Range)] =
+  def hyperlinks(range: Text.Range): List[Line.Range_Node] =
   {
-    snapshot.cumulate[List[(String, Line.Range)]](
+    snapshot.cumulate[List[Line.Range_Node]](
       range, Nil, VSCode_Rendering.hyperlink_elements, _ =>
         {
           case (links, Text.Info(_, XML.Elem(Markup.Path(name), _))) =>
-            Some((resolve_file_url(name), Line.Range.zero) :: links)
+            Some(Line.Range_Node(Line.Range.zero, resolve_file_url(name)) :: links)
 
 /* FIXME
           case (links, Text.Info(_, XML.Elem(Markup.Url(name), _))) =>