src/Pure/Isar/outer_syntax.scala
changeset 67005 11fca474d87a
parent 67004 af72fa58f71b
child 68729 3a02b424d5fb
     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