# HG changeset patch
# User wenzelm
# Date 1261328533 -3600
# Node ID bd7b3b91ababdc3897a4e04aea18faa07edde1d8
# Parent  ded454429df36c37f432c9802887d07d48571957
improve performance by reordering of parser combinators;

diff -r ded454429df3 -r bd7b3b91abab src/Pure/General/scan.scala
--- a/src/Pure/General/scan.scala	Sun Dec 20 17:47:59 2009 +0100
+++ b/src/Pure/General/scan.scala	Sun Dec 20 18:02:13 2009 +0100
@@ -275,10 +275,8 @@
 
       /* tokens */
 
-      // FIXME right-assoc !?
-
-      (string | alt_string | verbatim ^^ Verbatim | comment ^^ Comment | space) |
-      ((ident | var_ | type_ident | type_var | nat_ | sym_ident) |||
+      (space | (string | (alt_string | (verbatim ^^ Verbatim | comment ^^ Comment)))) |
+      ((ident | (var_ | (type_ident | (type_var | (nat_ | sym_ident))))) |||
         keyword ^^ (x => if (is_command(x)) Command(x) else Keyword(x))) |
       bad_input
     }