full range for Position.Item;
more hyperlinks for VSCode;

--- a/src/Pure/General/position.scala	Fri Dec 23 19:07:54 2016 +0100
+++ b/src/Pure/General/position.scala	Fri Dec 23 19:19:59 2016 +0100
@@ -66,40 +66,48 @@
 
   object Item_Id
   {
-    def unapply(pos: T): Option[(Long, Symbol.Offset)] =
+    def unapply(pos: T): Option[(Long, Symbol.Range)] =
       pos match {
-        case Id(id) => Some((id, Offset.unapply(pos) getOrElse 0))
+        case Id(id) =>
+          val offset = Offset.unapply(pos) getOrElse 0
+          val end_offset = End_Offset.unapply(pos) getOrElse (offset + 1)
+          Some((id, Text.Range(offset, end_offset)))
         case _ => None
       }
   }
 
   object Item_Def_Id
   {
-    def unapply(pos: T): Option[(Long, Symbol.Offset)] =
+    def unapply(pos: T): Option[(Long, Symbol.Range)] =
       pos match {
-        case Def_Id(id) => Some((id, Def_Offset.unapply(pos) getOrElse 0))
+        case Def_Id(id) =>
+          val offset = Def_Offset.unapply(pos) getOrElse 0
+          val end_offset = Def_End_Offset.unapply(pos) getOrElse (offset + 1)
+          Some((id, Text.Range(offset, end_offset)))
         case _ => None
       }
   }
 
   object Item_File
   {
-    def unapply(pos: T): Option[(String, Int, Symbol.Offset)] =
+    def unapply(pos: T): Option[(String, Int, Symbol.Range)] =
       pos match {
         case Line_File(line, name) =>
-          val offset = Position.Offset.unapply(pos) getOrElse 0
-          Some((name, line, offset))
+          val offset = Offset.unapply(pos) getOrElse 0
+          val end_offset = End_Offset.unapply(pos) getOrElse (offset + 1)
+          Some((name, line, Text.Range(offset, end_offset)))
         case _ => None
       }
   }
 
   object Item_Def_File
   {
-    def unapply(pos: T): Option[(String, Int, Symbol.Offset)] =
+    def unapply(pos: T): Option[(String, Int, Symbol.Range)] =
       pos match {
         case Def_Line_File(line, name) =>
-          val offset = Position.Def_Offset.unapply(pos) getOrElse 0
-          Some((name, line, offset))
+          val offset = Def_Offset.unapply(pos) getOrElse 0
+          val end_offset = Def_End_Offset.unapply(pos) getOrElse (offset + 1)
+          Some((name, line, Text.Range(offset, end_offset)))
         case _ => None
       }
   }

--- a/src/Tools/VSCode/src/document_model.scala	Fri Dec 23 19:07:54 2016 +0100
+++ b/src/Tools/VSCode/src/document_model.scala	Fri Dec 23 19:19:59 2016 +0100
@@ -56,6 +56,6 @@
 
   def snapshot(): Document.Snapshot = session.snapshot(node_name, text_edits)
 
-  def rendering(options: Options): VSCode_Rendering =
-    new VSCode_Rendering(this, snapshot(), options, session.resources)
+  def rendering(options: Options, text_length: Length): VSCode_Rendering =
+    new VSCode_Rendering(this, snapshot(), options, text_length, session.resources)
 }

--- a/src/Tools/VSCode/src/server.scala	Fri Dec 23 19:07:54 2016 +0100
+++ b/src/Tools/VSCode/src/server.scala	Fri Dec 23 19:19:59 2016 +0100
@@ -109,7 +109,7 @@
   def rendering_offset(node_pos: Line.Node_Position): Option[(VSCode_Rendering, Text.Offset)] =
     for {
       model <- state.value.models.get(node_pos.name)
-      rendering = model.rendering(options)
+      rendering = model.rendering(options, text_length)
       offset <- model.doc.offset(node_pos.pos, text_length)
     } yield (rendering, offset)
 

--- a/src/Tools/VSCode/src/vscode_rendering.scala	Fri Dec 23 19:07:54 2016 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Fri Dec 23 19:19:59 2016 +0100
@@ -20,6 +20,7 @@
     val model: Document_Model,
     snapshot: Document.Snapshot,
     options: Options,
+    text_length: Length,
     resources: Resources)
   extends Rendering(snapshot, options, resources)
 {
@@ -31,6 +32,51 @@
 
   /* hyperlinks */
 
+  def hyperlink_source_file(source_name: String, line1: Int, range: Symbol.Range)
+    : Option[Line.Node_Range] =
+  {
+    for (name <- resources.source_file(source_name))
+    yield {
+      val opt_text =
+        try { Some(File.read(Path.explode(name))) } // FIXME content from resources/models
+        catch { case ERROR(_) => None }
+      Line.Node_Range(name,
+        opt_text match {
+          case Some(text) if range.start > 0 =>
+            val chunk = Symbol.Text_Chunk(text)
+            val doc = Line.Document(text)
+            def position(offset: Symbol.Offset) = doc.position(chunk.decode(offset), text_length)
+            Line.Range(position(range.start), position(range.stop))
+          case _ =>
+            Line.Range(Line.Position((line1 - 1) max 0))
+        })
+    }
+  }
+
+  def hyperlink_command(id: Document_ID.Generic, range: Symbol.Range): Option[Line.Node_Range] =
+  {
+    if (snapshot.is_outdated) None
+    else
+      for {
+        start <- snapshot.find_command_position(id, range.start)
+        stop <- snapshot.find_command_position(id, range.stop)
+      } yield Line.Node_Range(start.name, Line.Range(start.pos, stop.pos))
+  }
+
+  def hyperlink_position(pos: Position.T): Option[Line.Node_Range] =
+    pos match {
+      case Position.Item_File(name, line, range) => hyperlink_source_file(name, line, range)
+      case Position.Item_Id(id, range) => hyperlink_command(id, range)
+      case _ => None
+    }
+
+  def hyperlink_def_position(pos: Position.T): Option[Line.Node_Range] =
+    pos match {
+      case Position.Item_Def_File(name, line, range) => hyperlink_source_file(name, line, range)
+      case Position.Item_Def_Id(id, range) => hyperlink_command(id, range)
+      case _ => None
+    }
+
   def hyperlinks(range: Text.Range): List[Line.Node_Range] =
   {
     snapshot.cumulate[List[Line.Node_Range]](
@@ -40,7 +86,11 @@
             val file = resources.append_file_url(snapshot.node_name.master_dir, name)
             Some(Line.Node_Range(file) :: links)
 
-          // FIXME more cases
+          case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
+            hyperlink_def_position(props).map(_ :: links)
+
+          case (links, Text.Info(info_range, XML.Elem(Markup(Markup.POSITION, props), _))) =>
+            hyperlink_position(props).map(_ :: links)
 
           case _ => None
         }) match { case Text.Info(_, links) :: _ => links.reverse case _ => Nil }

--- a/src/Tools/jEdit/src/jedit_editor.scala	Fri Dec 23 19:07:54 2016 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Fri Dec 23 19:19:59 2016 +0100
@@ -291,11 +291,11 @@
     text_offset: Text.Offset, pos: Position.T): Boolean =
   {
     pos match {
-      case Position.Item_Id(id, offset) if offset > 0 =>
+      case Position.Item_Id(id, range) if range.start > 0 =>
         snapshot.find_command(id) match {
           case Some((node, command)) if snapshot.version.nodes(command.node_name) eq node =>
             node.command_start(command) match {
-              case Some(start) => text_offset == start + command.chunk.decode(offset)
+              case Some(start) => text_offset == start + command.chunk.decode(range.start)
               case None => false
             }
           case _ => false
@@ -307,20 +307,20 @@
   def hyperlink_position(focus: Boolean, snapshot: Document.Snapshot, pos: Position.T)
       : Option[Hyperlink] =
     pos match {
-      case Position.Item_File(name, line, offset) =>
-        hyperlink_source_file(focus, name, line, offset)
-      case Position.Item_Id(id, offset) =>
-        hyperlink_command(focus, snapshot, id, offset)
+      case Position.Item_File(name, line, range) =>
+        hyperlink_source_file(focus, name, line, range.start)
+      case Position.Item_Id(id, range) =>
+        hyperlink_command(focus, snapshot, id, range.start)
       case _ => None
     }
 
   def hyperlink_def_position(focus: Boolean, snapshot: Document.Snapshot, pos: Position.T)
       : Option[Hyperlink] =
     pos match {
-      case Position.Item_Def_File(name, line, offset) =>
-        hyperlink_source_file(focus, name, line, offset)
-      case Position.Item_Def_Id(id, offset) =>
-        hyperlink_command(focus, snapshot, id, offset)
+      case Position.Item_Def_File(name, line, range) =>
+        hyperlink_source_file(focus, name, line, range.start)
+      case Position.Item_Def_Id(id, range) =>
+        hyperlink_command(focus, snapshot, id, range.start)
       case _ => None
     }
 }