just one Session.raw_messages event bus;
authorwenzelm
Wed Sep 22 14:53:42 2010 +0200 (2010-09-22)
changeset 39588507fcf86e1e0
parent 39587 f84b70e3bb9c
child 39589 5b81b8df1dde
just one Session.raw_messages event bus;
src/Pure/System/session.scala
src/Tools/jEdit/src/jedit/protocol_dockable.scala
src/Tools/jEdit/src/jedit/raw_output_dockable.scala
     1.1 --- a/src/Pure/System/session.scala	Wed Sep 22 14:29:13 2010 +0200
     1.2 +++ b/src/Pure/System/session.scala	Wed Sep 22 14:53:42 2010 +0200
     1.3 @@ -41,8 +41,7 @@
     1.4    /* pervasive event buses */
     1.5  
     1.6    val global_settings = new Event_Bus[Session.Global_Settings.type]
     1.7 -  val raw_protocol = new Event_Bus[Isabelle_Process.Result]
     1.8 -  val raw_output = new Event_Bus[Isabelle_Process.Result]
     1.9 +  val raw_messages = new Event_Bus[Isabelle_Process.Result]
    1.10    val commands_changed = new Event_Bus[Session.Commands_Changed]
    1.11    val perspective = new Event_Bus[Session.Perspective.type]
    1.12    val assignments = new Event_Bus[Session.Assignment.type]
    1.13 @@ -177,7 +176,7 @@
    1.14      def handle_result(result: Isabelle_Process.Result)
    1.15      //{{{
    1.16      {
    1.17 -      raw_protocol.event(result)
    1.18 +      raw_messages.event(result)
    1.19  
    1.20        result.properties match {
    1.21          case Position.Id(state_id) =>
    1.22 @@ -202,8 +201,7 @@
    1.23              }
    1.24            }
    1.25            else if (result.is_exit) prover = null  // FIXME ??
    1.26 -          else if (result.is_stdout) raw_output.event(result)
    1.27 -          else if (!result.is_system) bad_result(result)
    1.28 +          else if (!result.is_system && !result.is_stdout) bad_result(result)
    1.29          }
    1.30      }
    1.31      //}}}
     2.1 --- a/src/Tools/jEdit/src/jedit/protocol_dockable.scala	Wed Sep 22 14:29:13 2010 +0200
     2.2 +++ b/src/Tools/jEdit/src/jedit/protocol_dockable.scala	Wed Sep 22 14:53:42 2010 +0200
     2.3 @@ -34,6 +34,6 @@
     2.4      }
     2.5    }
     2.6  
     2.7 -  override def init() { Isabelle.session.raw_protocol += main_actor }
     2.8 -  override def exit() { Isabelle.session.raw_protocol -= main_actor }
     2.9 +  override def init() { Isabelle.session.raw_messages += main_actor }
    2.10 +  override def exit() { Isabelle.session.raw_messages -= main_actor }
    2.11  }
     3.1 --- a/src/Tools/jEdit/src/jedit/raw_output_dockable.scala	Wed Sep 22 14:29:13 2010 +0200
     3.2 +++ b/src/Tools/jEdit/src/jedit/raw_output_dockable.scala	Wed Sep 22 14:53:42 2010 +0200
     3.3 @@ -29,13 +29,14 @@
     3.4      loop {
     3.5        react {
     3.6          case result: Isabelle_Process.Result =>
     3.7 -          Swing_Thread.now { text_area.append(XML.content(result.message).mkString) }
     3.8 +          if (result.is_stdout)
     3.9 +            Swing_Thread.now { text_area.append(XML.content(result.message).mkString) }
    3.10  
    3.11          case bad => System.err.println("Raw_Output_Dockable: ignoring bad message " + bad)
    3.12        }
    3.13      }
    3.14    }
    3.15  
    3.16 -  override def init() { Isabelle.session.raw_output += main_actor }
    3.17 -  override def exit() { Isabelle.session.raw_output -= main_actor }
    3.18 +  override def init() { Isabelle.session.raw_messages += main_actor }
    3.19 +  override def exit() { Isabelle.session.raw_messages -= main_actor }
    3.20  }