--- a/src/Pure/Thy/thy_syntax.scala Sun Mar 04 11:03:10 2012 +0100
+++ b/src/Pure/Thy/thy_syntax.scala Sun Mar 04 16:02:14 2012 +0100
@@ -27,8 +27,7 @@
def length: Int = command.length
}
- def parse(syntax: Outer_Syntax, node_name: Document.Node.Name, text: CharSequence)
- : Entry =
+ def parse(syntax: Outer_Syntax, node_name: Document.Node.Name, text: CharSequence): Entry =
{
/* stack operations */
@@ -82,18 +81,10 @@
{
val result = new mutable.ListBuffer[List[Token]]
val span = new mutable.ListBuffer[Token]
- val whitespace = new mutable.ListBuffer[Token]
- 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)
+ def flush() { if (!span.isEmpty) { result += span.toList; span.clear } }
+ for (tok <- toks) { if (tok.is_command) flush(); span += tok }
+ flush()
result.toList
}