tuned prover message categorization;
authorwenzelm
Thu Sep 23 14:39:29 2010 +0200 (2010-09-23 ago)
changeset 39625fb0c851e4f9d
parent 39624 57496c868dcc
child 39626 a5d0bcfb95a3
tuned prover message categorization;
src/Pure/PIDE/isar_document.scala
src/Pure/System/isabelle_process.scala
src/Pure/System/session.scala
src/Tools/jEdit/src/jedit/session_dockable.scala
     1.1 --- a/src/Pure/PIDE/isar_document.scala	Thu Sep 23 14:26:55 2010 +0200
     1.2 +++ b/src/Pure/PIDE/isar_document.scala	Thu Sep 23 14:39:29 2010 +0200
     1.3 @@ -72,7 +72,14 @@
     1.4  
     1.5    /* specific messages */
     1.6  
     1.7 -  def is_tracing(msg: XML.Tree): Boolean =
     1.8 +  def is_ready(msg: XML.Tree): Boolean =
     1.9 +    msg match {
    1.10 +      case XML.Elem(Markup(Markup.STATUS, _),
    1.11 +        List(XML.Elem(Markup(Markup.READY, _), _))) => true
    1.12 +      case _ => false
    1.13 +    }
    1.14 +
    1.15 + def is_tracing(msg: XML.Tree): Boolean =
    1.16      msg match {
    1.17        case XML.Elem(Markup(Markup.TRACING, _), _) => true
    1.18        case _ => false
     2.1 --- a/src/Pure/System/isabelle_process.scala	Thu Sep 23 14:26:55 2010 +0200
     2.2 +++ b/src/Pure/System/isabelle_process.scala	Thu Sep 23 14:39:29 2010 +0200
     2.3 @@ -44,11 +44,8 @@
     2.4      def is_system = kind == Markup.SYSTEM
     2.5      def is_status = kind == Markup.STATUS
     2.6      def is_report = kind == Markup.REPORT
     2.7 -    def is_ready = is_status && {
     2.8 -      body match {
     2.9 -        case List(XML.Elem(Markup(Markup.READY, _), _)) => true
    2.10 -        case _ => false
    2.11 -      }}
    2.12 +    def is_ready = Isar_Document.is_ready(message)
    2.13 +    def is_syslog = is_init || is_exit || is_system || is_ready
    2.14  
    2.15      override def toString: String =
    2.16      {
     3.1 --- a/src/Pure/System/session.scala	Thu Sep 23 14:26:55 2010 +0200
     3.2 +++ b/src/Pure/System/session.scala	Thu Sep 23 14:39:29 2010 +0200
     3.3 @@ -187,7 +187,9 @@
     3.4            }
     3.5            catch { case _: Document.State.Fail => bad_result(result) }
     3.6          case _ =>
     3.7 -          if (result.is_status) {
     3.8 +          if (result.is_exit) prover = null  // FIXME ??
     3.9 +          else if (result.is_syslog || result.is_stdout) { }
    3.10 +          else if (result.is_status) {
    3.11              result.body match {
    3.12                case List(Isar_Document.Assign(id, edits)) =>
    3.13                  try {
    3.14 @@ -198,12 +200,10 @@
    3.15                  catch { case _: Document.State.Fail => bad_result(result) }
    3.16                case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
    3.17                case List(Keyword.Keyword_Decl(name)) => syntax += name
    3.18 -              case _ => if (!result.is_ready) bad_result(result)
    3.19 +              case _ => bad_result(result)
    3.20              }
    3.21            }
    3.22 -          else if (result.is_exit) prover = null  // FIXME ??
    3.23 -          else if (!(result.is_init || result.is_exit || result.is_system || result.is_stdout))
    3.24 -            bad_result(result)
    3.25 +          else bad_result(result)
    3.26          }
    3.27      }
    3.28      //}}}
     4.1 --- a/src/Tools/jEdit/src/jedit/session_dockable.scala	Thu Sep 23 14:26:55 2010 +0200
     4.2 +++ b/src/Tools/jEdit/src/jedit/session_dockable.scala	Thu Sep 23 14:39:29 2010 +0200
     4.3 @@ -53,8 +53,10 @@
     4.4      loop {
     4.5        react {
     4.6          case result: Isabelle_Process.Result =>
     4.7 -          if (result.is_init || result.is_exit || result.is_system || result.is_ready)
     4.8 -            Swing_Thread.now { syslog.append(XML.content(result.message).mkString + "\n") }
     4.9 +          if (result.is_syslog)
    4.10 +            Swing_Thread.now {
    4.11 +              syslog.append(XML.content(result.message).mkString + "\n")
    4.12 +            }
    4.13  
    4.14          case bad => System.err.println("Session_Dockable: ignoring bad message " + bad)
    4.15        }