src/Pure/Thy/thy_syntax.scala
author wenzelm
Sat, 14 Aug 2010 11:52:24 +0200
changeset 38373 e8197eea3cd0
parent 38239 89a4d1028fb3
child 38374 7eb0f6991e25
permissions -rw-r--r--
tuned;

/*  Title:      Pure/Thy/thy_syntax.scala
    Author:     Makarius

Superficial theory syntax: command spans.
*/

package isabelle


import scala.collection.mutable


object Thy_Syntax
{
  def parse_spans(toks: List[Token]): List[List[Token]] =
  {
    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)
    result.toList
  }
}