# HG changeset patch # User wenzelm # Date 1484161315 -3600 # Node ID 31e9920a0dc1770179a86c85f83f893d98b7ef91 # Parent 65a2474441004d3db26b0c4343f023d131a00c94 support for semantic completion; diff -r 65a247444100 -r 31e9920a0dc1 src/Pure/PIDE/line.scala --- a/src/Pure/PIDE/line.scala Wed Jan 11 16:43:31 2017 +0100 +++ b/src/Pure/PIDE/line.scala Wed Jan 11 20:01:55 2017 +0100 @@ -104,6 +104,10 @@ } lazy val text: String = lines.mkString("", "\n", "") + def try_get_text(range: Text.Range): Option[String] = + if (text_range.contains(range)) Some(text.substring(range.start, range.stop)) + else None + override def toString: String = text override def equals(that: Any): Boolean = diff -r 65a247444100 -r 31e9920a0dc1 src/Pure/PIDE/rendering.scala --- a/src/Pure/PIDE/rendering.scala Wed Jan 11 16:43:31 2017 +0100 +++ b/src/Pure/PIDE/rendering.scala Wed Jan 11 20:01:55 2017 +0100 @@ -39,6 +39,9 @@ /* markup elements */ + private val semantic_completion_elements = + Markup.Elements(Markup.COMPLETION, Markup.NO_COMPLETION) + private val tooltip_descriptions = Map( Markup.CITATION -> "citation", @@ -70,6 +73,24 @@ override def toString: String = "Rendering(" + snapshot.toString + ")" + /* completion */ + + def semantic_completion(completed_range: Option[Text.Range], range: Text.Range) + : Option[Text.Info[Completion.Semantic]] = + if (snapshot.is_outdated) None + else { + snapshot.select(range, Rendering.semantic_completion_elements, _ => + { + case Completion.Semantic.Info(info) => + completed_range match { + case Some(range0) if range0.contains(info.range) && range0 != info.range => None + case _ => Some(info) + } + case _ => None + }).headOption.map(_.info) + } + + /* tooltips */ def tooltip_margin: Int diff -r 65a247444100 -r 31e9920a0dc1 src/Tools/VSCode/src/document_model.scala --- a/src/Tools/VSCode/src/document_model.scala Wed Jan 11 16:43:31 2017 +0100 +++ b/src/Tools/VSCode/src/document_model.scala Wed Jan 11 20:01:55 2017 +0100 @@ -18,6 +18,7 @@ { def text_range: Text.Range = doc.text_range def text: String = doc.text + def try_get_text(range: Text.Range): Option[String] = doc.try_get_text(range) lazy val bytes: Bytes = Bytes(text) lazy val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(text) diff -r 65a247444100 -r 31e9920a0dc1 src/Tools/VSCode/src/protocol.scala --- a/src/Tools/VSCode/src/protocol.scala Wed Jan 11 16:43:31 2017 +0100 +++ b/src/Tools/VSCode/src/protocol.scala Wed Jan 11 20:01:55 2017 +0100 @@ -140,6 +140,7 @@ val json: JSON.T = Map( "textDocumentSync" -> 1, + "completionProvider" -> Map("resolveProvider" -> false, "triggerCharacters" -> Nil), "hoverProvider" -> true, "definitionProvider" -> true, "documentHighlightProvider" -> true) @@ -292,6 +293,32 @@ object DidSaveTextDocument extends TextDocumentNotification("textDocument/didSave") + /* completion */ + + sealed case class CompletionItem( + label: String, + kind: Option[Int] = None, + detail: Option[String] = None, + documentation: Option[String] = None, + insertText: Option[String] = None, + range: Option[Line.Range] = None) + { + def json: JSON.T = + Message.empty + ("label" -> label) ++ + (kind match { case Some(x) => Map("kind" -> x) case None => Map.empty }) ++ + (detail match { case Some(x) => Map("detail" -> x) case None => Map.empty }) ++ + (documentation match { case Some(x) => Map("documentation" -> x) case None => Map.empty }) ++ + (insertText match { case Some(x) => Map("insertText" -> x) case None => Map.empty }) ++ + (range match { case Some(x) => Map("range" -> Range(x)) case None => Map.empty }) + } + + object Completion extends RequestTextDocumentPosition("textDocument/completion") + { + def reply(id: Id, result: List[CompletionItem]): JSON.T = + ResponseMessage(id, Some(result.map(_.json))) + } + + /* hover request */ object Hover extends RequestTextDocumentPosition("textDocument/hover") diff -r 65a247444100 -r 31e9920a0dc1 src/Tools/VSCode/src/server.scala --- a/src/Tools/VSCode/src/server.scala Wed Jan 11 16:43:31 2017 +0100 +++ b/src/Tools/VSCode/src/server.scala Wed Jan 11 20:01:55 2017 +0100 @@ -277,6 +277,17 @@ } + /* completion */ + + def completion(id: Protocol.Id, node_pos: Line.Node_Position) + { + val result = + (for ((rendering, offset) <- rendering_offset(node_pos)) + yield rendering.completion(Text.Range(offset - 1, offset))) getOrElse Nil + channel.write(Protocol.Completion.reply(id, result)) + } + + /* hover */ def hover(id: Protocol.Id, node_pos: Line.Node_Position) @@ -341,6 +352,7 @@ update_document(file, text) case Protocol.DidCloseTextDocument(file) => close_document(file) + case Protocol.Completion(id, node_pos) => completion(id, node_pos) case Protocol.Hover(id, node_pos) => hover(id, node_pos) case Protocol.GotoDefinition(id, node_pos) => goto_definition(id, node_pos) case Protocol.DocumentHighlights(id, node_pos) => document_highlights(id, node_pos) diff -r 65a247444100 -r 31e9920a0dc1 src/Tools/VSCode/src/vscode_rendering.scala --- a/src/Tools/VSCode/src/vscode_rendering.scala Wed Jan 11 16:43:31 2017 +0100 +++ b/src/Tools/VSCode/src/vscode_rendering.scala Wed Jan 11 20:01:55 2017 +0100 @@ -43,6 +43,29 @@ resources: VSCode_Resources) extends Rendering(snapshot, resources.options, resources) { + /* completion */ + + def completion(range: Text.Range): List[Protocol.CompletionItem] = + semantic_completion(None, range) match { + case Some(Text.Info(complete_range, names: Completion.Names)) => + model.content.try_get_text(complete_range) match { + case Some(original) => + names.complete(complete_range, Completion.History.empty, + resources.decode_text, original) match { + case Some(result) => + result.items.map(item => + Protocol.CompletionItem( + label = item.replacement, + detail = Some(item.description.mkString(" ")), + range = Some(model.content.doc.range(item.range)))) + case None => Nil + } + case None => Nil + } + case _ => Nil + } + + /* diagnostics */ def diagnostics: List[Text.Info[Command.Results]] = diff -r 65a247444100 -r 31e9920a0dc1 src/Tools/VSCode/src/vscode_resources.scala --- a/src/Tools/VSCode/src/vscode_resources.scala Wed Jan 11 16:43:31 2017 +0100 +++ b/src/Tools/VSCode/src/vscode_resources.scala Wed Jan 11 20:01:55 2017 +0100 @@ -251,8 +251,10 @@ /* output text */ + def decode_text: Boolean = options.bool("vscode_unicode_symbols") + def output_text(s: String): String = - if (options.bool("vscode_unicode_symbols")) Symbol.decode(s) else Symbol.encode(s) + if (decode_text) Symbol.decode(s) else Symbol.encode(s) def output_pretty(body: XML.Body, margin: Int): String = output_text(Pretty.string_of(body, margin)) diff -r 65a247444100 -r 31e9920a0dc1 src/Tools/jEdit/src/jedit_rendering.scala --- a/src/Tools/jEdit/src/jedit_rendering.scala Wed Jan 11 16:43:31 2017 +0100 +++ b/src/Tools/jEdit/src/jedit_rendering.scala Wed Jan 11 20:01:55 2017 +0100 @@ -113,9 +113,6 @@ private val indentation_elements = Markup.Elements(Markup.Command_Indent.name) - private val semantic_completion_elements = - Markup.Elements(Markup.COMPLETION, Markup.NO_COMPLETION) - private val language_context_elements = Markup.Elements(Markup.STRING, Markup.ALT_STRING, Markup.VERBATIM, Markup.CARTOUCHE, Markup.COMMENT, Markup.LANGUAGE, @@ -262,21 +259,6 @@ /* completion */ - def semantic_completion(completed_range: Option[Text.Range], range: Text.Range) - : Option[Text.Info[Completion.Semantic]] = - if (snapshot.is_outdated) None - else { - snapshot.select(range, JEdit_Rendering.semantic_completion_elements, _ => - { - case Completion.Semantic.Info(info) => - completed_range match { - case Some(range0) if range0.contains(info.range) && range0 != info.range => None - case _ => Some(info) - } - case _ => None - }).headOption.map(_.info) - } - def language_context(range: Text.Range): Option[Completion.Language_Context] = snapshot.select(range, JEdit_Rendering.language_context_elements, _ => {