31 |
31 |
32 |
32 |
33 class Command( |
33 class Command( |
34 val id: Isar_Document.Command_ID, |
34 val id: Isar_Document.Command_ID, |
35 val tokens: List[Token], |
35 val tokens: List[Token], |
36 val starts: Map[Token, Int]) |
36 val starts: Map[Token, Int]) // FIXME eliminate |
37 extends Session.Entity |
37 extends Session.Entity |
38 { |
38 { |
39 require(!tokens.isEmpty) |
39 require(!tokens.isEmpty) |
40 |
40 |
41 // FIXME override equality as well |
41 // FIXME override equality as well |
47 override def toString = name |
47 override def toString = name |
48 |
48 |
49 val name = tokens.head.content |
49 val name = tokens.head.content |
50 val content: String = Token.string_from_tokens(tokens, starts) |
50 val content: String = Token.string_from_tokens(tokens, starts) |
51 def content(i: Int, j: Int): String = content.substring(i, j) |
51 def content(i: Int, j: Int): String = content.substring(i, j) |
52 val symbol_index = new Symbol.Index(content) |
52 lazy val symbol_index = new Symbol.Index(content) |
53 |
53 |
54 def start(doc: Document) = doc.token_start(tokens.first) |
54 def start(doc: Document) = doc.token_start(tokens.first) |
55 def stop(doc: Document) = doc.token_start(tokens.last) + tokens.last.length |
55 def stop(doc: Document) = doc.token_start(tokens.last) + tokens.last.length |
56 |
56 |
57 def contains(p: Token) = tokens.contains(p) |
57 def contains(p: Token) = tokens.contains(p) |
61 |
61 |
62 @volatile protected var state = new State(this) |
62 @volatile protected var state = new State(this) |
63 def current_state: State = state |
63 def current_state: State = state |
64 |
64 |
65 private case class Consume(session: Session, message: XML.Tree) |
65 private case class Consume(session: Session, message: XML.Tree) |
66 private case object Finish |
66 private case object Assign |
67 |
67 |
68 private val accumulator = actor { |
68 private val accumulator = actor { |
69 var finished = false |
69 var assigned = false |
70 loop { |
70 loop { |
71 react { |
71 react { |
72 case Consume(session: Session, message: XML.Tree) if !finished => |
72 case Consume(session: Session, message: XML.Tree) if !assigned => |
73 state = state.+(session, message) |
73 state = state.+(session, message) |
74 |
74 |
75 case Finish => finished = true; reply(()) |
75 case Assign => |
|
76 assigned = true // single assigment |
|
77 reply(()) |
76 |
78 |
77 case bad => System.err.println("command accumulator: ignoring bad message " + bad) |
79 case bad => System.err.println("command accumulator: ignoring bad message " + bad) |
78 } |
80 } |
79 } |
81 } |
80 } |
82 } |
81 |
83 |
82 def consume(session: Session, message: XML.Tree) { accumulator ! Consume(session, message) } |
84 def consume(session: Session, message: XML.Tree) { accumulator ! Consume(session, message) } |
83 |
85 |
84 def finish_static(state_id: Isar_Document.State_ID): Command = |
86 def assign_state(state_id: Isar_Document.State_ID): Command = |
85 { |
87 { |
86 val cmd = new Command(state_id, tokens, starts) |
88 val cmd = new Command(state_id, tokens, starts) |
87 accumulator !? Finish |
89 accumulator !? Assign |
88 cmd.state = current_state |
90 cmd.state = current_state |
89 cmd |
91 cmd |
90 } |
92 } |
91 |
93 |
92 |
94 |
98 { |
100 { |
99 val start = symbol_index.decode(begin) |
101 val start = symbol_index.decode(begin) |
100 val stop = symbol_index.decode(end) |
102 val stop = symbol_index.decode(end) |
101 new Markup_Tree(new Markup_Node(start, stop, info), Nil) |
103 new Markup_Tree(new Markup_Node(start, stop, info), Nil) |
102 } |
104 } |
103 |
|
104 |
|
105 /* results, markup, etc. */ |
|
106 |
|
107 def results: List[XML.Tree] = current_state.results |
|
108 def markup_root: Markup_Text = current_state.markup_root |
|
109 def type_at(pos: Int): Option[String] = current_state.type_at(pos) |
|
110 def ref_at(pos: Int): Option[Markup_Node] = current_state.ref_at(pos) |
|
111 def highlight: Markup_Text = current_state.highlight |
|
112 |
|
113 |
|
114 private def cmd_state(doc: Document): State = // FIXME clarify |
|
115 doc.states.getOrElse(this, this).current_state |
|
116 |
|
117 def status(doc: Document) = cmd_state(doc).status |
|
118 def results(doc: Document) = cmd_state(doc).results |
|
119 def markup_root(doc: Document) = cmd_state(doc).markup_root |
|
120 def highlight(doc: Document) = cmd_state(doc).highlight |
|
121 def type_at(doc: Document, offset: Int) = cmd_state(doc).type_at(offset) |
|
122 def ref_at(doc: Document, offset: Int) = cmd_state(doc).ref_at(offset) |
|
123 } |
105 } |