--- a/src/Pure/System/session.scala Sat Aug 14 21:25:20 2010 +0200
+++ b/src/Pure/System/session.scala Sat Aug 14 22:45:23 2010 +0200
@@ -132,27 +132,19 @@
raw_results.event(result)
Position.get_id(result.properties) match {
- case Some(target_id) =>
+ case Some(state_id) =>
try {
- val (st, state) = global_state.accumulate(target_id, result.message)
+ val (st, state) = global_state.accumulate(state_id, result.message)
global_state = state
- indicate_command_change(st.command) // FIXME forward Command.State (!?)
+ indicate_command_change(st.command)
}
- catch {
- case _: Document.State.Fail =>
- if (result.is_status) {
- result.body match {
- case List(Isar_Document.Assign(edits)) =>
- try { change_state(_.assign(target_id, edits)) }
- catch { case _: Document.State.Fail => bad_result(result) }
- case _ => bad_result(result)
- }
- }
- else bad_result(result)
- }
+ catch { case _: Document.State.Fail => bad_result(result) }
case None =>
if (result.is_status) {
result.body match {
+ case List(Isar_Document.Assign(doc_id, edits)) =>
+ try { change_state(_.assign(doc_id, edits)) }
+ catch { case _: Document.State.Fail => bad_result(result) }
case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
case List(Keyword.Keyword_Decl(name)) => syntax += name
case _ => if (!result.is_ready) bad_result(result)