tuned signature;
authorwenzelm
Sat Nov 04 18:57:49 2017 +0100 (17 months ago)
changeset 6700511fca474d87a
parent 67004 af72fa58f71b
child 67006 b1278ed3cd46
tuned signature;
src/Pure/Isar/outer_syntax.scala
src/Tools/VSCode/src/vscode_rendering.scala
src/Tools/jEdit/src/completion_popup.scala
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Sat Nov 04 17:11:21 2017 +0100
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Sat Nov 04 18:57:49 2017 +0100
     1.3 @@ -83,7 +83,7 @@
     1.4  
     1.5    /* completion */
     1.6  
     1.7 -  lazy val completion: Completion =
     1.8 +  private lazy val completion: Completion =
     1.9    {
    1.10      val completion_keywords = (keywords.minor.iterator ++ keywords.major.iterator).toList
    1.11      val completion_abbrevs =
    1.12 @@ -102,6 +102,18 @@
    1.13      Completion.make(completion_keywords, completion_abbrevs)
    1.14    }
    1.15  
    1.16 +  def complete(
    1.17 +    history: Completion.History,
    1.18 +    unicode: Boolean,
    1.19 +    explicit: Boolean,
    1.20 +    start: Text.Offset,
    1.21 +    text: CharSequence,
    1.22 +    caret: Int,
    1.23 +    context: Completion.Language_Context): Option[Completion.Result] =
    1.24 +  {
    1.25 +    completion.complete(history, unicode, explicit, start, text, caret, context)
    1.26 +  }
    1.27 +
    1.28  
    1.29    /* build */
    1.30  
     2.1 --- a/src/Tools/VSCode/src/vscode_rendering.scala	Sat Nov 04 17:11:21 2017 +0100
     2.2 +++ b/src/Tools/VSCode/src/vscode_rendering.scala	Sat Nov 04 18:57:49 2017 +0100
     2.3 @@ -97,7 +97,7 @@
     2.4  
     2.5          val syntax = model.syntax()
     2.6          val syntax_completion =
     2.7 -          syntax.completion.complete(history, unicode = false, explicit = true,
     2.8 +          syntax.complete(history, unicode = false, explicit = true,
     2.9              line_start, doc.lines(line).text, caret - line_start,
    2.10              language_context(caret_range) getOrElse syntax.language_context)
    2.11  
     3.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Sat Nov 04 17:11:21 2017 +0100
     3.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Sat Nov 04 18:57:49 2017 +0100
     3.3 @@ -173,7 +173,7 @@
     3.4            for {
     3.5              line_text <- JEdit_Lib.try_get_text(buffer, line_range)
     3.6              result <-
     3.7 -              syntax.completion.complete(
     3.8 +              syntax.complete(
     3.9                  history, unicode, explicit, line_start, line_text, caret - line_start, context)
    3.10            } yield result
    3.11  
    3.12 @@ -483,7 +483,7 @@
    3.13  
    3.14            val context = syntax.language_context
    3.15  
    3.16 -          syntax.completion.complete(history, true, false, 0, text, caret, context) match {
    3.17 +          syntax.complete(history, true, false, 0, text, caret, context) match {
    3.18              case Some(result) =>
    3.19                val fm = text_field.getFontMetrics(text_field.getFont)
    3.20                val loc =