# HG changeset patch # User wenzelm # Date 1482356993 -3600 # Node ID ea5620f7b0d8ad3523079f1a0bc8e5aea97ddf8e # Parent 011629dda9373c774367c7bb47bdb94ec5c11555 clarified signature; diff -r 011629dda937 -r ea5620f7b0d8 src/Pure/PIDE/line.scala --- a/src/Pure/PIDE/line.scala Wed Dec 21 22:37:53 2016 +0100 +++ b/src/Pure/PIDE/line.scala Wed Dec 21 22:49:53 2016 +0100 @@ -62,13 +62,13 @@ /* positions within document node */ - sealed case class Position_Node(pos: Position, name: String) + sealed case class Node_Position(name: String, pos: Position = Position.zero) { def line: Int = pos.line def column: Int = pos.column } - sealed case class Range_Node(range: Range, name: String) + sealed case class Node_Range(name: String, range: Range = Range.zero) { def start: Position = range.start def stop: Position = range.stop diff -r 011629dda937 -r ea5620f7b0d8 src/Tools/VSCode/src/protocol.scala --- a/src/Tools/VSCode/src/protocol.scala Wed Dec 21 22:37:53 2016 +0100 +++ b/src/Tools/VSCode/src/protocol.scala Wed Dec 21 22:49:53 2016 +0100 @@ -82,10 +82,10 @@ class RequestTextDocumentPosition(name: String) { - def unapply(json: JSON.T): Option[(Id, Line.Position_Node)] = + def unapply(json: JSON.T): Option[(Id, Line.Node_Position)] = json match { - case RequestMessage(id, method, Some(TextDocumentPosition(pos_node))) if method == name => - Some((id, pos_node)) + case RequestMessage(id, method, Some(TextDocumentPosition(node_pos))) if method == name => + Some((id, node_pos)) case _ => None } } @@ -178,26 +178,26 @@ object Location { - def apply(loc: Line.Range_Node): JSON.T = + def apply(loc: Line.Node_Range): JSON.T = Map("uri" -> loc.name, "range" -> Range(loc.range)) - def unapply(json: JSON.T): Option[Line.Range_Node] = + def unapply(json: JSON.T): Option[Line.Node_Range] = for { uri <- JSON.string(json, "uri") range_json <- JSON.value(json, "range") range <- Range.unapply(range_json) - } yield Line.Range_Node(range, uri) + } yield Line.Node_Range(uri, range) } object TextDocumentPosition { - def unapply(json: JSON.T): Option[Line.Position_Node] = + def unapply(json: JSON.T): Option[Line.Node_Position] = for { doc <- JSON.value(json, "textDocument") uri <- JSON.string(doc, "uri") pos_json <- JSON.value(json, "position") pos <- Position.unapply(pos_json) - } yield Line.Position_Node(pos, uri) + } yield Line.Node_Position(uri, pos) } @@ -308,7 +308,7 @@ object GotoDefinition extends RequestTextDocumentPosition("textDocument/definition") { - def reply(id: Id, result: List[Line.Range_Node]): JSON.T = + def reply(id: Id, result: List[Line.Node_Range]): JSON.T = ResponseMessage(id, Some(result.map(Location.apply(_)))) } } diff -r 011629dda937 -r ea5620f7b0d8 src/Tools/VSCode/src/server.scala --- a/src/Tools/VSCode/src/server.scala Wed Dec 21 22:37:53 2016 +0100 +++ b/src/Tools/VSCode/src/server.scala Wed Dec 21 22:49:53 2016 +0100 @@ -106,11 +106,11 @@ def session: Session = state.value.session getOrElse error("Session inactive") def resources: VSCode_Resources = session.resources.asInstanceOf[VSCode_Resources] - def rendering_offset(pos_node: Line.Position_Node): Option[(VSCode_Rendering, Text.Offset)] = + def rendering_offset(node_pos: Line.Node_Position): Option[(VSCode_Rendering, Text.Offset)] = for { - model <- state.value.models.get(pos_node.name) + model <- state.value.models.get(node_pos.name) rendering = model.rendering(options) - offset <- model.doc.offset(pos_node.pos, text_length) + offset <- model.doc.offset(node_pos.pos, text_length) } yield (rendering, offset) @@ -223,11 +223,11 @@ /* hover */ - def hover(id: Protocol.Id, pos_node: Line.Position_Node) + def hover(id: Protocol.Id, node_pos: Line.Node_Position) { val result = for { - (rendering, offset) <- rendering_offset(pos_node) + (rendering, offset) <- rendering_offset(node_pos) info <- rendering.tooltip(Text.Range(offset, offset + 1)) } yield { val doc = rendering.model.doc @@ -242,10 +242,10 @@ /* goto definition */ - def goto_definition(id: Protocol.Id, pos_node: Line.Position_Node) + def goto_definition(id: Protocol.Id, node_pos: Line.Node_Position) { val result = - (for ((rendering, offset) <- rendering_offset(pos_node)) + (for ((rendering, offset) <- rendering_offset(node_pos)) yield rendering.hyperlinks(Text.Range(offset, offset + 1))) getOrElse Nil channel.write(Protocol.GotoDefinition.reply(id, result)) } @@ -270,8 +270,8 @@ update_document(uri, text) case Protocol.DidCloseTextDocument(uri) => channel.log("CLOSE " + uri) case Protocol.DidSaveTextDocument(uri) => channel.log("SAVE " + uri) - case Protocol.Hover(id, pos_node) => hover(id, pos_node) - case Protocol.GotoDefinition(id, pos_node) => goto_definition(id, pos_node) + case Protocol.Hover(id, node_pos) => hover(id, node_pos) + case Protocol.GotoDefinition(id, node_pos) => goto_definition(id, node_pos) case _ => channel.log("### IGNORED") } } diff -r 011629dda937 -r ea5620f7b0d8 src/Tools/VSCode/src/vscode_rendering.scala --- a/src/Tools/VSCode/src/vscode_rendering.scala Wed Dec 21 22:37:53 2016 +0100 +++ b/src/Tools/VSCode/src/vscode_rendering.scala Wed Dec 21 22:49:53 2016 +0100 @@ -31,13 +31,13 @@ /* hyperlinks */ - def hyperlinks(range: Text.Range): List[Line.Range_Node] = + def hyperlinks(range: Text.Range): List[Line.Node_Range] = { - snapshot.cumulate[List[Line.Range_Node]]( + snapshot.cumulate[List[Line.Node_Range]]( range, Nil, VSCode_Rendering.hyperlink_elements, _ => { case (links, Text.Info(_, XML.Elem(Markup.Path(name), _))) => - Some(Line.Range_Node(Line.Range.zero, resolve_file_url(name)) :: links) + Some(Line.Node_Range(resolve_file_url(name)) :: links) /* FIXME case (links, Text.Info(_, XML.Elem(Markup.Url(name), _))) =>