src/Pure/System/session.scala
changeset 38373 e8197eea3cd0
parent 38370 8b15d0f98962
child 38374 7eb0f6991e25
     1.1 --- a/src/Pure/System/session.scala	Fri Aug 13 21:33:13 2010 +0200
     1.2 +++ b/src/Pure/System/session.scala	Sat Aug 14 11:52:24 2010 +0200
     1.3 @@ -139,12 +139,12 @@
     1.4              indicate_command_change(st.command)  // FIXME forward Command.State (!?)
     1.5            }
     1.6            catch {
     1.7 -            case _: Document.Failed_State =>
     1.8 +            case _: Document.State.Fail =>
     1.9                if (result.is_status) {
    1.10                  result.body match {
    1.11                    case List(Isar_Document.Assign(edits)) =>
    1.12                      try { change_state(_.assign(target_id, edits)) }
    1.13 -                    catch { case _: Document.Failed_State => bad_result(result) }
    1.14 +                    catch { case _: Document.State.Fail => bad_result(result) }
    1.15                    case _ => bad_result(result)
    1.16                  }
    1.17                }