src/Pure/System/session.scala
changeset 38414 49f1f657adc2
parent 38413 224efb14f258
child 38415 f3220ef79d51
     1.1 --- a/src/Pure/System/session.scala	Sat Aug 14 21:25:20 2010 +0200
     1.2 +++ b/src/Pure/System/session.scala	Sat Aug 14 22:45:23 2010 +0200
     1.3 @@ -132,27 +132,19 @@
     1.4        raw_results.event(result)
     1.5  
     1.6        Position.get_id(result.properties) match {
     1.7 -        case Some(target_id) =>
     1.8 +        case Some(state_id) =>
     1.9            try {
    1.10 -            val (st, state) = global_state.accumulate(target_id, result.message)
    1.11 +            val (st, state) = global_state.accumulate(state_id, result.message)
    1.12              global_state = state
    1.13 -            indicate_command_change(st.command)  // FIXME forward Command.State (!?)
    1.14 +            indicate_command_change(st.command)
    1.15            }
    1.16 -          catch {
    1.17 -            case _: Document.State.Fail =>
    1.18 -              if (result.is_status) {
    1.19 -                result.body match {
    1.20 -                  case List(Isar_Document.Assign(edits)) =>
    1.21 -                    try { change_state(_.assign(target_id, edits)) }
    1.22 -                    catch { case _: Document.State.Fail => bad_result(result) }
    1.23 -                  case _ => bad_result(result)
    1.24 -                }
    1.25 -              }
    1.26 -              else bad_result(result)
    1.27 -          }
    1.28 +          catch { case _: Document.State.Fail => bad_result(result) }
    1.29          case None =>
    1.30            if (result.is_status) {
    1.31              result.body match {
    1.32 +              case List(Isar_Document.Assign(doc_id, edits)) =>
    1.33 +                try { change_state(_.assign(doc_id, edits)) }
    1.34 +                catch { case _: Document.State.Fail => bad_result(result) }
    1.35                case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
    1.36                case List(Keyword.Keyword_Decl(name)) => syntax += name
    1.37                case _ => if (!result.is_ready) bad_result(result)