--- a/src/Pure/PIDE/rendering.scala Fri Jun 09 19:23:29 2017 +0200
+++ b/src/Pure/PIDE/rendering.scala Fri Jun 09 21:43:31 2017 +0200
@@ -206,11 +206,11 @@
/* completion */
- def semantic_completion(completed_range: Option[Text.Range], range: Text.Range)
+ def semantic_completion(completed_range: Option[Text.Range], caret_range: Text.Range)
: Option[Text.Info[Completion.Semantic]] =
if (snapshot.is_outdated) None
else {
- snapshot.select(range, Rendering.semantic_completion_elements, _ =>
+ snapshot.select(caret_range, Rendering.semantic_completion_elements, _ =>
{
case Completion.Semantic.Info(info) =>
completed_range match {
@@ -221,6 +221,24 @@
}).headOption.map(_.info)
}
+ def semantic_completion_result(
+ history: Completion.History,
+ decode: Boolean,
+ completed_range: Option[Text.Range],
+ caret_range: Text.Range,
+ try_get_text: Text.Range => Option[String]): (Boolean, Option[Completion.Result]) =
+ {
+ semantic_completion(completed_range, caret_range) match {
+ case Some(Text.Info(_, Completion.No_Completion)) => (true, None)
+ case Some(Text.Info(range, names: Completion.Names)) =>
+ try_get_text(range) match {
+ case Some(original) => (false, names.complete(range, history, decode, original))
+ case None => (false, None)
+ }
+ case None => (false, None)
+ }
+ }
+
def language_context(range: Text.Range): Option[Completion.Language_Context] =
snapshot.select(range, Rendering.language_context_elements, _ =>
{
--- a/src/Tools/VSCode/src/document_model.scala Fri Jun 09 19:23:29 2017 +0200
+++ b/src/Tools/VSCode/src/document_model.scala Fri Jun 09 21:43:31 2017 +0200
@@ -191,4 +191,12 @@
def rendering(snapshot: Document.Snapshot): VSCode_Rendering =
new VSCode_Rendering(this, snapshot)
def rendering(): VSCode_Rendering = rendering(snapshot())
+
+
+ /* syntax */
+
+ lazy private val syntax0 = Outer_Syntax.init()
+
+ def syntax(): Outer_Syntax =
+ if (is_theory) session.recent_syntax(node_name) else syntax0
}
--- a/src/Tools/VSCode/src/server.scala Fri Jun 09 19:23:29 2017 +0200
+++ b/src/Tools/VSCode/src/server.scala Fri Jun 09 21:43:31 2017 +0200
@@ -325,7 +325,7 @@
{
val result =
(for ((rendering, offset) <- rendering_offset(node_pos))
- yield rendering.completion(Text.Range(offset - 1, offset))) getOrElse Nil
+ yield rendering.completion(node_pos.pos, offset)) getOrElse Nil
channel.write(Protocol.Completion.reply(id, result))
}
--- a/src/Tools/VSCode/src/vscode_rendering.scala Fri Jun 09 19:23:29 2017 +0200
+++ b/src/Tools/VSCode/src/vscode_rendering.scala Fri Jun 09 21:43:31 2017 +0200
@@ -68,28 +68,56 @@
class VSCode_Rendering(val model: Document_Model, snapshot: Document.Snapshot)
extends Rendering(snapshot, model.resources.options, model.session)
{
+ rendering =>
+
+
/* 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,
- model.resources.unicode_symbols, 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
+ def before_caret_range(caret: Text.Offset): Text.Range =
+ {
+ val former_caret = snapshot.revert(caret)
+ snapshot.convert(Text.Range(former_caret - 1, former_caret))
+ }
+
+ def completion(caret_pos: Line.Position, caret: Text.Offset): List[Protocol.CompletionItem] =
+ {
+ val caret_range = before_caret_range(caret)
+
+ val history = Completion.History.empty
+ val doc = model.content.doc
+
+ val syntax_completion =
+ {
+ val syntax = model.syntax()
+ val context = language_context(caret_range) getOrElse syntax.language_context
+
+ val line = caret_pos.line
+ doc.offset(Line.Position(line)) match {
+ case Some(line_start) =>
+ syntax.completion.complete(history, false, true,
+ line_start, doc.lines(line).text, caret - line_start, context)
+ case None => None
+ }
}
+ val (no_completion, semantic_completion) =
+ rendering.semantic_completion_result(
+ history, false, syntax_completion.map(_.range), caret_range, doc.try_get_text(_))
+
+ if (no_completion) Nil
+ else {
+ Completion.Result.merge(history, semantic_completion, syntax_completion) match {
+ case None => Nil
+ case Some(result) =>
+ result.items.map(item =>
+ Protocol.CompletionItem(
+ label = item.replacement,
+ detail = Some(item.description.mkString(" ")),
+ range = Some(doc.range(item.range))))
+ }
+ }
+ }
+
/* diagnostics */
--- a/src/Tools/jEdit/src/completion_popup.scala Fri Jun 09 19:23:29 2017 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala Fri Jun 09 21:43:31 2017 +0200
@@ -164,8 +164,8 @@
(for {
rendering <- opt_rendering
if PIDE.options.bool("jedit_completion_context")
- range = JEdit_Lib.before_caret_range(text_area, rendering)
- context <- rendering.language_context(range)
+ caret_range = JEdit_Lib.before_caret_range(text_area, rendering)
+ context <- rendering.language_context(caret_range)
} yield context) getOrElse syntax.language_context
val caret = text_area.getCaretPosition
@@ -355,16 +355,9 @@
{
opt_rendering match {
case Some(rendering) =>
- val caret_range = JEdit_Lib.before_caret_range(text_area, rendering)
- rendering.semantic_completion(result0.map(_.range), caret_range) match {
- case Some(Text.Info(_, Completion.No_Completion)) => (true, None)
- case Some(Text.Info(range, names: Completion.Names)) =>
- JEdit_Lib.try_get_text(buffer, range) match {
- case Some(original) => (false, names.complete(range, history, decode, original))
- case None => (false, None)
- }
- case None => (false, None)
- }
+ rendering.semantic_completion_result(history, decode, result0.map(_.range),
+ JEdit_Lib.before_caret_range(text_area, rendering),
+ JEdit_Lib.try_get_text(buffer, _))
case None => (false, None)
}
}