equal
deleted
inserted
replaced
89 : Outer_Syntax = |
89 : Outer_Syntax = |
90 { |
90 { |
91 val keywords1 = keywords + (name, kind, tags) |
91 val keywords1 = keywords + (name, kind, tags) |
92 val completion1 = |
92 val completion1 = |
93 if (replace == Some("")) completion |
93 if (replace == Some("")) completion |
|
94 else if (replace.isEmpty && Keyword.theory_block.contains(kind)) |
|
95 completion + (name, name + "\nbegin\n\u0007\nend") + (name, name) |
94 else completion + (name, replace getOrElse name) |
96 else completion + (name, replace getOrElse name) |
95 new Outer_Syntax(keywords1, completion1, language_context, true) |
97 new Outer_Syntax(keywords1, completion1, language_context, true) |
96 } |
98 } |
97 |
99 |
98 def add_keywords(keywords: Thy_Header.Keywords): Outer_Syntax = |
100 def add_keywords(keywords: Thy_Header.Keywords): Outer_Syntax = |