parse_spans: somewhat faster low-level implementation;

--- a/src/Pure/Thy/thy_syntax.scala	Sun Aug 08 20:03:31 2010 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Sun Aug 08 22:33:41 2010 +0200
@@ -7,30 +7,29 @@
 package isabelle
 
 
+import scala.collection.mutable
+
+
 object Thy_Syntax
 {
-  private val parser = new Parse.Parser
-  {
-    override def filter_proper = false
-
-    val command_span: Parser[Span] =
-    {
-      val whitespace = token("white space", _.is_ignored)
-      val command = token("command keyword", _.is_command)
-      val body = not(rep(whitespace) ~ (command | eof)) ~> not_eof
-      command ~ rep(body) ^^ { case x ~ ys => x :: ys } | rep1(whitespace) | rep1(body)
-    }
-  }
-
   type Span = List[Token]
 
   def parse_spans(toks: List[Token]): List[Span] =
   {
-    import parser._
+    val result = new mutable.ListBuffer[Span]
+    val span = new mutable.ListBuffer[Token]
+    val whitespace = new mutable.ListBuffer[Token]
 
-    parse(rep(command_span), Token.reader(toks)) match {
-      case Success(spans, rest) if rest.atEnd => spans
-      case bad => error(bad.toString)
+    def flush(buffer: mutable.ListBuffer[Token])
+    {
+      if (!buffer.isEmpty) { result += buffer.toList; buffer.clear }
     }
+    for (tok <- toks) {
+      if (tok.is_command) { flush(span); flush(whitespace); span += tok }
+      else if (tok.is_ignored) whitespace += tok
+      else { span ++= whitespace; whitespace.clear; span += tok }
+    }
+    flush(span); flush(whitespace)
+    result.toList
   }
 }