src/Pure/System/session.scala

             val st = global_state.change_yield(_.accumulate(state_id, result.message))
             command_change_buffer ! st.command
           }
           catch { case _: Document.State.Fail => bad_result(result) }
         case _ =>
-          if (result.is_status) {
+          if (result.is_exit) prover = null  // FIXME ??
+          else if (result.is_syslog || result.is_stdout) { }
+          else if (result.is_status) {
             result.body match {
               case List(Isar_Document.Assign(id, edits)) =>
                 try {
                   val cmds: List[Command] = global_state.change_yield(_.assign(id, edits))
                   for (cmd <- cmds) command_change_buffer ! cmd
                   assignments.event(Session.Assignment)
                 }
                 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)
+              case _ => bad_result(result)
             }
           }
-          else if (result.is_exit) prover = null  // FIXME ??
-          else if (!(result.is_init || result.is_exit || result.is_system || result.is_stdout))
-            bad_result(result)
+          else bad_result(result)
         }
     }
     //}}}