clarified signature;

--- a/src/Pure/PIDE/line.scala	Wed Dec 21 22:37:53 2016 +0100
+++ b/src/Pure/PIDE/line.scala	Wed Dec 21 22:49:53 2016 +0100
@@ -62,13 +62,13 @@
 
   /* positions within document node */
 
-  sealed case class Position_Node(pos: Position, name: String)
+  sealed case class Node_Position(name: String, pos: Position = Position.zero)
   {
     def line: Int = pos.line
     def column: Int = pos.column
   }
 
-  sealed case class Range_Node(range: Range, name: String)
+  sealed case class Node_Range(name: String, range: Range = Range.zero)
   {
     def start: Position = range.start
     def stop: Position = range.stop

--- a/src/Tools/VSCode/src/protocol.scala	Wed Dec 21 22:37:53 2016 +0100
+++ b/src/Tools/VSCode/src/protocol.scala	Wed Dec 21 22:49:53 2016 +0100
@@ -82,10 +82,10 @@
 
   class RequestTextDocumentPosition(name: String)
   {
-    def unapply(json: JSON.T): Option[(Id, Line.Position_Node)] =
+    def unapply(json: JSON.T): Option[(Id, Line.Node_Position)] =
       json match {
-        case RequestMessage(id, method, Some(TextDocumentPosition(pos_node))) if method == name =>
-          Some((id, pos_node))
+        case RequestMessage(id, method, Some(TextDocumentPosition(node_pos))) if method == name =>
+          Some((id, node_pos))
         case _ => None
       }
   }
@@ -178,26 +178,26 @@
 
   object Location
   {
-    def apply(loc: Line.Range_Node): JSON.T =
+    def apply(loc: Line.Node_Range): JSON.T =
       Map("uri" -> loc.name, "range" -> Range(loc.range))
 
-    def unapply(json: JSON.T): Option[Line.Range_Node] =
+    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.Range_Node(range, uri)
+      } yield Line.Node_Range(uri, range)
   }
 
   object TextDocumentPosition
   {
-    def unapply(json: JSON.T): Option[Line.Position_Node] =
+    def unapply(json: JSON.T): Option[Line.Node_Position] =
       for {
         doc <- JSON.value(json, "textDocument")
         uri <- JSON.string(doc, "uri")
         pos_json <- JSON.value(json, "position")
         pos <- Position.unapply(pos_json)
-      } yield Line.Position_Node(pos, uri)
+      } yield Line.Node_Position(uri, pos)
   }
 
 
@@ -308,7 +308,7 @@
 
   object GotoDefinition extends RequestTextDocumentPosition("textDocument/definition")
   {
-    def reply(id: Id, result: List[Line.Range_Node]): JSON.T =
+    def reply(id: Id, result: List[Line.Node_Range]): JSON.T =
       ResponseMessage(id, Some(result.map(Location.apply(_))))
   }
 }

--- a/src/Tools/VSCode/src/server.scala	Wed Dec 21 22:37:53 2016 +0100
+++ b/src/Tools/VSCode/src/server.scala	Wed Dec 21 22:49:53 2016 +0100
@@ -106,11 +106,11 @@
   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)] =
+  def rendering_offset(node_pos: Line.Node_Position): Option[(VSCode_Rendering, Text.Offset)] =
     for {
-      model <- state.value.models.get(pos_node.name)
+      model <- state.value.models.get(node_pos.name)
       rendering = model.rendering(options)
-      offset <- model.doc.offset(pos_node.pos, text_length)
+      offset <- model.doc.offset(node_pos.pos, text_length)
     } yield (rendering, offset)
 
 
@@ -223,11 +223,11 @@
 
   /* hover */
 
-  def hover(id: Protocol.Id, pos_node: Line.Position_Node)
+  def hover(id: Protocol.Id, node_pos: Line.Node_Position)
   {
     val result =
       for {
-        (rendering, offset) <- rendering_offset(pos_node)
+        (rendering, offset) <- rendering_offset(node_pos)
         info <- rendering.tooltip(Text.Range(offset, offset + 1))
       } yield {
         val doc = rendering.model.doc
@@ -242,10 +242,10 @@
 
   /* goto definition */
 
-  def goto_definition(id: Protocol.Id, pos_node: Line.Position_Node)
+  def goto_definition(id: Protocol.Id, node_pos: Line.Node_Position)
   {
     val result =
-      (for ((rendering, offset) <- rendering_offset(pos_node))
+      (for ((rendering, offset) <- rendering_offset(node_pos))
         yield rendering.hyperlinks(Text.Range(offset, offset + 1))) getOrElse Nil
     channel.write(Protocol.GotoDefinition.reply(id, result))
   }
@@ -270,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, pos_node) => hover(id, pos_node)
-          case Protocol.GotoDefinition(id, pos_node) => goto_definition(id, pos_node)
+          case Protocol.Hover(id, node_pos) => hover(id, node_pos)
+          case Protocol.GotoDefinition(id, node_pos) => goto_definition(id, node_pos)
           case _ => channel.log("### IGNORED")
         }
       }

--- a/src/Tools/VSCode/src/vscode_rendering.scala	Wed Dec 21 22:37:53 2016 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Wed Dec 21 22:49:53 2016 +0100
@@ -31,13 +31,13 @@
 
   /* hyperlinks */
 
-  def hyperlinks(range: Text.Range): List[Line.Range_Node] =
+  def hyperlinks(range: Text.Range): List[Line.Node_Range] =
   {
-    snapshot.cumulate[List[Line.Range_Node]](
+    snapshot.cumulate[List[Line.Node_Range]](
       range, Nil, VSCode_Rendering.hyperlink_elements, _ =>
         {
           case (links, Text.Info(_, XML.Elem(Markup.Path(name), _))) =>
-            Some(Line.Range_Node(Line.Range.zero, resolve_file_url(name)) :: links)
+            Some(Line.Node_Range(resolve_file_url(name)) :: links)
 
 /* FIXME
           case (links, Text.Info(_, XML.Elem(Markup.Url(name), _))) =>