# HG changeset patch # User wenzelm # Date 1482351517 -3600 # Node ID 5d7f741aaccb88f6c35b77286eb6401923b875f5 # Parent bbfcef118acbf88e2b6e650cb9dd04c73cebaefc basic support for hyperlinks / Goto Definition Request; diff -r bbfcef118acb -r 5d7f741aaccb src/Pure/PIDE/rendering.scala --- a/src/Pure/PIDE/rendering.scala Wed Dec 21 21:17:44 2016 +0100 +++ b/src/Pure/PIDE/rendering.scala Wed Dec 21 21:18:37 2016 +0100 @@ -46,6 +46,11 @@ resources.append(snapshot.node_name.master_dir, Path.explode(name)) else name + def resolve_file_url(name: String): String = + if (Path.is_valid(name)) + "file://" + resources.append(snapshot.node_name.master_dir, Path.explode(name)) + else name + /* tooltips */ diff -r bbfcef118acb -r 5d7f741aaccb src/Tools/VSCode/src/protocol.scala --- a/src/Tools/VSCode/src/protocol.scala Wed Dec 21 21:17:44 2016 +0100 +++ b/src/Tools/VSCode/src/protocol.scala Wed Dec 21 21:18:37 2016 +0100 @@ -80,6 +80,16 @@ } } + class RequestTextDocumentPosition(name: String) + { + def unapply(json: JSON.T): Option[(Id, String, Line.Position)] = + json match { + case RequestMessage(id, method, Some(TextDocumentPosition(uri, pos))) if method == name => + Some((id, uri, 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") @@ -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[(String, Line.Range)]): JSON.T = + ResponseMessage(id, Some(result.map({ case (uri, range) => Location.apply(uri, range) }))) + } } diff -r bbfcef118acb -r 5d7f741aaccb src/Tools/VSCode/src/server.scala --- a/src/Tools/VSCode/src/server.scala Wed Dec 21 21:17:44 2016 +0100 +++ b/src/Tools/VSCode/src/server.scala Wed Dec 21 21:18:37 2016 +0100 @@ -234,6 +234,21 @@ } + /* goto definition */ + + def goto_definition(id: Protocol.Id, uri: String, pos: Line.Position) + { + val result = + (for { + model <- state.value.models.get(uri) + rendering = model.rendering(options) + offset <- model.doc.offset(pos, text_length) + } yield rendering.hyperlinks(Text.Range(offset, offset + 1))) getOrElse Nil + channel.log("hyperlinks = " + result) + channel.write(Protocol.GotoDefinition.reply(id, result)) + } + + /* main loop */ def start() @@ -254,6 +269,7 @@ case Protocol.DidCloseTextDocument(uri) => channel.log("CLOSE " + uri) case Protocol.DidSaveTextDocument(uri) => channel.log("SAVE " + uri) case Protocol.Hover(id, uri, pos) => hover(id, uri, pos) + case Protocol.GotoDefinition(id, uri, pos) => goto_definition(id, uri, pos) case _ => channel.log("### IGNORED") } } diff -r bbfcef118acb -r 5d7f741aaccb src/Tools/VSCode/src/vscode_rendering.scala --- a/src/Tools/VSCode/src/vscode_rendering.scala Wed Dec 21 21:17:44 2016 +0100 +++ b/src/Tools/VSCode/src/vscode_rendering.scala Wed Dec 21 21:18:37 2016 +0100 @@ -10,6 +10,11 @@ import isabelle._ +object VSCode_Rendering +{ + private val hyperlink_elements = + Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.URL) +} class VSCode_Rendering(snapshot: Document.Snapshot, options: Options, resources: Resources) extends Rendering(snapshot, options, resources) @@ -18,4 +23,36 @@ def tooltip_margin: Int = options.int("vscode_tooltip_margin") def timing_threshold: Double = options.real("vscode_timing_threshold") + + + /* hyperlinks */ + + def hyperlinks(range: Text.Range): List[(String, Line.Range)] = + { + snapshot.cumulate[List[(String, Line.Range)]]( + range, Nil, VSCode_Rendering.hyperlink_elements, _ => + { + case (links, Text.Info(_, XML.Elem(Markup.Path(name), _))) => + Some((resolve_file_url(name), Line.Range.zero) :: links) + +/* FIXME + case (links, Text.Info(_, XML.Elem(Markup.Url(name), _))) => + Some(PIDE.editor.hyperlink_url(name) :: links) + + 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 }) => + val opt_link = PIDE.editor.hyperlink_def_position(true, snapshot, props) + opt_link.map(_ :: links) + + case (links, Text.Info(info_range, XML.Elem(Markup(Markup.POSITION, props), _))) => + val opt_link = PIDE.editor.hyperlink_position(true, snapshot, props) + opt_link.map(_ :: links) +*/ + + case _ => None + }) match { case Text.Info(_, links) :: _ => links.reverse case _ => Nil } + } }