src/Pure/Thy/thy_syntax.scala
changeset 38373 e8197eea3cd0
parent 38239 89a4d1028fb3
child 38374 7eb0f6991e25
     1.1 --- a/src/Pure/Thy/thy_syntax.scala	Fri Aug 13 21:33:13 2010 +0200
     1.2 +++ b/src/Pure/Thy/thy_syntax.scala	Sat Aug 14 11:52:24 2010 +0200
     1.3 @@ -12,11 +12,9 @@
     1.4  
     1.5  object Thy_Syntax
     1.6  {
     1.7 -  type Span = List[Token]
     1.8 -
     1.9 -  def parse_spans(toks: List[Token]): List[Span] =
    1.10 +  def parse_spans(toks: List[Token]): List[List[Token]] =
    1.11    {
    1.12 -    val result = new mutable.ListBuffer[Span]
    1.13 +    val result = new mutable.ListBuffer[List[Token]]
    1.14      val span = new mutable.ListBuffer[Token]
    1.15      val whitespace = new mutable.ListBuffer[Token]
    1.16