11 import scala.annotation.tailrec |
11 import scala.annotation.tailrec |
12 |
12 |
13 |
13 |
14 object Thy_Syntax |
14 object Thy_Syntax |
15 { |
15 { |
16 /** nested structure **/ |
|
17 |
|
18 object Structure |
|
19 { |
|
20 sealed abstract class Entry { def length: Int } |
|
21 case class Block(val name: String, val body: List[Entry]) extends Entry |
|
22 { |
|
23 val length: Int = (0 /: body)(_ + _.length) |
|
24 } |
|
25 case class Atom(val command: Command) extends Entry |
|
26 { |
|
27 def length: Int = command.length |
|
28 } |
|
29 |
|
30 def parse(syntax: Outer_Syntax, node_name: Document.Node.Name, text: CharSequence): Entry = |
|
31 { |
|
32 /* stack operations */ |
|
33 |
|
34 def buffer(): mutable.ListBuffer[Entry] = new mutable.ListBuffer[Entry] |
|
35 var stack: List[(Int, String, mutable.ListBuffer[Entry])] = |
|
36 List((0, node_name.toString, buffer())) |
|
37 |
|
38 @tailrec def close(level: Int => Boolean) |
|
39 { |
|
40 stack match { |
|
41 case (lev, name, body) :: (_, _, body2) :: rest if level(lev) => |
|
42 body2 += Block(name, body.toList) |
|
43 stack = stack.tail |
|
44 close(level) |
|
45 case _ => |
|
46 } |
|
47 } |
|
48 |
|
49 def result(): Entry = |
|
50 { |
|
51 close(_ => true) |
|
52 val (_, name, body) = stack.head |
|
53 Block(name, body.toList) |
|
54 } |
|
55 |
|
56 def add(command: Command) |
|
57 { |
|
58 syntax.heading_level(command) match { |
|
59 case Some(i) => |
|
60 close(_ > i) |
|
61 stack = (i + 1, command.source, buffer()) :: stack |
|
62 case None => |
|
63 } |
|
64 stack.head._3 += Atom(command) |
|
65 } |
|
66 |
|
67 |
|
68 /* result structure */ |
|
69 |
|
70 val spans = parse_spans(syntax.scan(text)) |
|
71 spans.foreach(span => add(Command(Document_ID.none, node_name, Nil, span))) |
|
72 result() |
|
73 } |
|
74 } |
|
75 |
|
76 |
|
77 |
|
78 /** parse spans **/ |
16 /** parse spans **/ |
79 |
17 |
80 def parse_spans(toks: List[Token]): List[List[Token]] = |
18 def parse_spans(toks: List[Token]): List[List[Token]] = |
81 { |
19 { |
82 val result = new mutable.ListBuffer[List[Token]] |
20 val result = new mutable.ListBuffer[List[Token]] |