src/Pure/Thy/thy_syntax.scala

parse_spans: somewhat faster low-level implementation;

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

Superficial theory syntax: command spans.
*/

package isabelle


import scala.collection.mutable


object Thy_Syntax
{
  type Span = List[Token]

  def parse_spans(toks: List[Token]): List[Span] =
  {
    val result = new mutable.ListBuffer[Span]
    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
  }
}