src/Pure/PIDE/session.scala
changeset 56385 76acce58aeab
parent 56335 8953d4cc060a
child 56387 d92eb5c3960d
     1.1 --- a/src/Pure/PIDE/session.scala	Thu Apr 03 10:51:24 2014 +0200
     1.2 +++ b/src/Pure/PIDE/session.scala	Thu Apr 03 13:46:18 2014 +0200
     1.3 @@ -56,12 +56,12 @@
     1.4    abstract class Protocol_Handler
     1.5    {
     1.6      def stop(prover: Prover): Unit = {}
     1.7 -    val functions: Map[String, (Prover, Isabelle_Process.Protocol_Output) => Boolean]
     1.8 +    val functions: Map[String, (Prover, Prover.Protocol_Output) => Boolean]
     1.9    }
    1.10  
    1.11    class Protocol_Handlers(
    1.12      handlers: Map[String, Session.Protocol_Handler] = Map.empty,
    1.13 -    functions: Map[String, Isabelle_Process.Protocol_Output => Boolean] = Map.empty)
    1.14 +    functions: Map[String, Prover.Protocol_Output => Boolean] = Map.empty)
    1.15    {
    1.16      def get(name: String): Option[Protocol_Handler] = handlers.get(name)
    1.17  
    1.18 @@ -81,7 +81,7 @@
    1.19            val new_handler = Class.forName(name).newInstance.asInstanceOf[Protocol_Handler]
    1.20            val new_functions =
    1.21              for ((a, f) <- new_handler.functions.toList) yield
    1.22 -              (a, (msg: Isabelle_Process.Protocol_Output) => f(prover, msg))
    1.23 +              (a, (msg: Prover.Protocol_Output) => f(prover, msg))
    1.24  
    1.25            val dups = for ((a, _) <- new_functions if functions1.isDefinedAt(a)) yield a
    1.26            if (!dups.isEmpty) error("Duplicate protocol functions: " + commas_quote(dups))
    1.27 @@ -98,7 +98,7 @@
    1.28        new Protocol_Handlers(handlers2, functions2)
    1.29      }
    1.30  
    1.31 -    def invoke(msg: Isabelle_Process.Protocol_Output): Boolean =
    1.32 +    def invoke(msg: Prover.Protocol_Output): Boolean =
    1.33        msg.properties match {
    1.34          case Markup.Function(a) if functions.isDefinedAt(a) =>
    1.35            try { functions(a)(msg) }
    1.36 @@ -146,9 +146,9 @@
    1.37    val raw_edits = new Event_Bus[Session.Raw_Edits]
    1.38    val commands_changed = new Event_Bus[Session.Commands_Changed]
    1.39    val phase_changed = new Event_Bus[Session.Phase]
    1.40 -  val syslog_messages = new Event_Bus[Isabelle_Process.Output]
    1.41 -  val raw_output_messages = new Event_Bus[Isabelle_Process.Output]
    1.42 -  val all_messages = new Event_Bus[Isabelle_Process.Message]  // potential bottle-neck
    1.43 +  val syslog_messages = new Event_Bus[Prover.Output]
    1.44 +  val raw_output_messages = new Event_Bus[Prover.Output]
    1.45 +  val all_messages = new Event_Bus[Prover.Message]  // potential bottle-neck
    1.46    val trace_events = new Event_Bus[Simplifier_Trace.Event.type]
    1.47  
    1.48  
    1.49 @@ -261,7 +261,7 @@
    1.50    private case class Start(args: List[String])
    1.51    private case class Cancel_Exec(exec_id: Document_ID.Exec)
    1.52    private case class Protocol_Command(name: String, args: List[String])
    1.53 -  private case class Messages(msgs: List[Isabelle_Process.Message])
    1.54 +  private case class Messages(msgs: List[Prover.Message])
    1.55    private case class Update_Options(options: Options)
    1.56  
    1.57    private val (_, session_actor) = Simple_Thread.actor("session_actor", daemon = true)
    1.58 @@ -275,22 +275,22 @@
    1.59  
    1.60      object receiver
    1.61      {
    1.62 -      private var buffer = new mutable.ListBuffer[Isabelle_Process.Message]
    1.63 +      private var buffer = new mutable.ListBuffer[Prover.Message]
    1.64  
    1.65        private def flush(): Unit = synchronized {
    1.66          if (!buffer.isEmpty) {
    1.67            val msgs = buffer.toList
    1.68            this_actor ! Messages(msgs)
    1.69 -          buffer = new mutable.ListBuffer[Isabelle_Process.Message]
    1.70 +          buffer = new mutable.ListBuffer[Prover.Message]
    1.71          }
    1.72        }
    1.73 -      def invoke(msg: Isabelle_Process.Message): Unit = synchronized {
    1.74 +      def invoke(msg: Prover.Message): Unit = synchronized {
    1.75          msg match {
    1.76 -          case _: Isabelle_Process.Input =>
    1.77 +          case _: Prover.Input =>
    1.78              buffer += msg
    1.79 -          case output: Isabelle_Process.Protocol_Output if output.properties == Markup.Flush =>
    1.80 +          case output: Prover.Protocol_Output if output.properties == Markup.Flush =>
    1.81              flush()
    1.82 -          case output: Isabelle_Process.Output =>
    1.83 +          case output: Prover.Output =>
    1.84              buffer += msg
    1.85              if (output.is_syslog)
    1.86                syslog >> (queue =>
    1.87 @@ -410,7 +410,7 @@
    1.88  
    1.89      /* prover output */
    1.90  
    1.91 -    def handle_output(output: Isabelle_Process.Output)
    1.92 +    def handle_output(output: Prover.Output)
    1.93      //{{{
    1.94      {
    1.95        def bad_output()
    1.96 @@ -431,7 +431,7 @@
    1.97        }
    1.98  
    1.99        output match {
   1.100 -        case msg: Isabelle_Process.Protocol_Output =>
   1.101 +        case msg: Prover.Protocol_Output =>
   1.102            val handled = _protocol_handlers.invoke(msg)
   1.103            if (!handled) {
   1.104              msg.properties match {
   1.105 @@ -541,17 +541,17 @@
   1.106  
   1.107          case Session.Dialog_Result(id, serial, result) if prover.isDefined =>
   1.108            prover.get.dialog_result(serial, result)
   1.109 -          handle_output(new Isabelle_Process.Output(Protocol.Dialog_Result(id, serial, result)))
   1.110 +          handle_output(new Prover.Output(Protocol.Dialog_Result(id, serial, result)))
   1.111  
   1.112          case Protocol_Command(name, args) if prover.isDefined =>
   1.113            prover.get.protocol_command(name, args:_*)
   1.114  
   1.115          case Messages(msgs) =>
   1.116            msgs foreach {
   1.117 -            case input: Isabelle_Process.Input =>
   1.118 +            case input: Prover.Input =>
   1.119                all_messages.event(input)
   1.120  
   1.121 -            case output: Isabelle_Process.Output =>
   1.122 +            case output: Prover.Output =>
   1.123                if (output.is_stdout || output.is_stderr) raw_output_messages.event(output)
   1.124                else handle_output(output)
   1.125                if (output.is_syslog) syslog_messages.event(output)