src/Pure/Isar/outer_syntax.scala
changeset 63528 0f39f59317c1
parent 63479 464ef556bd21
child 63579 73939a9b70a3
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Wed Jul 20 11:44:11 2016 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Wed Jul 20 16:02:00 2016 +0200
     1.3 @@ -91,6 +91,8 @@
     1.4      val keywords1 = keywords + (name, kind, tags)
     1.5      val completion1 =
     1.6        if (replace == Some("")) completion
     1.7 +      else if (replace.isEmpty && Keyword.theory_block.contains(kind))
     1.8 +        completion + (name, name + "\nbegin\n\u0007\nend") + (name, name)
     1.9        else completion + (name, replace getOrElse name)
    1.10      new Outer_Syntax(keywords1, completion1, language_context, true)
    1.11    }