# HG changeset patch
# User wenzelm
# Date 1261219691 -3600
# Node ID 63dd95e3b39325e2cbc67375726326d2308de66f
# Parent  d8d9df8407f65a2a35d8ed753e3774a7fdfa3004
indicate final state of keywords;
added symbol scanner;

diff -r d8d9df8407f6 -r 63dd95e3b393 src/Pure/General/scan.scala
--- a/src/Pure/General/scan.scala	Sat Dec 19 11:45:14 2009 +0100
+++ b/src/Pure/General/scan.scala	Sat Dec 19 11:48:11 2009 +0100
@@ -91,7 +91,8 @@
                 Tree(tree.branches +
                   (c -> (if (end) elem else "", extend(Lexicon.empty_tree, i + 1))))
             }
-          } else tree
+          }
+          else tree
         val old = this
         new Lexicon { override val main_tree = extend(old.main_tree, 0) }
       }
@@ -106,28 +107,45 @@
 
     override val whiteSpace = "".r
 
-    def keyword: Parser[String] = new Parser[String] {
+    type Result = (String, Boolean)
+
+    def keyword: Parser[Result] = new Parser[Result]
+    {
       def apply(in: Input) =
       {
         val source = in.source
         val offset = in.offset
         val len = source.length - offset
 
-        def scan(tree: Tree, text: String, i: Int): String =
+        def scan(tree: Tree, result: Result, i: Int): Result =
         {
           if (i < len) {
             tree.branches.get(source.charAt(offset + i)) match {
-              case Some((s, tr)) => scan(tr, if (s.isEmpty) text else s, i + 1)
-              case None => text
+              case Some((s, tr)) =>
+                scan(tr, if (s.isEmpty) result else (s, tr.branches.isEmpty), i + 1)
+              case None => result
             }
-          } else text
+          }
+          else result
         }
-        val text = scan(main_tree, "", 0)
+        val result @ (text, terminated) = scan(main_tree, ("", false), 0)
         if (text.isEmpty) Failure("keyword expected", in)
-        else Success(text, in.drop(text.length))
+        else Success(result, in.drop(text.length))
       }
     }.named("keyword")
 
+    def symbol: Parser[String] = new Parser[String]
+    {
+      private val symbol_regex = regex(Symbol.regex)
+      def apply(in: Input) =
+      {
+        val source = in.source
+        val offset = in.offset
+        if (offset >= source.length) Failure("input expected", in)
+        else if (Symbol.could_open(source.charAt(offset))) symbol_regex(in)
+        else Success(source.subSequence(offset, offset + 1).toString, in.drop(1))
+      }
+    }.named("symbol")
   }
 }
 
diff -r d8d9df8407f6 -r 63dd95e3b393 src/Pure/Thy/completion.scala
--- a/src/Pure/Thy/completion.scala	Sat Dec 19 11:45:14 2009 +0100
+++ b/src/Pure/Thy/completion.scala	Sat Dec 19 11:48:11 2009 +0100
@@ -114,7 +114,7 @@
   def complete(line: CharSequence): Option[(String, List[String])] =
   {
     abbrevs_lex.parse(abbrevs_lex.keyword, new Completion.Reverse(line)) match {
-      case abbrevs_lex.Success(rev_a, _) =>
+      case abbrevs_lex.Success((rev_a, _), _) =>
         val (word, c) = abbrevs_map(rev_a)
         if (word == c) None
         else Some(word, List(c))