# HG changeset patch # User wenzelm # Date 1312802359 -7200 # Node ID 2ec66075a75cb627b29ad1572ad850b55d2f33b2 # Parent f7634e2300bce581e588508b0e1f47dd0db14854 avoid pointless completion of illegal control commands; diff -r f7634e2300bc -r 2ec66075a75c src/Pure/Isar/outer_syntax.scala --- a/src/Pure/Isar/outer_syntax.scala Mon Aug 08 08:56:58 2011 +0200 +++ b/src/Pure/Isar/outer_syntax.scala Mon Aug 08 13:19:19 2011 +0200 @@ -47,7 +47,9 @@ { val new_keywords = keywords + (name -> kind) val new_lexicon = lexicon + name - val new_completion = completion + (name, replace) + val new_completion = + if (Keyword.control(kind)) completion + else completion + (name, replace) new Outer_Syntax { override val lexicon = new_lexicon override val keywords = new_keywords