# HG changeset patch
# User wenzelm
# Date 1395264387 -3600
# Node ID a8dfbe9f25daeee07f8b354ceb4454dabe3307de
# Parent  4c43a2881b2578736038d417239ce394360748c6
accomodate word as part of schematic variable name;

diff -r 4c43a2881b25 -r a8dfbe9f25da src/Pure/General/completion.scala
--- a/src/Pure/General/completion.scala	Wed Mar 19 22:10:33 2014 +0100
+++ b/src/Pure/General/completion.scala	Wed Mar 19 22:26:27 2014 +0100
@@ -250,7 +250,8 @@
       val reverse_in = new Library.Reverse(in)
       val parser =
         (reverse_symbol | reverse_symb | escape) ^^ (x => (x.reverse, "")) |
-        underscores ~ parse_word ^^ { case x ~ y => (y.reverse, x) }
+        underscores ~ parse_word ~ opt("?") ^^
+        { case x ~ y ~ z => (z.getOrElse("") + y.reverse, x) }
       parse(parser, reverse_in) match {
         case Success(result, _) => Some(result)
         case _ => None