# HG changeset patch
# User wenzelm
# Date 1509818269 -3600
# Node ID 11fca474d87aec207bd486d253cf2d05847473f9
# Parent  af72fa58f71badb363e75a28321cb11f25c9fb35
tuned signature;

diff -r af72fa58f71b -r 11fca474d87a src/Pure/Isar/outer_syntax.scala
--- 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 */
 
diff -r af72fa58f71b -r 11fca474d87a src/Tools/VSCode/src/vscode_rendering.scala
--- 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)
 
diff -r af72fa58f71b -r 11fca474d87a src/Tools/jEdit/src/completion_popup.scala
--- 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 =