--- 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 */
--- 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
}
}
--- /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)
+ }
+}
--- 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;
--- 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 @@
}
}
}
-
--- 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]
}
--- 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)
}
}
--- 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)
}
--- 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)
--- 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) { }
}
-
--- 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 =
--- 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)
- }
-}
--- 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
--- 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)
}
--- 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)
}
--- 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(_))))
+ }
}
--- 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()
--- 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 }
+ }
}
--- 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)
}
}
--- 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 {
--- 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) =>
--- 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
}
}
--- 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))
--- 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)) }
}