--- a/src/Pure/Isar/outer_syntax.scala Sat Nov 04 17:11:21 2017 +0100
+++ b/src/Pure/Isar/outer_syntax.scala Sat Nov 04 18:57:49 2017 +0100
@@ -83,7 +83,7 @@
/* completion */
- lazy val completion: Completion =
+ private lazy val completion: Completion =
{
val completion_keywords = (keywords.minor.iterator ++ keywords.major.iterator).toList
val completion_abbrevs =
@@ -102,6 +102,18 @@
Completion.make(completion_keywords, completion_abbrevs)
}
+ def complete(
+ history: Completion.History,
+ unicode: Boolean,
+ explicit: Boolean,
+ start: Text.Offset,
+ text: CharSequence,
+ caret: Int,
+ context: Completion.Language_Context): Option[Completion.Result] =
+ {
+ completion.complete(history, unicode, explicit, start, text, caret, context)
+ }
+
/* build */
--- a/src/Tools/VSCode/src/vscode_rendering.scala Sat Nov 04 17:11:21 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala Sat Nov 04 18:57:49 2017 +0100
@@ -97,7 +97,7 @@
val syntax = model.syntax()
val syntax_completion =
- syntax.completion.complete(history, unicode = false, explicit = true,
+ syntax.complete(history, unicode = false, explicit = true,
line_start, doc.lines(line).text, caret - line_start,
language_context(caret_range) getOrElse syntax.language_context)
--- a/src/Tools/jEdit/src/completion_popup.scala Sat Nov 04 17:11:21 2017 +0100
+++ b/src/Tools/jEdit/src/completion_popup.scala Sat Nov 04 18:57:49 2017 +0100
@@ -173,7 +173,7 @@
for {
line_text <- JEdit_Lib.try_get_text(buffer, line_range)
result <-
- syntax.completion.complete(
+ syntax.complete(
history, unicode, explicit, line_start, line_text, caret - line_start, context)
} yield result
@@ -483,7 +483,7 @@
val context = syntax.language_context
- syntax.completion.complete(history, true, false, 0, text, caret, context) match {
+ syntax.complete(history, true, false, 0, text, caret, context) match {
case Some(result) =>
val fm = text_field.getFontMetrics(text_field.getFont)
val loc =