src/Pure/Thy/thy_syntax.scala

--- a/src/Pure/Thy/thy_syntax.scala	Fri Aug 13 21:33:13 2010 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Sat Aug 14 11:52:24 2010 +0200
@@ -12,11 +12,9 @@
 
 object Thy_Syntax
 {
-  type Span = List[Token]
-
-  def parse_spans(toks: List[Token]): List[Span] =
+  def parse_spans(toks: List[Token]): List[List[Token]] =
   {
-    val result = new mutable.ListBuffer[Span]
+    val result = new mutable.ListBuffer[List[Token]]
     val span = new mutable.ListBuffer[Token]
     val whitespace = new mutable.ListBuffer[Token]