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