--- a/src/Pure/Thy/thy_syntax.scala Fri Jul 05 18:37:44 2013 +0200
+++ b/src/Pure/Thy/thy_syntax.scala Fri Jul 05 22:09:16 2013 +0200
@@ -77,9 +77,9 @@
/** parse spans **/
- def parse_spans(toks: List[Token]): List[Command.Span] =
+ def parse_spans(toks: List[Token]): List[List[Token]] =
{
- val result = new mutable.ListBuffer[Command.Span]
+ val result = new mutable.ListBuffer[List[Token]]
val span = new mutable.ListBuffer[Token]
def flush() { if (!span.isEmpty) { result += span.toList; span.clear } }
@@ -198,7 +198,7 @@
/* reparse range of command spans */
@tailrec private def chop_common(
- cmds: List[Command], spans: List[Command.Span]): (List[Command], List[Command.Span]) =
+ cmds: List[Command], spans: List[List[Token]]): (List[Command], List[List[Token]]) =
(cmds, spans) match {
case (c :: cs, s :: ss) if c.span == s => chop_common(cs, ss)
case _ => (cmds, spans)