src/Pure/Thy/thy_syntax.scala
author wenzelm
Sun Aug 08 22:33:41 2010 +0200 (2010-08-08)
changeset 38239 89a4d1028fb3
parent 36956 21be4832c362
child 38373 e8197eea3cd0
permissions -rw-r--r--
parse_spans: somewhat faster low-level implementation;
wenzelm@34268
     1
/*  Title:      Pure/Thy/thy_syntax.scala
wenzelm@34268
     2
    Author:     Makarius
wenzelm@34268
     3
wenzelm@34268
     4
Superficial theory syntax: command spans.
wenzelm@34268
     5
*/
wenzelm@34268
     6
wenzelm@34268
     7
package isabelle
wenzelm@34268
     8
wenzelm@34268
     9
wenzelm@38239
    10
import scala.collection.mutable
wenzelm@38239
    11
wenzelm@38239
    12
wenzelm@34303
    13
object Thy_Syntax
wenzelm@34268
    14
{
wenzelm@36956
    15
  type Span = List[Token]
wenzelm@34268
    16
wenzelm@36956
    17
  def parse_spans(toks: List[Token]): List[Span] =
wenzelm@34268
    18
  {
wenzelm@38239
    19
    val result = new mutable.ListBuffer[Span]
wenzelm@38239
    20
    val span = new mutable.ListBuffer[Token]
wenzelm@38239
    21
    val whitespace = new mutable.ListBuffer[Token]
wenzelm@34268
    22
wenzelm@38239
    23
    def flush(buffer: mutable.ListBuffer[Token])
wenzelm@38239
    24
    {
wenzelm@38239
    25
      if (!buffer.isEmpty) { result += buffer.toList; buffer.clear }
wenzelm@34268
    26
    }
wenzelm@38239
    27
    for (tok <- toks) {
wenzelm@38239
    28
      if (tok.is_command) { flush(span); flush(whitespace); span += tok }
wenzelm@38239
    29
      else if (tok.is_ignored) whitespace += tok
wenzelm@38239
    30
      else { span ++= whitespace; whitespace.clear; span += tok }
wenzelm@38239
    31
    }
wenzelm@38239
    32
    flush(span); flush(whitespace)
wenzelm@38239
    33
    result.toList
wenzelm@34268
    34
  }
wenzelm@34268
    35
}