src/Pure/System/session.scala
changeset 51662 3391a493f39a
parent 51083 10062c40ddaa
child 51664 080ef458f21a
     1.1 --- a/src/Pure/System/session.scala	Tue Apr 09 15:59:02 2013 +0200
     1.2 +++ b/src/Pure/System/session.scala	Tue Apr 09 20:16:52 2013 +0200
     1.3 @@ -300,22 +300,31 @@
     1.4      def handle_output(output: Isabelle_Process.Output)
     1.5      //{{{
     1.6      {
     1.7 -      def bad_output(output: Isabelle_Process.Output)
     1.8 +      def bad_output()
     1.9        {
    1.10          if (verbose)
    1.11            System.err.println("Ignoring prover output: " + output.message.toString)
    1.12        }
    1.13  
    1.14 +      def accumulate(state_id: Document.ID, message: XML.Elem)
    1.15 +      {
    1.16 +        try {
    1.17 +          val st = global_state >>> (_.accumulate(state_id, message))
    1.18 +          delay_commands_changed.invoke(false, List(st.command))
    1.19 +        }
    1.20 +        catch {
    1.21 +          case _: Document.State.Fail => bad_output()
    1.22 +        }
    1.23 +      }
    1.24 +
    1.25        output.properties match {
    1.26  
    1.27          case Position.Id(state_id) if !output.is_protocol =>
    1.28 -          try {
    1.29 -            val st = global_state >>> (_.accumulate(state_id, output.message))
    1.30 -            delay_commands_changed.invoke(false, List(st.command))
    1.31 -          }
    1.32 -          catch {
    1.33 -            case _: Document.State.Fail => bad_output(output)
    1.34 -          }
    1.35 +          accumulate(state_id, output.message)
    1.36 +
    1.37 +        case Markup.Command_Timing(state_id, timing) if output.is_protocol =>
    1.38 +          // FIXME XML.cache (!?)
    1.39 +          accumulate(state_id, XML.elem(Markup.STATUS, List(XML.Elem(Markup.Timing(timing), Nil))))
    1.40  
    1.41          case Markup.Assign_Execs if output.is_protocol =>
    1.42            XML.content(output.body) match {
    1.43 @@ -324,8 +333,8 @@
    1.44                  val cmds = global_state >>> (_.assign(id, assign))
    1.45                  delay_commands_changed.invoke(true, cmds)
    1.46                }
    1.47 -              catch { case _: Document.State.Fail => bad_output(output) }
    1.48 -            case _ => bad_output(output)
    1.49 +              catch { case _: Document.State.Fail => bad_output() }
    1.50 +            case _ => bad_output()
    1.51            }
    1.52            // FIXME separate timeout event/message!?
    1.53            if (prover.isDefined && System.currentTimeMillis() > prune_next) {
    1.54 @@ -340,8 +349,8 @@
    1.55                try {
    1.56                  global_state >> (_.removed_versions(removed))
    1.57                }
    1.58 -              catch { case _: Document.State.Fail => bad_output(output) }
    1.59 -            case _ => bad_output(output)
    1.60 +              catch { case _: Document.State.Fail => bad_output() }
    1.61 +            case _ => bad_output()
    1.62            }
    1.63  
    1.64          case Markup.Invoke_Scala(name, id) if output.is_protocol =>
    1.65 @@ -374,7 +383,7 @@
    1.66            if (rc == 0) phase = Session.Inactive
    1.67            else phase = Session.Failed
    1.68  
    1.69 -        case _ => bad_output(output)
    1.70 +        case _ => bad_output()
    1.71        }
    1.72      }
    1.73      //}}}