# HG changeset patch
# User wenzelm
# Date 1482520238 -3600
# Node ID ce441970956fe94ce67064763541d83bed688412
# Parent  235df39ade8721715935adc8816fa5f141df6aef# Parent  39a6c88c059b6d431d7ec65fd29daba46523ac57
merged

diff -r 235df39ade87 -r ce441970956f src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Fri Dec 23 00:13:30 2016 +0100
+++ b/src/Pure/General/file.scala	Fri Dec 23 20:10:38 2016 +0100
@@ -99,12 +99,18 @@
   {
     val path = raw_path.expand
     require(path.is_absolute)
-    val s = platform_path(path).replaceAll(" ", "%20")
-    if (!Platform.is_windows) "file://" + s
-    else if (s.startsWith("\\\\")) "file:" + s.replace('\\', '/')
-    else "file:///" + s.replace('\\', '/')
+    platform_url(platform_path(path))
   }
 
+  def platform_url(name: String): String =
+    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('\\', '/')
+    }
+
 
   /* bash path */
 
diff -r 235df39ade87 -r ce441970956f src/Pure/General/position.scala
--- a/src/Pure/General/position.scala	Fri Dec 23 00:13:30 2016 +0100
+++ b/src/Pure/General/position.scala	Fri Dec 23 20:10:38 2016 +0100
@@ -64,20 +64,50 @@
       }
   }
 
-  object Id_Offset0
+  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 Def_Id_Offset0
+  object Item_Def_Id
+  {
+    def unapply(pos: T): Option[(Long, Symbol.Range)] =
+      pos match {
+        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[(Long, Symbol.Offset)] =
+    def unapply(pos: T): Option[(String, Int, Symbol.Range)] =
       pos match {
-        case Def_Id(id) => Some((id, Def_Offset.unapply(pos) getOrElse 0))
+        case Line_File(line, name) =>
+          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.Range)] =
+      pos match {
+        case Def_Line_File(line, name) =>
+          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
       }
   }
diff -r 235df39ade87 -r ce441970956f src/Pure/General/utf8.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/utf8.scala	Fri Dec 23 20:10:38 2016 +0100
@@ -0,0 +1,99 @@
+/*  Title:      Pure/General/utf8.scala
+    Author:     Makarius
+
+Variations on UTF-8.
+*/
+
+package isabelle
+
+
+import java.nio.charset.Charset
+import scala.io.Codec
+
+
+object UTF8
+{
+  /* charset */
+
+  val charset_name: String = "UTF-8"
+  val charset: Charset = Charset.forName(charset_name)
+  def codec(): Codec = Codec(charset)
+
+  def bytes(s: String): Array[Byte] = s.getBytes(charset)
+
+  object Length extends Codepoint.Length
+  {
+    override def codepoint_length(c: Int): Int =
+      if (c < 0x80) 1
+      else if (c < 0x800) 2
+      else if (c < 0x10000) 3
+      else 4
+  }
+
+
+  /* permissive UTF-8 decoding */
+
+  // see also http://en.wikipedia.org/wiki/UTF-8#Description
+  // overlong encodings enable byte-stuffing of low-ASCII
+
+  def decode_permissive(text: CharSequence): String =
+  {
+    val buf = new java.lang.StringBuilder(text.length)
+    var code = -1
+    var rest = 0
+    def flush()
+    {
+      if (code != -1) {
+        if (rest == 0 && Character.isValidCodePoint(code))
+          buf.appendCodePoint(code)
+        else buf.append('\uFFFD')
+        code = -1
+        rest = 0
+      }
+    }
+    def init(x: Int, n: Int)
+    {
+      flush()
+      code = x
+      rest = n
+    }
+    def push(x: Int)
+    {
+      if (rest <= 0) init(x, -1)
+      else {
+        code <<= 6
+        code += x
+        rest -= 1
+      }
+    }
+    for (i <- 0 until text.length) {
+      val c = text.charAt(i)
+      if (c < 128) { flush(); buf.append(c) }
+      else if ((c & 0xC0) == 0x80) push(c & 0x3F)
+      else if ((c & 0xE0) == 0xC0) init(c & 0x1F, 1)
+      else if ((c & 0xF0) == 0xE0) init(c & 0x0F, 2)
+      else if ((c & 0xF8) == 0xF0) init(c & 0x07, 3)
+    }
+    flush()
+    buf.toString
+  }
+
+  private class Decode_Chars(decode: String => String,
+    buffer: Array[Byte], start: Int, end: Int) extends CharSequence
+  {
+    def length: Int = end - start
+    def charAt(i: Int): Char = (buffer(start + i).asInstanceOf[Int] & 0xFF).asInstanceOf[Char]
+    def subSequence(i: Int, j: Int): CharSequence =
+      new Decode_Chars(decode, buffer, start + i, start + j)
+
+    // toString with adhoc decoding: abuse of CharSequence interface
+    override def toString: String = decode(decode_permissive(this))
+  }
+
+  def decode_chars(decode: String => String,
+    buffer: Array[Byte], start: Int, end: Int): CharSequence =
+  {
+    require(0 <= start && start <= end && end <= buffer.length)
+    new Decode_Chars(decode, buffer, start, end)
+  }
+}
diff -r 235df39ade87 -r ce441970956f src/Pure/ML/ml_compiler.ML
--- a/src/Pure/ML/ml_compiler.ML	Fri Dec 23 00:13:30 2016 +0100
+++ b/src/Pure/ML/ml_compiler.ML	Fri Dec 23 20:10:38 2016 +0100
@@ -86,7 +86,7 @@
       let
         val pos = Exn_Properties.position_of_polyml_location loc;
       in
-        is_reported pos ?
+        (is_reported pos andalso id <> 0) ?
           let
             fun markup () =
               (Markup.entityN, [(if def then Markup.defN else Markup.refN, Value.print_int id)]);
@@ -109,8 +109,6 @@
       | reported loc (PolyML.PTrefId id) = reported_entity_id false (FixedInt.toLarge id) loc
       | reported loc (PolyML.PTtype types) = reported_types loc types
       | reported loc (PolyML.PTdeclaredAt decl) = reported_entity Markup.ML_defN loc decl
-      | reported loc (PolyML.PTopenedAt decl) = reported_entity Markup.ML_openN loc decl
-      | reported loc (PolyML.PTstructureAt decl) = reported_entity Markup.ML_structureN loc decl
       | reported loc (PolyML.PTcompletions names) = reported_completions loc names
       | reported _ _ = I
     and reported_tree (loc, props) = fold (reported loc) props;
diff -r 235df39ade87 -r ce441970956f src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Fri Dec 23 00:13:30 2016 +0100
+++ b/src/Pure/PIDE/document.scala	Fri Dec 23 20:10:38 2016 +0100
@@ -454,6 +454,10 @@
     val load_commands: List[Command]
     def is_loaded: Boolean
 
+    def find_command(id: Document_ID.Generic): Option[(Node, Command)]
+    def find_command_position(id: Document_ID.Generic, offset: Symbol.Offset)
+      : Option[Line.Node_Position]
+
     def cumulate[A](
       range: Text.Range,
       info: A,
@@ -546,15 +550,6 @@
 
     def defined_command(id: Document_ID.Command): Boolean = commands.isDefinedAt(id)
 
-    def find_command(version: Version, id: Document_ID.Generic): Option[(Node, Command)] =
-      commands.get(id) orElse execs.get(id) match {
-        case None => None
-        case Some(st) =>
-          val command = st.command
-          val node = version.nodes(command.node_name)
-          if (node.commands.contains(command)) Some((node, command)) else None
-      }
-
     def the_version(id: Document_ID.Version): Version = versions.getOrElse(id, fail)
     def the_static_state(id: Document_ID.Command): Command.State = commands.getOrElse(id, fail)
     def the_dynamic_state(id: Document_ID.Exec): Command.State = execs.getOrElse(id, fail)
@@ -793,6 +788,31 @@
         val is_loaded: Boolean = node_name.is_theory || load_commands.nonEmpty
 
 
+        /* find command */
+
+        def find_command(id: Document_ID.Generic): Option[(Node, Command)] =
+          state.commands.get(id) orElse state.execs.get(id) match {
+            case None => None
+            case Some(st) =>
+              val command = st.command
+              val node = version.nodes(command.node_name)
+              if (node.commands.contains(command)) Some((node, command)) else None
+          }
+
+        def find_command_position(id: Document_ID.Generic, offset: Symbol.Offset)
+            : Option[Line.Node_Position] =
+          for ((node, command) <- find_command(id))
+          yield {
+            val name = command.node_name.node
+            val sources_iterator =
+              node.commands.iterator.takeWhile(_ != command).map(_.source) ++
+                (if (offset == 0) Iterator.empty
+                 else Iterator.single(command.source(Text.Range(0, command.chunk.decode(offset)))))
+            val pos = (Line.Position.zero /: sources_iterator)(_.advance(_))
+            Line.Node_Position(name, pos)
+          }
+
+
         /* cumulate markup */
 
         def cumulate[A](
@@ -853,4 +873,3 @@
     }
   }
 }
-
diff -r 235df39ade87 -r ce441970956f src/Pure/PIDE/editor.scala
--- a/src/Pure/PIDE/editor.scala	Fri Dec 23 00:13:30 2016 +0100
+++ b/src/Pure/PIDE/editor.scala	Fri Dec 23 20:10:38 2016 +0100
@@ -24,11 +24,11 @@
   def remove_overlay(command: Command, fn: String, args: List[String]): Unit
 
   abstract class Hyperlink {
-    def external: Boolean
+    def external: Boolean = false
     def follow(context: Context): Unit
   }
   def hyperlink_command(
-    focus: Boolean, snapshot: Document.Snapshot, command: Command, offset: Symbol.Offset = 0)
+    focus: Boolean, snapshot: Document.Snapshot, id: Document_ID.Generic, offset: Symbol.Offset = 0)
       : Option[Hyperlink]
 }
 
diff -r 235df39ade87 -r ce441970956f src/Pure/PIDE/line.scala
--- a/src/Pure/PIDE/line.scala	Fri Dec 23 00:13:30 2016 +0100
+++ b/src/Pure/PIDE/line.scala	Fri Dec 23 20:10:38 2016 +0100
@@ -16,10 +16,10 @@
 
   object Position
   {
-    val zero: Position = Position(0, 0)
+    val zero: Position = Position()
   }
 
-  sealed case class Position(line: Int, column: Int)
+  sealed case class Position(line: Int = 0, column: Int = 0)
   {
     def line1: Int = line + 1
     def column1: Int = column + 1
@@ -44,12 +44,35 @@
 
   /* range (right-open interval) */
 
+  object Range
+  {
+    def apply(start: Position): Range = Range(start, start)
+    val zero: Range = Range(Position.zero)
+  }
+
   sealed case class Range(start: Position, stop: Position)
   {
     if (start.compare(stop) > 0)
       error("Bad line range: " + start.print + ".." + stop.print)
 
-    def print: String = start.print + ".." + stop.print
+    def print: String =
+      if (start == stop) start.print
+      else start.print + ".." + stop.print
+  }
+
+
+  /* positions within document node */
+
+  sealed case class Node_Position(name: String, pos: Position = Position.zero)
+  {
+    def line: Int = pos.line
+    def column: Int = pos.column
+  }
+
+  sealed case class Node_Range(name: String, range: Range = Range.zero)
+  {
+    def start: Position = range.start
+    def stop: Position = range.stop
   }
 
 
@@ -86,11 +109,11 @@
       @tailrec def move(i: Text.Offset, lines_count: Int, lines_rest: List[Line]): Position =
       {
         lines_rest match {
-          case Nil => require(i == 0); Position(lines_count, 0)
+          case Nil => require(i == 0); Position(lines_count)
           case line :: ls =>
             val n = line.text.length
             if (ls.isEmpty || i <= n)
-              Position(lines_count, 0).advance(line.text.substring(n - i), length)
+              Position(lines_count).advance(line.text.substring(n - i), length)
             else move(i - (n + 1), lines_count + 1, ls)
         }
       }
diff -r 235df39ade87 -r ce441970956f src/Pure/PIDE/query_operation.scala
--- a/src/Pure/PIDE/query_operation.scala	Fri Dec 23 00:13:30 2016 +0100
+++ b/src/Pure/PIDE/query_operation.scala	Fri Dec 23 20:10:38 2016 +0100
@@ -208,7 +208,7 @@
     for {
       command <- state.location
       snapshot = editor.node_snapshot(command.node_name)
-      link <- editor.hyperlink_command(true, snapshot, command)
+      link <- editor.hyperlink_command(true, snapshot, command.id)
     } link.follow(editor_context)
   }
 
diff -r 235df39ade87 -r ce441970956f src/Pure/PIDE/rendering.scala
--- a/src/Pure/PIDE/rendering.scala	Fri Dec 23 00:13:30 2016 +0100
+++ b/src/Pure/PIDE/rendering.scala	Fri Dec 23 20:10:38 2016 +0100
@@ -39,14 +39,6 @@
   override def toString: String = "Rendering(" + snapshot.toString + ")"
 
 
-  /* resources */
-
-  def resolve_file(name: String): String =
-    if (Path.is_valid(name))
-      resources.append(snapshot.node_name.master_dir, Path.explode(name))
-    else name
-
-
   /* tooltips */
 
   def tooltip_margin: Int
@@ -72,10 +64,7 @@
             Some(Text.Info(r, (t1 + t2, info)))
 
           case (prev, Text.Info(r, XML.Elem(Markup.Entity(kind, name), _)))
-          if kind != "" &&
-            kind != Markup.ML_DEF &&
-            kind != Markup.ML_OPEN &&
-            kind != Markup.ML_STRUCTURE =>
+          if kind != "" && kind != Markup.ML_DEF =>
             val kind1 = Word.implode(Word.explode('_', kind))
             val txt1 =
               if (name == "") kind1
@@ -89,7 +78,7 @@
             Some(add(prev, r, (true, XML.Text(txt1 + txt2))))
 
           case (prev, Text.Info(r, XML.Elem(Markup.Path(name), _))) =>
-            val file = resolve_file(name)
+            val file = resources.append_file(snapshot.node_name.master_dir, name)
             val text =
               if (name == file) "file " + quote(file)
               else "path " + quote(name) + "\nfile " + quote(file)
diff -r 235df39ade87 -r ce441970956f src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Fri Dec 23 00:13:30 2016 +0100
+++ b/src/Pure/PIDE/resources.scala	Fri Dec 23 20:10:38 2016 +0100
@@ -43,13 +43,37 @@
   def append(dir: String, source_path: Path): String =
     (Path.explode(dir) + source_path).expand.implode
 
-  def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
+  def append_file(dir: String, raw_name: String): String =
+    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 */
+
+  def source_file(raw_name: String): Option[String] =
   {
-    val path = Path.explode(name.node)
-    if (!path.is_file) error("No such file: " + path.toString)
+    if (Path.is_wellformed(raw_name)) {
+      if (Path.is_valid(raw_name)) {
+        def check(p: Path): Option[Path] = if (p.is_file) Some(p) else None
 
-    val reader = Scan.byte_reader(path.file)
-    try { f(reader) } finally { reader.close }
+        val path = Path.explode(raw_name)
+        val path1 =
+          if (path.is_absolute || path.is_current) check(path)
+          else {
+            check(Path.explode("~~/src/Pure") + path) orElse
+              (if (Isabelle_System.getenv("ML_SOURCES") == "") None
+               else check(Path.explode("$ML_SOURCES") + path))
+          }
+        Some(File.platform_path(path1 getOrElse path))
+      }
+      else None
+    }
+    else Some(raw_name)
   }
 
 
@@ -87,6 +111,15 @@
     }
   }
 
+  def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
+  {
+    val path = Path.explode(name.node)
+    if (!path.is_file) error("No such file: " + path.toString)
+
+    val reader = Scan.byte_reader(path.file)
+    try { f(reader) } finally { reader.close }
+  }
+
   def check_thy_reader(qualifier: String, node_name: Document.Node.Name,
     reader: Reader[Char], start: Token.Pos): Document.Node.Header =
   {
@@ -133,4 +166,3 @@
 
   def commit(change: Session.Change) { }
 }
-
diff -r 235df39ade87 -r ce441970956f src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Fri Dec 23 00:13:30 2016 +0100
+++ b/src/Pure/System/isabelle_system.scala	Fri Dec 23 20:10:38 2016 +0100
@@ -161,21 +161,6 @@
 
   /** file-system operations **/
 
-  /* source files of Isabelle/ML bootstrap */
-
-  def source_file(path: Path): Option[Path] =
-  {
-    def check(p: Path): Option[Path] = if (p.is_file) Some(p) else None
-
-    if (path.is_absolute || path.is_current) check(path)
-    else {
-      check(Path.explode("~~/src/Pure") + path) orElse
-        (if (getenv("ML_SOURCES") == "") None
-         else check(Path.explode("$ML_SOURCES") + path))
-    }
-  }
-
-
   /* directories */
 
   def mkdirs(path: Path): Unit =
diff -r 235df39ade87 -r ce441970956f src/Pure/System/utf8.scala
--- a/src/Pure/System/utf8.scala	Fri Dec 23 00:13:30 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,99 +0,0 @@
-/*  Title:      Pure/System/utf8.scala
-    Author:     Makarius
-
-Variations on UTF-8.
-*/
-
-package isabelle
-
-
-import java.nio.charset.Charset
-import scala.io.Codec
-
-
-object UTF8
-{
-  /* charset */
-
-  val charset_name: String = "UTF-8"
-  val charset: Charset = Charset.forName(charset_name)
-  def codec(): Codec = Codec(charset)
-
-  def bytes(s: String): Array[Byte] = s.getBytes(charset)
-
-  object Length extends Codepoint.Length
-  {
-    override def codepoint_length(c: Int): Int =
-      if (c < 0x80) 1
-      else if (c < 0x800) 2
-      else if (c < 0x10000) 3
-      else 4
-  }
-
-
-  /* permissive UTF-8 decoding */
-
-  // see also http://en.wikipedia.org/wiki/UTF-8#Description
-  // overlong encodings enable byte-stuffing of low-ASCII
-
-  def decode_permissive(text: CharSequence): String =
-  {
-    val buf = new java.lang.StringBuilder(text.length)
-    var code = -1
-    var rest = 0
-    def flush()
-    {
-      if (code != -1) {
-        if (rest == 0 && Character.isValidCodePoint(code))
-          buf.appendCodePoint(code)
-        else buf.append('\uFFFD')
-        code = -1
-        rest = 0
-      }
-    }
-    def init(x: Int, n: Int)
-    {
-      flush()
-      code = x
-      rest = n
-    }
-    def push(x: Int)
-    {
-      if (rest <= 0) init(x, -1)
-      else {
-        code <<= 6
-        code += x
-        rest -= 1
-      }
-    }
-    for (i <- 0 until text.length) {
-      val c = text.charAt(i)
-      if (c < 128) { flush(); buf.append(c) }
-      else if ((c & 0xC0) == 0x80) push(c & 0x3F)
-      else if ((c & 0xE0) == 0xC0) init(c & 0x1F, 1)
-      else if ((c & 0xF0) == 0xE0) init(c & 0x0F, 2)
-      else if ((c & 0xF8) == 0xF0) init(c & 0x07, 3)
-    }
-    flush()
-    buf.toString
-  }
-
-  private class Decode_Chars(decode: String => String,
-    buffer: Array[Byte], start: Int, end: Int) extends CharSequence
-  {
-    def length: Int = end - start
-    def charAt(i: Int): Char = (buffer(start + i).asInstanceOf[Int] & 0xFF).asInstanceOf[Char]
-    def subSequence(i: Int, j: Int): CharSequence =
-      new Decode_Chars(decode, buffer, start + i, start + j)
-
-    // toString with adhoc decoding: abuse of CharSequence interface
-    override def toString: String = decode(decode_permissive(this))
-  }
-
-  def decode_chars(decode: String => String,
-    buffer: Array[Byte], start: Int, end: Int): CharSequence =
-  {
-    require(0 <= start && start <= end && end <= buffer.length)
-    new Decode_Chars(decode, buffer, start, end)
-  }
-}
diff -r 235df39ade87 -r ce441970956f src/Pure/build-jars
--- a/src/Pure/build-jars	Fri Dec 23 00:13:30 2016 +0100
+++ b/src/Pure/build-jars	Fri Dec 23 20:10:38 2016 +0100
@@ -70,6 +70,7 @@
   General/timing.scala
   General/untyped.scala
   General/url.scala
+  General/utf8.scala
   General/value.scala
   General/word.scala
   General/xz.scala
@@ -118,7 +119,6 @@
   System/process_result.scala
   System/progress.scala
   System/system_channel.scala
-  System/utf8.scala
   Thy/html.scala
   Thy/present.scala
   Thy/sessions.scala
diff -r 235df39ade87 -r ce441970956f src/Tools/VSCode/src/channel.scala
--- a/src/Tools/VSCode/src/channel.scala	Fri Dec 23 00:13:30 2016 +0100
+++ b/src/Tools/VSCode/src/channel.scala	Fri Dec 23 20:10:38 2016 +0100
@@ -86,4 +86,17 @@
       out.flush
     }
   }
+
+
+  /* display message */
+
+  def display_message(message_type: Int, message: String, show: Boolean = true): Unit =
+    write(Protocol.DisplayMessage(message_type, Output.clean_yxml(message), show))
+
+  def error_message(message: String, show: Boolean = true): Unit =
+    display_message(Protocol.MessageType.Error, message, show)
+  def warning(message: String, show: Boolean = true): Unit =
+    display_message(Protocol.MessageType.Warning, message, show)
+  def writeln(message: String, show: Boolean = true): Unit =
+    display_message(Protocol.MessageType.Info, message, show)
 }
diff -r 235df39ade87 -r ce441970956f src/Tools/VSCode/src/document_model.scala
--- a/src/Tools/VSCode/src/document_model.scala	Fri Dec 23 00:13:30 2016 +0100
+++ b/src/Tools/VSCode/src/document_model.scala	Fri Dec 23 20:10:38 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(snapshot(), options, session.resources)
+  def rendering(options: Options, text_length: Length): VSCode_Rendering =
+    new VSCode_Rendering(this, snapshot(), options, text_length, session.resources)
 }
diff -r 235df39ade87 -r ce441970956f src/Tools/VSCode/src/protocol.scala
--- a/src/Tools/VSCode/src/protocol.scala	Fri Dec 23 00:13:30 2016 +0100
+++ b/src/Tools/VSCode/src/protocol.scala	Fri Dec 23 20:10:38 2016 +0100
@@ -80,6 +80,16 @@
       }
   }
 
+  class RequestTextDocumentPosition(name: String)
+  {
+    def unapply(json: JSON.T): Option[(Id, Line.Node_Position)] =
+      json match {
+        case RequestMessage(id, method, Some(TextDocumentPosition(node_pos))) if method == name =>
+          Some((id, node_pos))
+        case _ => None
+      }
+  }
+
 
   /* response message */
 
@@ -125,7 +135,10 @@
   object ServerCapabilities
   {
     val json: JSON.T =
-      Map("textDocumentSync" -> 1, "hoverProvider" -> true)
+      Map(
+        "textDocumentSync" -> 1,
+        "hoverProvider" -> true,
+        "definitionProvider" -> true)
   }
 
   object Shutdown extends Request0("shutdown")
@@ -165,26 +178,26 @@
 
   object Location
   {
-    def apply(uri: String, range: Line.Range): JSON.T =
-      Map("uri" -> uri, "range" -> Range(range))
+    def apply(loc: Line.Node_Range): 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.Node_Range] =
       for {
         uri <- JSON.string(json, "uri")
         range_json <- JSON.value(json, "range")
         range <- Range.unapply(range_json)
-      } yield (uri, range)
+      } yield Line.Node_Range(uri, range)
   }
 
   object TextDocumentPosition
   {
-    def unapply(json: JSON.T): Option[(String, Line.Position)] =
+    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 (uri, pos)
+      } yield Line.Node_Position(uri, pos)
   }
 
 
@@ -277,15 +290,8 @@
 
   /* hover request */
 
-  object Hover
+  object Hover extends RequestTextDocumentPosition("textDocument/hover")
   {
-    def unapply(json: JSON.T): Option[(Id, String, Line.Position)] =
-      json match {
-        case RequestMessage(id, "textDocument/hover", Some(TextDocumentPosition(uri, pos))) =>
-          Some((id, uri, pos))
-        case _ => None
-      }
-
     def reply(id: Id, result: Option[(Line.Range, List[String])]): JSON.T =
     {
       val res =
@@ -296,4 +302,13 @@
       ResponseMessage(id, Some(res))
     }
   }
+
+
+  /* goto definition request */
+
+  object GotoDefinition extends RequestTextDocumentPosition("textDocument/definition")
+  {
+    def reply(id: Id, result: List[Line.Node_Range]): JSON.T =
+      ResponseMessage(id, Some(result.map(Location.apply(_))))
+  }
 }
diff -r 235df39ade87 -r ce441970956f src/Tools/VSCode/src/server.scala
--- a/src/Tools/VSCode/src/server.scala	Fri Dec 23 00:13:30 2016 +0100
+++ b/src/Tools/VSCode/src/server.scala	Fri Dec 23 20:10:38 2016 +0100
@@ -25,18 +25,19 @@
 
   val isabelle_tool = Isabelle_Tool("vscode_server", "VSCode Language Server for PIDE", args =>
   {
-    var log_file: Option[Path] = None
-    var text_length = Length.encoding(default_text_length)
-    var dirs: List[Path] = Nil
-    var logic = default_logic
-    var modes: List[String] = Nil
-    var options = Options.init()
+    try {
+      var log_file: Option[Path] = None
+      var text_length = Length.encoding(default_text_length)
+      var dirs: List[Path] = Nil
+      var logic = default_logic
+      var modes: List[String] = Nil
+      var options = Options.init()
 
-    def text_length_choice: String =
-      commas(Length.encodings.map(
-        { case (a, _) => if (a == default_text_length) a + " (default)" else a }))
+      def text_length_choice: String =
+        commas(Length.encodings.map(
+          { case (a, _) => if (a == default_text_length) a + " (default)" else a }))
 
-    val getopts = Getopts("""
+      val getopts = Getopts("""
 Usage: isabelle vscode_server [OPTIONS]
 
   Options are:
@@ -49,30 +50,37 @@
 
   Run the VSCode Language Server protocol (JSON RPC) over stdin/stdout.
 """,
-      "L:" -> (arg => log_file = Some(Path.explode(arg))),
-      "T:" -> (arg => Length.encoding(arg)),
-      "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
-      "l:" -> (arg => logic = arg),
-      "m:" -> (arg => modes = arg :: modes),
-      "o:" -> (arg => options = options + arg))
+        "L:" -> (arg => log_file = Some(Path.explode(arg))),
+        "T:" -> (arg => Length.encoding(arg)),
+        "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
+        "l:" -> (arg => logic = arg),
+        "m:" -> (arg => modes = arg :: modes),
+        "o:" -> (arg => options = options + arg))
 
-    val more_args = getopts(args)
-    if (more_args.nonEmpty) getopts.usage()
+      val more_args = getopts(args)
+      if (more_args.nonEmpty) getopts.usage()
+
+      if (!Build.build(options = options, build_heap = true, no_build = true,
+            dirs = dirs, sessions = List(logic)).ok)
+        error("Missing logic image " + quote(logic))
 
-    if (!Build.build(options = options, build_heap = true, no_build = true,
-          dirs = dirs, sessions = List(logic)).ok)
-      error("Missing logic image " + quote(logic))
-
-    val channel = new Channel(System.in, System.out, log_file)
-    val server = new Server(channel, options, text_length, logic, dirs, modes)
+      val channel = new Channel(System.in, System.out, log_file)
+      val server = new Server(channel, options, text_length, logic, dirs, modes)
 
-    // prevent spurious garbage on the main protocol channel
-    val orig_out = System.out
-    try {
-      System.setOut(new PrintStream(new OutputStream { def write(n: Int) {} }))
-      server.start()
+      // prevent spurious garbage on the main protocol channel
+      val orig_out = System.out
+      try {
+        System.setOut(new PrintStream(new OutputStream { def write(n: Int) {} }))
+        server.start()
+      }
+      finally { System.setOut(orig_out) }
     }
-    finally { System.setOut(orig_out) }
+    catch {
+      case exn: Throwable =>
+        val channel = new Channel(System.in, System.out, None)
+        channel.error_message(Exn.message(exn))
+        throw(exn)
+    }
   })
 
 
@@ -98,46 +106,68 @@
   def session: Session = state.value.session getOrElse error("Session inactive")
   def resources: VSCode_Resources = session.resources.asInstanceOf[VSCode_Resources]
 
+  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, text_length)
+      offset <- model.doc.offset(node_pos.pos, text_length)
+    } yield (rendering, offset)
+
 
   /* init and exit */
 
-  def initialize(reply: String => Unit)
+  def init(id: Protocol.Id)
   {
-    val content = Build.session_content(options, false, session_dirs, session_name)
-    val resources =
-      new VSCode_Resources(content.loaded_theories, content.known_theories, content.syntax)
+    def reply(err: String)
+    {
+      channel.write(Protocol.Initialize.reply(id, err))
+      if (err == "")
+        channel.writeln("Welcome to Isabelle/" + session_name + " (" + Distribution.version + ")")
+      else channel.error_message(err)
+    }
 
-    val session =
-      new Session(resources) {
-        override def output_delay = options.seconds("editor_output_delay")
-        override def prune_delay = options.seconds("editor_prune_delay")
-        override def syslog_limit = options.int("editor_syslog_limit")
-        override def reparse_limit = options.int("editor_reparse_limit")
-      }
+    val try_session =
+      try {
+        val content = Build.session_content(options, false, session_dirs, session_name)
+        val resources =
+          new VSCode_Resources(content.loaded_theories, content.known_theories, content.syntax)
 
-    var session_phase: Session.Consumer[Session.Phase] = null
-    session_phase =
-      Session.Consumer(getClass.getName) {
-        case Session.Ready =>
-          session.phase_changed -= session_phase
-          session.update_options(options)
-          reply("")
-        case Session.Failed =>
-          session.phase_changed -= session_phase
-          reply("Prover startup failed")
-        case _ =>
+        Some(new Session(resources) {
+          override def output_delay = options.seconds("editor_output_delay")
+          override def prune_delay = options.seconds("editor_prune_delay")
+          override def syslog_limit = options.int("editor_syslog_limit")
+          override def reparse_limit = options.int("editor_reparse_limit")
+        })
       }
-    session.phase_changed += session_phase
+      catch { case ERROR(msg) => reply(msg); None }
 
-    session.start(receiver =>
-      Isabelle_Process(options = options, logic = session_name, dirs = session_dirs,
-        modes = modes, receiver = receiver))
+    for (session <- try_session) {
+      var session_phase: Session.Consumer[Session.Phase] = null
+      session_phase =
+        Session.Consumer(getClass.getName) {
+          case Session.Ready =>
+            session.phase_changed -= session_phase
+            session.update_options(options)
+            reply("")
+          case Session.Failed =>
+            session.phase_changed -= session_phase
+            reply("Prover startup failed")
+          case _ =>
+        }
+      session.phase_changed += session_phase
 
-    state.change(_.copy(session = Some(session)))
+      session.start(receiver =>
+        Isabelle_Process(options = options, logic = session_name, dirs = session_dirs,
+          modes = modes, receiver = receiver))
+
+      state.change(_.copy(session = Some(session)))
+    }
   }
 
-  def shutdown(reply: String => Unit)
+  def shutdown(id: Protocol.Id)
   {
+    def reply(err: String): Unit = channel.write(Protocol.Shutdown.reply(id, err))
+
     state.change(st =>
       st.session match {
         case None => reply("Prover inactive"); st
@@ -156,7 +186,10 @@
       })
   }
 
-  def exit() { sys.exit(if (state.value.session.isDefined) 1 else 0) }
+  def exit() {
+    channel.log("\n")
+    sys.exit(if (state.value.session.isDefined) 1 else 0)
+  }
 
 
   /* document management */
@@ -190,57 +223,59 @@
 
   /* hover */
 
-  def hover(uri: String, pos: Line.Position): Option[(Line.Range, List[String])] =
-    for {
-      model <- state.value.models.get(uri)
-      rendering = model.rendering(options)
-      offset <- model.doc.offset(pos, text_length)
-      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 s = Pretty.string_of(info.info, margin = rendering.tooltip_margin)
-      (Line.Range(start, stop), List("```\n" + s + "\n```"))
-    }
+  def hover(id: Protocol.Id, node_pos: Line.Node_Position)
+  {
+    val result =
+      for {
+        (rendering, offset) <- rendering_offset(node_pos)
+        info <- rendering.tooltip(Text.Range(offset, offset + 1))
+      } yield {
+        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
+      }
+    channel.write(Protocol.Hover.reply(id, result))
+  }
+
+
+  /* goto definition */
+
+  def goto_definition(id: Protocol.Id, node_pos: Line.Node_Position)
+  {
+    val result =
+      (for ((rendering, offset) <- rendering_offset(node_pos))
+        yield rendering.hyperlinks(Text.Range(offset, offset + 1))) getOrElse Nil
+    channel.write(Protocol.GotoDefinition.reply(id, result))
+  }
 
 
   /* main loop */
 
   def start()
   {
-    channel.log("\nServer started " + Date.now())
+    channel.log("Server started " + Date.now())
 
     def handle(json: JSON.T)
     {
       try {
         json match {
-          case Protocol.Initialize(id) =>
-            def initialize_reply(err: String)
-            {
-              channel.write(Protocol.Initialize.reply(id, err))
-              if (err == "") {
-                channel.write(Protocol.DisplayMessage(Protocol.MessageType.Info,
-                  "Welcome to Isabelle/" + session_name + " (" + Distribution.version + ")"))
-              }
-              else channel.write(Protocol.DisplayMessage(Protocol.MessageType.Error, err))
-            }
-            initialize(initialize_reply _)
-          case Protocol.Shutdown(id) =>
-            shutdown((error: String) => channel.write(Protocol.Shutdown.reply(id, error)))
-          case Protocol.Exit =>
-            exit()
+          case Protocol.Initialize(id) => init(id)
+          case Protocol.Shutdown(id) => shutdown(id)
+          case Protocol.Exit(()) => exit()
           case Protocol.DidOpenTextDocument(uri, lang, version, text) =>
             update_document(uri, text)
           case Protocol.DidChangeTextDocument(uri, version, List(Protocol.TextDocumentContent(text))) =>
             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) =>
-            channel.write(Protocol.Hover.reply(id, hover(uri, pos)))
+          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")
         }
       }
-      catch { case exn: Throwable => channel.log("*** ERROR: " + Exn.message(exn)) }
+      catch { case exn: Throwable => channel.error_message(Exn.message(exn)) }
     }
 
     @tailrec def loop()
diff -r 235df39ade87 -r ce441970956f src/Tools/VSCode/src/vscode_rendering.scala
--- a/src/Tools/VSCode/src/vscode_rendering.scala	Fri Dec 23 00:13:30 2016 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Fri Dec 23 20:10:38 2016 +0100
@@ -10,12 +10,89 @@
 
 import isabelle._
 
+object VSCode_Rendering
+{
+  private val hyperlink_elements =
+    Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION)
+}
 
-class VSCode_Rendering(snapshot: Document.Snapshot, options: Options, resources: Resources)
+class VSCode_Rendering(
+    val model: Document_Model,
+    snapshot: Document.Snapshot,
+    options: Options,
+    text_length: Length,
+    resources: Resources)
   extends Rendering(snapshot, options, resources)
 {
   /* tooltips */
 
   def tooltip_margin: Int = options.int("vscode_tooltip_margin")
   def timing_threshold: Double = options.real("vscode_timing_threshold")
+
+
+  /* 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(File.platform_url(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]](
+      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)
+            Some(Line.Node_Range(file) :: links)
+
+          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 }
+  }
 }
diff -r 235df39ade87 -r ce441970956f src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Fri Dec 23 00:13:30 2016 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Fri Dec 23 20:10:38 2016 +0100
@@ -34,10 +34,10 @@
 {
   def node_name(uri: String): Document.Node.Name =
   {
-    val file = VSCode_Resources.canonical_file(uri)  // FIXME wellformed!?
-    val node = file.getPath
-    val theory = Thy_Header.thy_name_bootstrap(node).getOrElse("")
-    val master_dir = if (theory == "") "" else file.getParent
-    Document.Node.Name(node, master_dir, theory)
+    val theory = Thy_Header.thy_name(uri).getOrElse("")
+    val master_dir =
+      if (!VSCode_Resources.is_wellformed(uri) || theory == "") ""
+      else VSCode_Resources.canonical_file(uri).getParent
+    Document.Node.Name(uri, master_dir, theory)
   }
 }
diff -r 235df39ade87 -r ce441970956f src/Tools/jEdit/src/active.scala
--- a/src/Tools/jEdit/src/active.scala	Fri Dec 23 00:13:30 2016 +0100
+++ b/src/Tools/jEdit/src/active.scala	Fri Dec 23 20:10:38 2016 +0100
@@ -51,7 +51,7 @@
               case XML.Elem(Markup(Markup.SIMP_TRACE_PANEL, props), _) =>
                 val link =
                   props match {
-                    case Position.Id(id) => PIDE.editor.hyperlink_command_id(true, snapshot, id)
+                    case Position.Id(id) => PIDE.editor.hyperlink_command(true, snapshot, id)
                     case _ => None
                   }
                 GUI_Thread.later {
diff -r 235df39ade87 -r ce441970956f src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Fri Dec 23 00:13:30 2016 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala	Fri Dec 23 20:10:38 2016 +0100
@@ -329,7 +329,7 @@
   {
     val buffer = text_area.getBuffer
     if (!snapshot.is_outdated && text != "") {
-      (snapshot.state.find_command(snapshot.version, id), PIDE.document_model(buffer)) match {
+      (snapshot.find_command(id), PIDE.document_model(buffer)) match {
         case (Some((node, command)), Some(model)) if command.node_name == model.node_name =>
           node.command_start(command) match {
             case Some(start) =>
diff -r 235df39ade87 -r ce441970956f src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Fri Dec 23 00:13:30 2016 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Fri Dec 23 20:10:38 2016 +0100
@@ -158,21 +158,28 @@
     }
   }
 
-  def goto_file(focus: Boolean, view: View, name: String, line: Int = 0, column: Int = 0)
+  def goto_file(focus: Boolean, view: View, name: String): Unit =
+    goto_file(focus, view, Line.Node_Position(name))
+
+  def goto_file(focus: Boolean, view: View, pos: Line.Node_Position)
   {
     GUI_Thread.require {}
 
     push_position(view)
 
+    val name = pos.name
+    val line = pos.line
+    val column = pos.column
+
     JEdit_Lib.jedit_buffer(name) match {
       case Some(buffer) =>
         if (focus) view.goToBuffer(buffer) else view.showBuffer(buffer)
         val text_area = view.getTextArea
 
         try {
-          val line_start = text_area.getBuffer.getLineStartOffset(line - 1)
+          val line_start = text_area.getBuffer.getLineStartOffset(line)
           text_area.moveCaretPosition(line_start)
-          if (column > 0) text_area.moveCaretPosition(line_start + column - 1)
+          if (column > 0) text_area.moveCaretPosition(line_start + column)
         }
         catch {
           case _: ArrayIndexOutOfBoundsException =>
@@ -185,8 +192,8 @@
       case None =>
         val args =
           if (line <= 0) Array(name)
-          else if (column <= 0) Array(name, "+line:" + line.toInt)
-          else Array(name, "+line:" + line.toInt + "," + column.toInt)
+          else if (column <= 0) Array(name, "+line:" + (line + 1))
+          else Array(name, "+line:" + (line + 1) + "," + (column + 1))
         jEdit.openFiles(view, null, args)
     }
   }
@@ -217,14 +224,14 @@
       case doc: Doc.Text_File if doc.name == name => doc.path
       case doc: Doc.Doc if doc.name == name => doc.path}).map(path =>
         new Hyperlink {
-          val external = !path.is_file
+          override val external = !path.is_file
           def follow(view: View): Unit = goto_doc(view, path)
           override def toString: String = "doc " + quote(name)
         })
 
   def hyperlink_url(name: String): Hyperlink =
     new Hyperlink {
-      val external = true
+      override val external = true
       def follow(view: View): Unit =
         Standard_Thread.fork("hyperlink_url") {
           try { Isabelle_System.open(Url.escape(name)) }
@@ -240,87 +247,55 @@
 
   def hyperlink_buffer(focus: Boolean, buffer: Buffer, offset: Text.Offset): Hyperlink =
     new Hyperlink {
-      val external = false
       def follow(view: View): Unit = goto_buffer(focus, view, buffer, offset)
       override def toString: String = "buffer " + quote(JEdit_Lib.buffer_name(buffer))
     }
 
-  def hyperlink_file(focus: Boolean, name: String, line: Int = 0, column: Int = 0): Hyperlink =
+  def hyperlink_file(focus: Boolean, name: String): Hyperlink =
+    hyperlink_file(focus, Line.Node_Position(name))
+
+  def hyperlink_file(focus: Boolean, pos: Line.Node_Position): Hyperlink =
     new Hyperlink {
-      val external = false
-      def follow(view: View): Unit = goto_file(focus, view, name, line, column)
-      override def toString: String = "file " + quote(name)
+      def follow(view: View): Unit = goto_file(focus, view, pos)
+      override def toString: String = "file " + quote(pos.name)
     }
 
-  def hyperlink_source_file(focus: Boolean, source_name: String, line: Int, offset: Symbol.Offset)
+  def hyperlink_source_file(focus: Boolean, source_name: String, line1: Int, offset: Symbol.Offset)
     : Option[Hyperlink] =
   {
-    val opt_name =
-      if (Path.is_wellformed(source_name)) {
-        if (Path.is_valid(source_name)) {
-          val path = Path.explode(source_name)
-          Some(File.platform_path(Isabelle_System.source_file(path) getOrElse path))
-        }
-        else None
+    for (name <- PIDE.resources.source_file(source_name)) yield {
+      JEdit_Lib.jedit_buffer(name) match {
+        case Some(buffer) if offset > 0 =>
+          val pos =
+            JEdit_Lib.buffer_lock(buffer) {
+              (Line.Position.zero /:
+                (Symbol.iterator(JEdit_Lib.buffer_text(buffer)).
+                  zipWithIndex.takeWhile(p => p._2 < offset - 1).map(_._1)))(_.advance(_))
+            }
+          hyperlink_file(focus, Line.Node_Position(name, pos))
+        case _ =>
+          hyperlink_file(focus, Line.Node_Position(name, Line.Position((line1 - 1) max 0)))
       }
-      else Some(source_name)
-
-    opt_name match {
-      case Some(name) =>
-        JEdit_Lib.jedit_buffer(name) match {
-          case Some(buffer) if offset > 0 =>
-            val pos =
-              JEdit_Lib.buffer_lock(buffer) {
-                (Line.Position.zero /:
-                  (Symbol.iterator(JEdit_Lib.buffer_text(buffer)).
-                    zipWithIndex.takeWhile(p => p._2 < offset - 1).map(_._1)))(_.advance(_))
-              }
-            Some(hyperlink_file(focus, name, pos.line1, pos.column1))
-          case _ => Some(hyperlink_file(focus, name, line))
-        }
-      case None => None
     }
   }
 
   override def hyperlink_command(
-    focus: Boolean, snapshot: Document.Snapshot, command: Command, offset: Symbol.Offset = 0)
+    focus: Boolean, snapshot: Document.Snapshot, id: Document_ID.Generic, offset: Symbol.Offset = 0)
       : Option[Hyperlink] =
   {
     if (snapshot.is_outdated) None
-    else {
-      snapshot.state.find_command(snapshot.version, command.id) match {
-        case None => None
-        case Some((node, _)) =>
-          val file_name = command.node_name.node
-          val sources_iterator =
-            node.commands.iterator.takeWhile(_ != command).map(_.source) ++
-              (if (offset == 0) Iterator.empty
-               else Iterator.single(command.source(Text.Range(0, command.chunk.decode(offset)))))
-          val pos = (Line.Position.zero /: sources_iterator)(_.advance(_))
-          Some(hyperlink_file(focus, file_name, pos.line1, pos.column1))
-      }
-    }
-  }
-
-  def hyperlink_command_id(
-    focus: Boolean, snapshot: Document.Snapshot, id: Document_ID.Generic, offset: Symbol.Offset = 0)
-      : Option[Hyperlink] =
-  {
-    snapshot.state.find_command(snapshot.version, id) match {
-      case Some((node, command)) => hyperlink_command(focus, snapshot, command, offset)
-      case None => None
-    }
+    else snapshot.find_command_position(id, offset).map(hyperlink_file(focus, _))
   }
 
   def is_hyperlink_position(snapshot: Document.Snapshot,
     text_offset: Text.Offset, pos: Position.T): Boolean =
   {
     pos match {
-      case Position.Id_Offset0(id, offset) if offset > 0 =>
-        snapshot.state.find_command(snapshot.version, id) match {
+      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
@@ -332,22 +307,20 @@
   def hyperlink_position(focus: Boolean, snapshot: Document.Snapshot, pos: Position.T)
       : Option[Hyperlink] =
     pos match {
-      case Position.Line_File(line, name) =>
-        val offset = Position.Offset.unapply(pos) getOrElse 0
-        hyperlink_source_file(focus, name, line, offset)
-      case Position.Id_Offset0(id, offset) =>
-        hyperlink_command_id(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.Def_Line_File(line, name) =>
-        val offset = Position.Def_Offset.unapply(pos) getOrElse 0
-        hyperlink_source_file(focus, name, line, offset)
-      case Position.Def_Id_Offset0(id, offset) =>
-        hyperlink_command_id(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
     }
 }
diff -r 235df39ade87 -r ce441970956f src/Tools/jEdit/src/jedit_rendering.scala
--- a/src/Tools/jEdit/src/jedit_rendering.scala	Fri Dec 23 00:13:30 2016 +0100
+++ b/src/Tools/jEdit/src/jedit_rendering.scala	Fri Dec 23 20:10:38 2016 +0100
@@ -466,7 +466,8 @@
       range, Vector.empty, JEdit_Rendering.hyperlink_elements, _ =>
         {
           case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _))) =>
-            val link = PIDE.editor.hyperlink_file(true, resolve_file(name))
+            val file = resources.append_file(snapshot.node_name.master_dir, name)
+            val link = PIDE.editor.hyperlink_file(true, file)
             Some(links :+ Text.Info(snapshot.convert(info_range), link))
 
           case (links, Text.Info(info_range, XML.Elem(Markup.Doc(name), _))) =>
@@ -477,11 +478,7 @@
             val link = PIDE.editor.hyperlink_url(name)
             Some(links :+ Text.Info(snapshot.convert(info_range), link))
 
-          case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _)))
-          if !props.exists(
-            { case (Markup.KIND, Markup.ML_OPEN) => true
-              case (Markup.KIND, Markup.ML_STRUCTURE) => true
-              case _ => false }) =>
+          case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
             val opt_link = PIDE.editor.hyperlink_def_position(true, snapshot, props)
             opt_link.map(link => links :+ Text.Info(snapshot.convert(info_range), link))
 
diff -r 235df39ade87 -r ce441970956f src/Tools/jEdit/src/timing_dockable.scala
--- a/src/Tools/jEdit/src/timing_dockable.scala	Fri Dec 23 00:13:30 2016 +0100
+++ b/src/Tools/jEdit/src/timing_dockable.scala	Fri Dec 23 20:10:38 2016 +0100
@@ -96,7 +96,7 @@
     def print: String =
       "  " + Time.print_seconds(timing) + "s command " + quote(command.span.name)
     def follow(snapshot: Document.Snapshot)
-    { PIDE.editor.hyperlink_command(true, snapshot, command).foreach(_.follow(view)) }
+    { PIDE.editor.hyperlink_command(true, snapshot, command.id).foreach(_.follow(view)) }
   }