# 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