130 //{{{ |
130 //{{{ |
131 { |
131 { |
132 raw_results.event(result) |
132 raw_results.event(result) |
133 |
133 |
134 Position.get_id(result.properties) match { |
134 Position.get_id(result.properties) match { |
135 case Some(target_id) => |
135 case Some(state_id) => |
136 try { |
136 try { |
137 val (st, state) = global_state.accumulate(target_id, result.message) |
137 val (st, state) = global_state.accumulate(state_id, result.message) |
138 global_state = state |
138 global_state = state |
139 indicate_command_change(st.command) // FIXME forward Command.State (!?) |
139 indicate_command_change(st.command) |
140 } |
140 } |
141 catch { |
141 catch { case _: Document.State.Fail => bad_result(result) } |
142 case _: Document.State.Fail => |
|
143 if (result.is_status) { |
|
144 result.body match { |
|
145 case List(Isar_Document.Assign(edits)) => |
|
146 try { change_state(_.assign(target_id, edits)) } |
|
147 catch { case _: Document.State.Fail => bad_result(result) } |
|
148 case _ => bad_result(result) |
|
149 } |
|
150 } |
|
151 else bad_result(result) |
|
152 } |
|
153 case None => |
142 case None => |
154 if (result.is_status) { |
143 if (result.is_status) { |
155 result.body match { |
144 result.body match { |
|
145 case List(Isar_Document.Assign(doc_id, edits)) => |
|
146 try { change_state(_.assign(doc_id, edits)) } |
|
147 catch { case _: Document.State.Fail => bad_result(result) } |
156 case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind) |
148 case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind) |
157 case List(Keyword.Keyword_Decl(name)) => syntax += name |
149 case List(Keyword.Keyword_Decl(name)) => syntax += name |
158 case _ => if (!result.is_ready) bad_result(result) |
150 case _ => if (!result.is_ready) bad_result(result) |
159 } |
151 } |
160 } |
152 } |