--- 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 =
--- 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
--- 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)
--- 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")
--- 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)
--- 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]] =
--- 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))
--- 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, _ =>
{