merged
authorwenzelm
Fri Apr 25 14:39:11 2014 +0200 (2014-04-25)
changeset 56721f2ffead641d4
parent 56684 d8f32f55e463
parent 56720 e1317a26f8c0
child 56722 ba1ac087b3a7
merged
src/Pure/Concurrent/volatile.scala
src/Pure/System/event_bus.scala
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Concurrent/consumer_thread.scala	Fri Apr 25 14:39:11 2014 +0200
     1.3 @@ -0,0 +1,84 @@
     1.4 +/*  Title:      Pure/Concurrent/consumer_thread.scala
     1.5 +    Module:     PIDE
     1.6 +    Author:     Makarius
     1.7 +
     1.8 +Consumer thread with unbounded queueing of requests, and optional
     1.9 +acknowledgment.
    1.10 +*/
    1.11 +
    1.12 +package isabelle
    1.13 +
    1.14 +
    1.15 +import scala.annotation.tailrec
    1.16 +
    1.17 +
    1.18 +object Consumer_Thread
    1.19 +{
    1.20 +  def fork[A](name: String = "", daemon: Boolean = false)(
    1.21 +      consume: A => Boolean,
    1.22 +      finish: () => Unit = () => ()): Consumer_Thread[A] =
    1.23 +    new Consumer_Thread[A](name, daemon, consume, finish)
    1.24 +
    1.25 +
    1.26 +  /* internal messages */
    1.27 +
    1.28 +  private type Ack = Synchronized[Option[Exn.Result[Boolean]]]
    1.29 +  private type Request[A] = (A, Option[Ack])
    1.30 +}
    1.31 +
    1.32 +final class Consumer_Thread[A] private(
    1.33 +  name: String, daemon: Boolean, consume: A => Boolean, finish: () => Unit)
    1.34 +{
    1.35 +  private var active = true
    1.36 +  private val mbox = Mailbox[Option[Consumer_Thread.Request[A]]]
    1.37 +
    1.38 +  private val thread = Simple_Thread.fork(name, daemon) { main_loop() }
    1.39 +  def is_active: Boolean = active && thread.isAlive
    1.40 +
    1.41 +  private def failure(exn: Throwable): Unit =
    1.42 +    System.err.println(
    1.43 +      "Consumer thread failure: " + quote(thread.getName) + "\n" + Exn.message(exn))
    1.44 +
    1.45 +  private def robust_finish(): Unit =
    1.46 +    try { finish() } catch { case exn: Throwable => failure(exn) }
    1.47 +
    1.48 +  @tailrec private def main_loop(): Unit =
    1.49 +    mbox.receive match {
    1.50 +      case Some((arg, ack)) =>
    1.51 +        val result = Exn.capture { consume(arg) }
    1.52 +        val continue =
    1.53 +          result match {
    1.54 +            case Exn.Res(cont) => cont
    1.55 +            case Exn.Exn(exn) =>
    1.56 +              if (!ack.isDefined) failure(exn)
    1.57 +              true
    1.58 +          }
    1.59 +        ack.foreach(a => a.change(_ => Some(result)))
    1.60 +        if (continue) main_loop() else robust_finish()
    1.61 +      case None => robust_finish()
    1.62 +    }
    1.63 +
    1.64 +  assert(is_active)
    1.65 +
    1.66 +
    1.67 +  /* main methods */
    1.68 +
    1.69 +  private def request(x: A, ack: Option[Consumer_Thread.Ack])
    1.70 +  {
    1.71 +    synchronized {
    1.72 +      if (is_active) mbox.send(Some((x, ack)))
    1.73 +      else error("Consumer thread not active: " + quote(thread.getName))
    1.74 +    }
    1.75 +    ack.foreach(a =>
    1.76 +      Exn.release(a.guarded_access({ case None => None case res => Some((res.get, res)) })))
    1.77 +  }
    1.78 +
    1.79 +  def send(arg: A) { request(arg, None) }
    1.80 +  def send_wait(arg: A) { request(arg, Some(Synchronized(None))) }
    1.81 +
    1.82 +  def shutdown(): Unit =
    1.83 +  {
    1.84 +    synchronized { if (is_active) { active = false; mbox.send(None) } }
    1.85 +    thread.join
    1.86 +  }
    1.87 +}
     2.1 --- a/src/Pure/Concurrent/counter.scala	Fri Apr 25 12:09:15 2014 +0200
     2.2 +++ b/src/Pure/Concurrent/counter.scala	Fri Apr 25 14:39:11 2014 +0200
     2.3 @@ -25,5 +25,7 @@
     2.4      count -= 1
     2.5      count
     2.6    }
     2.7 +
     2.8 +  override def toString: String = count.toString
     2.9  }
    2.10  
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Pure/Concurrent/mailbox.scala	Fri Apr 25 14:39:11 2014 +0200
     3.3 @@ -0,0 +1,37 @@
     3.4 +/*  Title:      Pure/Concurrent/mailbox.scala
     3.5 +    Module:     PIDE
     3.6 +    Author:     Makarius
     3.7 +
     3.8 +Message exchange via mailbox, with non-blocking send (due to unbounded
     3.9 +queueing) and potentially blocking receive.
    3.10 +*/
    3.11 +
    3.12 +package isabelle
    3.13 +
    3.14 +
    3.15 +import scala.collection.immutable.Queue
    3.16 +
    3.17 +
    3.18 +object Mailbox
    3.19 +{
    3.20 +  def apply[A]: Mailbox[A] = new Mailbox[A]()
    3.21 +}
    3.22 +
    3.23 +
    3.24 +class Mailbox[A] private()
    3.25 +{
    3.26 +  private val mailbox = Synchronized(Queue.empty[A])
    3.27 +  override def toString: String = mailbox.value.mkString("Mailbox(", ",", ")")
    3.28 +
    3.29 +  def send(msg: A): Unit =
    3.30 +    mailbox.change(_.enqueue(msg))
    3.31 +
    3.32 +  def receive: A =
    3.33 +    mailbox.guarded_access(_.dequeueOption)
    3.34 +
    3.35 +  def receive_timeout(timeout: Time): Option[A] =
    3.36 +    mailbox.timed_access(_ => Some(Time.now() + timeout), _.dequeueOption)
    3.37 +
    3.38 +  def await_empty: Unit =
    3.39 +    mailbox.guarded_access(queue => if (queue.isEmpty) Some(((), queue)) else None)
    3.40 +}
     4.1 --- a/src/Pure/Concurrent/simple_thread.scala	Fri Apr 25 12:09:15 2014 +0200
     4.2 +++ b/src/Pure/Concurrent/simple_thread.scala	Fri Apr 25 14:39:11 2014 +0200
     4.3 @@ -10,8 +10,6 @@
     4.4  
     4.5  import java.lang.Thread
     4.6  
     4.7 -import scala.actors.Actor
     4.8 -
     4.9  
    4.10  object Simple_Thread
    4.11  {
    4.12 @@ -42,15 +40,5 @@
    4.13      val thread = fork(name, daemon) { result.fulfill_result(Exn.capture(body)) }
    4.14      (thread, result)
    4.15    }
    4.16 -
    4.17 -
    4.18 -  /* thread as actor */
    4.19 -
    4.20 -  def actor(name: String, daemon: Boolean = false)(body: => Unit): (Thread, Actor) =
    4.21 -  {
    4.22 -    val actor = Future.promise[Actor]
    4.23 -    val thread = fork(name, daemon) { actor.fulfill(Actor.self); body }
    4.24 -    (thread, actor.join)
    4.25 -  }
    4.26  }
    4.27  
     5.1 --- a/src/Pure/Concurrent/synchronized.ML	Fri Apr 25 12:09:15 2014 +0200
     5.2 +++ b/src/Pure/Concurrent/synchronized.ML	Fri Apr 25 14:39:11 2014 +0200
     5.3 @@ -1,7 +1,7 @@
     5.4  (*  Title:      Pure/Concurrent/synchronized.ML
     5.5      Author:     Fabian Immler and Makarius
     5.6  
     5.7 -State variables with synchronized access.
     5.8 +Synchronized variables.
     5.9  *)
    5.10  
    5.11  signature SYNCHRONIZED =
    5.12 @@ -18,7 +18,7 @@
    5.13  structure Synchronized: SYNCHRONIZED =
    5.14  struct
    5.15  
    5.16 -(* state variables *)
    5.17 +(* state variable *)
    5.18  
    5.19  abstype 'a var = Var of
    5.20   {name: string,
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/Pure/Concurrent/synchronized.scala	Fri Apr 25 14:39:11 2014 +0200
     6.3 @@ -0,0 +1,79 @@
     6.4 +/*  Title:      Pure/Concurrent/synchronized.scala
     6.5 +    Module:     PIDE
     6.6 +    Author:     Makarius
     6.7 +
     6.8 +Synchronized variables.
     6.9 +*/
    6.10 +
    6.11 +package isabelle
    6.12 +
    6.13 +
    6.14 +import scala.annotation.tailrec
    6.15 +
    6.16 +
    6.17 +object Synchronized
    6.18 +{
    6.19 +  def apply[A](init: A): Synchronized[A] = new Synchronized(init)
    6.20 +}
    6.21 +
    6.22 +
    6.23 +final class Synchronized[A] private(init: A)
    6.24 +{
    6.25 +  /* state variable */
    6.26 +
    6.27 +  private var state: A = init
    6.28 +
    6.29 +  def value: A = synchronized { state }
    6.30 +  override def toString: String = value.toString
    6.31 +
    6.32 +
    6.33 +  /* synchronized access */
    6.34 +
    6.35 +  def timed_access[B](time_limit: A => Option[Time], f: A => Option[(B, A)]): Option[B] =
    6.36 +    synchronized {
    6.37 +      def check(x: A): Option[B] =
    6.38 +        f(x) match {
    6.39 +          case None => None
    6.40 +          case Some((y, x1)) =>
    6.41 +            state = x1
    6.42 +            notifyAll()
    6.43 +            Some(y)
    6.44 +        }
    6.45 +      @tailrec def try_change(): Option[B] =
    6.46 +      {
    6.47 +        val x = state
    6.48 +        check(x) match {
    6.49 +          case None =>
    6.50 +            time_limit(x) match {
    6.51 +              case Some(t) =>
    6.52 +                val timeout = (t - Time.now()).ms
    6.53 +                if (timeout > 0L) {
    6.54 +                  wait(timeout)
    6.55 +                  check(state)
    6.56 +                }
    6.57 +                else None
    6.58 +              case None =>
    6.59 +                wait()
    6.60 +                try_change()
    6.61 +            }
    6.62 +          case some => some
    6.63 +        }
    6.64 +      }
    6.65 +      try_change()
    6.66 +    }
    6.67 +
    6.68 +  def guarded_access[B](f: A => Option[(B, A)]): B =
    6.69 +    timed_access(_ => None, f).get
    6.70 +
    6.71 +
    6.72 +  /* unconditional change */
    6.73 +
    6.74 +  def change(f: A => A): Unit = synchronized { state = f(state); notifyAll() }
    6.75 +
    6.76 +  def change_result[B](f: A => (B, A)): B = synchronized {
    6.77 +    val (result, new_state) = f(state)
    6.78 +    state = new_state
    6.79 +    notifyAll()
    6.80 +    result
    6.81 +  }
    6.82 +}
     7.1 --- a/src/Pure/Concurrent/volatile.scala	Fri Apr 25 12:09:15 2014 +0200
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,29 +0,0 @@
     7.4 -/*  Title:      Pure/Concurrent/volatile.scala
     7.5 -    Module:     PIDE
     7.6 -    Author:     Makarius
     7.7 -
     7.8 -Volatile variables.
     7.9 -*/
    7.10 -
    7.11 -package isabelle
    7.12 -
    7.13 -
    7.14 -object Volatile
    7.15 -{
    7.16 -  def apply[A](init: A): Volatile[A] = new Volatile(init)
    7.17 -}
    7.18 -
    7.19 -
    7.20 -final class Volatile[A] private(init: A)
    7.21 -{
    7.22 -  @volatile private var state: A = init
    7.23 -  def apply(): A = state
    7.24 -  def >> (f: A => A) { state = f(state) }
    7.25 -  def >>>[B] (f: A => (B, A)): B =
    7.26 -  {
    7.27 -    val (result, new_state) = f(state)
    7.28 -    state = new_state
    7.29 -    result
    7.30 -  }
    7.31 -}
    7.32 -
     8.1 --- a/src/Pure/General/time.scala	Fri Apr 25 12:09:15 2014 +0200
     8.2 +++ b/src/Pure/General/time.scala	Fri Apr 25 14:39:11 2014 +0200
     8.3 @@ -16,6 +16,7 @@
     8.4    def seconds(s: Double): Time = new Time((s * 1000.0).round)
     8.5    def ms(m: Long): Time = new Time(m)
     8.6    val zero: Time = ms(0)
     8.7 +  def now(): Time = ms(System.currentTimeMillis())
     8.8  
     8.9    def print_seconds(s: Double): String =
    8.10      String.format(Locale.ROOT, "%.3f", s.asInstanceOf[AnyRef])
    8.11 @@ -23,12 +24,18 @@
    8.12  
    8.13  final class Time private(val ms: Long) extends AnyVal
    8.14  {
    8.15 -  def + (t: Time): Time = new Time(ms + t.ms)
    8.16 -
    8.17    def seconds: Double = ms / 1000.0
    8.18  
    8.19 -  def min(t: Time): Time = if (ms < t.ms) this else t
    8.20 -  def max(t: Time): Time = if (ms > t.ms) this else t
    8.21 +  def + (t: Time): Time = new Time(ms + t.ms)
    8.22 +  def - (t: Time): Time = new Time(ms - t.ms)
    8.23 +
    8.24 +  def < (t: Time): Boolean = ms < t.ms
    8.25 +  def <= (t: Time): Boolean = ms <= t.ms
    8.26 +  def > (t: Time): Boolean = ms > t.ms
    8.27 +  def >= (t: Time): Boolean = ms >= t.ms
    8.28 +
    8.29 +  def min(t: Time): Time = if (this < t) this else t
    8.30 +  def max(t: Time): Time = if (this > t) this else t
    8.31  
    8.32    def is_zero: Boolean = ms == 0
    8.33    def is_relevant: Boolean = ms >= 1
     9.1 --- a/src/Pure/General/timing.scala	Fri Apr 25 12:09:15 2014 +0200
     9.2 +++ b/src/Pure/General/timing.scala	Fri Apr 25 14:39:11 2014 +0200
     9.3 @@ -14,11 +14,11 @@
     9.4  
     9.5    def timeit[A](message: String, enabled: Boolean = true)(e: => A) =
     9.6      if (enabled) {
     9.7 -      val start = System.currentTimeMillis()
     9.8 +      val start = Time.now()
     9.9        val result = Exn.capture(e)
    9.10 -      val stop = System.currentTimeMillis()
    9.11 +      val stop = Time.now()
    9.12  
    9.13 -      val timing = Time.ms(stop - start)
    9.14 +      val timing = stop - start
    9.15        if (timing.is_relevant)
    9.16          System.err.println(
    9.17            (if (message == null || message.isEmpty) "" else message + ": ") +
    10.1 --- a/src/Pure/PIDE/document.scala	Fri Apr 25 12:09:15 2014 +0200
    10.2 +++ b/src/Pure/PIDE/document.scala	Fri Apr 25 14:39:11 2014 +0200
    10.3 @@ -608,12 +608,12 @@
    10.4      def tip_version: Version = history.tip.version.get_finished
    10.5  
    10.6      def continue_history(
    10.7 -        previous: Future[Version],
    10.8 -        edits: List[Edit_Text],
    10.9 -        version: Future[Version]): (Change, State) =
   10.10 +      previous: Future[Version],
   10.11 +      edits: List[Edit_Text],
   10.12 +      version: Future[Version]): State =
   10.13      {
   10.14        val change = Change.make(previous, edits, version)
   10.15 -      (change, copy(history = history + change))
   10.16 +      copy(history = history + change)
   10.17      }
   10.18  
   10.19      def prune_history(retain: Int = 0): (List[Version], State) =
    11.1 --- a/src/Pure/PIDE/query_operation.scala	Fri Apr 25 12:09:15 2014 +0200
    11.2 +++ b/src/Pure/PIDE/query_operation.scala	Fri Apr 25 14:39:11 2014 +0200
    11.3 @@ -8,9 +8,6 @@
    11.4  package isabelle
    11.5  
    11.6  
    11.7 -import scala.actors.Actor._
    11.8 -
    11.9 -
   11.10  object Query_Operation
   11.11  {
   11.12    object Status extends Enumeration
   11.13 @@ -33,12 +30,12 @@
   11.14  
   11.15    /* implicit state -- owned by Swing thread */
   11.16  
   11.17 -  private var current_location: Option[Command] = None
   11.18 -  private var current_query: List[String] = Nil
   11.19 -  private var current_update_pending = false
   11.20 -  private var current_output: List[XML.Tree] = Nil
   11.21 -  private var current_status = Query_Operation.Status.FINISHED
   11.22 -  private var current_exec_id = Document_ID.none
   11.23 +  @volatile private var current_location: Option[Command] = None
   11.24 +  @volatile private var current_query: List[String] = Nil
   11.25 +  @volatile private var current_update_pending = false
   11.26 +  @volatile private var current_output: List[XML.Tree] = Nil
   11.27 +  @volatile private var current_status = Query_Operation.Status.FINISHED
   11.28 +  @volatile private var current_exec_id = Document_ID.none
   11.29  
   11.30    private def reset_state()
   11.31    {
   11.32 @@ -209,32 +206,27 @@
   11.33    }
   11.34  
   11.35  
   11.36 -  /* main actor */
   11.37 +  /* main */
   11.38  
   11.39 -  private val main_actor = actor {
   11.40 -    loop {
   11.41 -      react {
   11.42 -        case changed: Session.Commands_Changed =>
   11.43 -          current_location match {
   11.44 -            case Some(command)
   11.45 -            if current_update_pending ||
   11.46 -              (current_status != Query_Operation.Status.FINISHED &&
   11.47 -                changed.commands.contains(command)) =>
   11.48 -              Swing_Thread.later { content_update() }
   11.49 -            case _ =>
   11.50 -          }
   11.51 -        case bad =>
   11.52 -          System.err.println("Query_Operation: ignoring bad message " + bad)
   11.53 -      }
   11.54 +  private val main =
   11.55 +    Session.Consumer[Session.Commands_Changed](getClass.getName) {
   11.56 +      case changed =>
   11.57 +        current_location match {
   11.58 +          case Some(command)
   11.59 +          if current_update_pending ||
   11.60 +            (current_status != Query_Operation.Status.FINISHED &&
   11.61 +              changed.commands.contains(command)) =>
   11.62 +            Swing_Thread.later { content_update() }
   11.63 +          case _ =>
   11.64 +        }
   11.65      }
   11.66 -  }
   11.67  
   11.68    def activate() {
   11.69 -    editor.session.commands_changed += main_actor
   11.70 +    editor.session.commands_changed += main
   11.71    }
   11.72  
   11.73    def deactivate() {
   11.74 -    editor.session.commands_changed -= main_actor
   11.75 +    editor.session.commands_changed -= main
   11.76      remove_overlay()
   11.77      reset_state()
   11.78      consume_output(Document.Snapshot.init, Command.Results.empty, Nil)
    12.1 --- a/src/Pure/PIDE/session.scala	Fri Apr 25 12:09:15 2014 +0200
    12.2 +++ b/src/Pure/PIDE/session.scala	Fri Apr 25 14:39:11 2014 +0200
    12.3 @@ -12,12 +12,40 @@
    12.4  
    12.5  import scala.collection.mutable
    12.6  import scala.collection.immutable.Queue
    12.7 -import scala.actors.TIMEOUT
    12.8 -import scala.actors.Actor._
    12.9  
   12.10  
   12.11  object Session
   12.12  {
   12.13 +  /* outlets */
   12.14 +
   12.15 +  object Consumer
   12.16 +  {
   12.17 +    def apply[A](name: String)(consume: A => Unit): Consumer[A] =
   12.18 +      new Consumer[A](name, consume)
   12.19 +  }
   12.20 +  final class Consumer[-A] private(val name: String, val consume: A => Unit)
   12.21 +
   12.22 +  class Outlet[A](dispatcher: Consumer_Thread[() => Unit])
   12.23 +  {
   12.24 +    private val consumers = Synchronized(List.empty[Consumer[A]])
   12.25 +
   12.26 +    def += (c: Consumer[A]) { consumers.change(Library.update(c)) }
   12.27 +    def -= (c: Consumer[A]) { consumers.change(Library.remove(c)) }
   12.28 +
   12.29 +    def post(a: A)
   12.30 +    {
   12.31 +      for (c <- consumers.value.iterator) {
   12.32 +        dispatcher.send(() =>
   12.33 +          try { c.consume(a) }
   12.34 +          catch {
   12.35 +            case exn: Throwable =>
   12.36 +              System.err.println("Consumer failed: " + quote(c.name) + "\n" + Exn.message(exn))
   12.37 +          })
   12.38 +      }
   12.39 +    }
   12.40 +  }
   12.41 +
   12.42 +
   12.43    /* change */
   12.44  
   12.45    sealed case class Change(
   12.46 @@ -136,91 +164,65 @@
   12.47    def reparse_limit: Int = 0
   12.48  
   12.49  
   12.50 -  /* pervasive event buses */
   12.51 +  /* outlets */
   12.52  
   12.53 -  val statistics = new Event_Bus[Session.Statistics]
   12.54 -  val global_options = new Event_Bus[Session.Global_Options]
   12.55 -  val caret_focus = new Event_Bus[Session.Caret_Focus.type]
   12.56 -  val raw_edits = new Event_Bus[Session.Raw_Edits]
   12.57 -  val commands_changed = new Event_Bus[Session.Commands_Changed]
   12.58 -  val phase_changed = new Event_Bus[Session.Phase]
   12.59 -  val syslog_messages = new Event_Bus[Prover.Output]
   12.60 -  val raw_output_messages = new Event_Bus[Prover.Output]
   12.61 -  val all_messages = new Event_Bus[Prover.Message]  // potential bottle-neck
   12.62 -  val trace_events = new Event_Bus[Simplifier_Trace.Event.type]
   12.63 -
   12.64 -
   12.65 -  /** buffered command changes (delay_first discipline) **/
   12.66 +  private val dispatcher =
   12.67 +    Consumer_Thread.fork[() => Unit]("Session.dispatcher", daemon = true) { case e => e(); true }
   12.68  
   12.69 -  //{{{
   12.70 -  private case object Stop
   12.71 +  val statistics = new Session.Outlet[Session.Statistics](dispatcher)
   12.72 +  val global_options = new Session.Outlet[Session.Global_Options](dispatcher)
   12.73 +  val caret_focus = new Session.Outlet[Session.Caret_Focus.type](dispatcher)
   12.74 +  val raw_edits = new Session.Outlet[Session.Raw_Edits](dispatcher)
   12.75 +  val commands_changed = new Session.Outlet[Session.Commands_Changed](dispatcher)
   12.76 +  val phase_changed = new Session.Outlet[Session.Phase](dispatcher)
   12.77 +  val syslog_messages = new Session.Outlet[Prover.Output](dispatcher)
   12.78 +  val raw_output_messages = new Session.Outlet[Prover.Output](dispatcher)
   12.79 +  val all_messages = new Session.Outlet[Prover.Message](dispatcher)  // potential bottle-neck
   12.80 +  val trace_events = new Session.Outlet[Simplifier_Trace.Event.type](dispatcher)
   12.81  
   12.82 -  private val (_, commands_changed_buffer) =
   12.83 -    Simple_Thread.actor("commands_changed_buffer", daemon = true)
   12.84 -  {
   12.85 -    var finished = false
   12.86 -    while (!finished) {
   12.87 -      receive {
   12.88 -        case Stop => finished = true; reply(())
   12.89 -        case changed: Session.Commands_Changed => commands_changed.event(changed)
   12.90 -        case bad => System.err.println("commands_changed_buffer: ignoring bad message " + bad)
   12.91 -      }
   12.92 -    }
   12.93 -  }
   12.94 -  //}}}
   12.95  
   12.96  
   12.97    /** pipelined change parsing **/
   12.98  
   12.99 -  //{{{
  12.100    private case class Text_Edits(
  12.101      previous: Future[Document.Version],
  12.102      doc_blobs: Document.Blobs,
  12.103      text_edits: List[Document.Edit_Text],
  12.104      version_result: Promise[Document.Version])
  12.105  
  12.106 -  private val (_, change_parser) = Simple_Thread.actor("change_parser", daemon = true)
  12.107 +  private val change_parser = Consumer_Thread.fork[Text_Edits]("change_parser", daemon = true)
  12.108    {
  12.109 -    var finished = false
  12.110 -    while (!finished) {
  12.111 -      receive {
  12.112 -        case Stop => finished = true; reply(())
  12.113 -
  12.114 -        case Text_Edits(previous, doc_blobs, text_edits, version_result) =>
  12.115 -          val prev = previous.get_finished
  12.116 -          val change =
  12.117 -            Timing.timeit("parse_change", timing) {
  12.118 -              resources.parse_change(reparse_limit, prev, doc_blobs, text_edits)
  12.119 -            }
  12.120 -          version_result.fulfill(change.version)
  12.121 -          sender ! change
  12.122 -
  12.123 -        case bad => System.err.println("change_parser: ignoring bad message " + bad)
  12.124 -      }
  12.125 -    }
  12.126 +    case Text_Edits(previous, doc_blobs, text_edits, version_result) =>
  12.127 +      val prev = previous.get_finished
  12.128 +      val change =
  12.129 +        Timing.timeit("parse_change", timing) {
  12.130 +          resources.parse_change(reparse_limit, prev, doc_blobs, text_edits)
  12.131 +        }
  12.132 +      version_result.fulfill(change.version)
  12.133 +      manager.send(change)
  12.134 +      true
  12.135    }
  12.136 -  //}}}
  12.137  
  12.138  
  12.139  
  12.140 -  /** main protocol actor **/
  12.141 +  /** main protocol manager **/
  12.142  
  12.143    /* global state */
  12.144  
  12.145 -  private val syslog = Volatile(Queue.empty[XML.Elem])
  12.146 -  def current_syslog(): String = cat_lines(syslog().iterator.map(XML.content))
  12.147 +  private val syslog = Synchronized(Queue.empty[XML.Elem])
  12.148 +  def current_syslog(): String = cat_lines(syslog.value.iterator.map(XML.content))
  12.149  
  12.150    @volatile private var _phase: Session.Phase = Session.Inactive
  12.151    private def phase_=(new_phase: Session.Phase)
  12.152    {
  12.153      _phase = new_phase
  12.154 -    phase_changed.event(new_phase)
  12.155 +    phase_changed.post(new_phase)
  12.156    }
  12.157    def phase = _phase
  12.158    def is_ready: Boolean = phase == Session.Ready
  12.159  
  12.160 -  private val global_state = Volatile(Document.State.init)
  12.161 -  def current_state(): Document.State = global_state()
  12.162 +  private val global_state = Synchronized(Document.State.init)
  12.163 +  def current_state(): Document.State = global_state.value
  12.164  
  12.165    def recent_syntax(): Prover.Syntax =
  12.166    {
  12.167 @@ -230,7 +232,7 @@
  12.168  
  12.169    def snapshot(name: Document.Node.Name = Document.Node.Name.empty,
  12.170        pending_edits: List[Text.Edit] = Nil): Document.Snapshot =
  12.171 -    global_state().snapshot(name, pending_edits)
  12.172 +    global_state.value.snapshot(name, pending_edits)
  12.173  
  12.174  
  12.175    /* protocol handlers */
  12.176 @@ -253,116 +255,130 @@
  12.177    }
  12.178  
  12.179  
  12.180 -  /* actor messages */
  12.181 +  /* internal messages */
  12.182  
  12.183    private case class Start(name: String, args: List[String])
  12.184 +  private case object Stop
  12.185    private case class Cancel_Exec(exec_id: Document_ID.Exec)
  12.186    private case class Protocol_Command(name: String, args: List[String])
  12.187    private case class Messages(msgs: List[Prover.Message])
  12.188    private case class Update_Options(options: Options)
  12.189  
  12.190 -  private val (_, session_actor) = Simple_Thread.actor("session_actor", daemon = true)
  12.191 +
  12.192 +  /* buffered changes */
  12.193 +
  12.194 +  private object change_buffer
  12.195    {
  12.196 -    val this_actor = self
  12.197 +    private var assignment: Boolean = false
  12.198 +    private var nodes: Set[Document.Node.Name] = Set.empty
  12.199 +    private var commands: Set[Command] = Set.empty
  12.200 +
  12.201 +    def flush(): Unit = synchronized {
  12.202 +      if (assignment || !nodes.isEmpty || !commands.isEmpty)
  12.203 +        commands_changed.post(Session.Commands_Changed(assignment, nodes, commands))
  12.204 +      assignment = false
  12.205 +      nodes = Set.empty
  12.206 +      commands = Set.empty
  12.207 +    }
  12.208  
  12.209 -    var prune_next = System.currentTimeMillis() + prune_delay.ms
  12.210 +    def invoke(assign: Boolean, cmds: List[Command]): Unit = synchronized {
  12.211 +      assignment |= assign
  12.212 +      for (command <- cmds) {
  12.213 +        nodes += command.node_name
  12.214 +        commands += command
  12.215 +      }
  12.216 +    }
  12.217 +
  12.218 +    private val timer = new Timer("change_buffer", true)
  12.219 +    timer.schedule(new TimerTask { def run = flush() }, output_delay.ms, output_delay.ms)
  12.220 +
  12.221 +    def shutdown()
  12.222 +    {
  12.223 +      timer.cancel()
  12.224 +      flush()
  12.225 +    }
  12.226 +  }
  12.227  
  12.228  
  12.229 -    /* buffered prover messages */
  12.230 +  /* buffered prover messages */
  12.231 +
  12.232 +  private object receiver
  12.233 +  {
  12.234 +    private var buffer = new mutable.ListBuffer[Prover.Message]
  12.235  
  12.236 -    object receiver
  12.237 -    {
  12.238 -      private var buffer = new mutable.ListBuffer[Prover.Message]
  12.239 +    private def flush(): Unit = synchronized {
  12.240 +      if (!buffer.isEmpty) {
  12.241 +        val msgs = buffer.toList
  12.242 +        manager.send(Messages(msgs))
  12.243 +        buffer = new mutable.ListBuffer[Prover.Message]
  12.244 +      }
  12.245 +    }
  12.246  
  12.247 -      private def flush(): Unit = synchronized {
  12.248 -        if (!buffer.isEmpty) {
  12.249 -          val msgs = buffer.toList
  12.250 -          this_actor ! Messages(msgs)
  12.251 -          buffer = new mutable.ListBuffer[Prover.Message]
  12.252 -        }
  12.253 +    def invoke(msg: Prover.Message): Unit = synchronized {
  12.254 +      msg match {
  12.255 +        case _: Prover.Input =>
  12.256 +          buffer += msg
  12.257 +        case output: Prover.Protocol_Output if output.properties == Markup.Flush =>
  12.258 +          flush()
  12.259 +        case output: Prover.Output =>
  12.260 +          buffer += msg
  12.261 +          if (output.is_syslog)
  12.262 +            syslog.change(queue =>
  12.263 +              {
  12.264 +                val queue1 = queue.enqueue(output.message)
  12.265 +                if (queue1.length > syslog_limit) queue1.dequeue._2 else queue1
  12.266 +              })
  12.267        }
  12.268 -      def invoke(msg: Prover.Message): Unit = synchronized {
  12.269 -        msg match {
  12.270 -          case _: Prover.Input =>
  12.271 -            buffer += msg
  12.272 -          case output: Prover.Protocol_Output if output.properties == Markup.Flush =>
  12.273 -            flush()
  12.274 -          case output: Prover.Output =>
  12.275 -            buffer += msg
  12.276 -            if (output.is_syslog)
  12.277 -              syslog >> (queue =>
  12.278 -                {
  12.279 -                  val queue1 = queue.enqueue(output.message)
  12.280 -                  if (queue1.length > syslog_limit) queue1.dequeue._2 else queue1
  12.281 -                })
  12.282 -        }
  12.283 -      }
  12.284 +    }
  12.285 +
  12.286 +    private val timer = new Timer("receiver", true)
  12.287 +    timer.schedule(new TimerTask { def run = flush }, message_delay.ms, message_delay.ms)
  12.288 +
  12.289 +    def shutdown() { timer.cancel(); flush() }
  12.290 +  }
  12.291 +
  12.292 +
  12.293 +  /* postponed changes */
  12.294 +
  12.295 +  private object postponed_changes
  12.296 +  {
  12.297 +    private var postponed: List[Session.Change] = Nil
  12.298  
  12.299 -      private val timer = new Timer("session_actor.receiver", true)
  12.300 -      timer.schedule(new TimerTask { def run = flush }, message_delay.ms, message_delay.ms)
  12.301 +    def store(change: Session.Change): Unit = synchronized { postponed ::= change }
  12.302  
  12.303 -      def cancel() { timer.cancel() }
  12.304 +    def flush(): Unit = synchronized {
  12.305 +      val state = global_state.value
  12.306 +      val (assigned, unassigned) = postponed.partition(change => state.is_assigned(change.previous))
  12.307 +      postponed = unassigned
  12.308 +      assigned.reverseIterator.foreach(change => manager.send(change))
  12.309      }
  12.310 +  }
  12.311 +
  12.312 +
  12.313 +  /* manager thread */
  12.314 +
  12.315 +  private val manager: Consumer_Thread[Any] =
  12.316 +  {
  12.317 +    var prune_next = Time.now() + prune_delay
  12.318  
  12.319      var prover: Option[Prover] = None
  12.320  
  12.321  
  12.322 -    /* delayed command changes */
  12.323 -
  12.324 -    object delay_commands_changed
  12.325 -    {
  12.326 -      private var changed_assignment: Boolean = false
  12.327 -      private var changed_nodes: Set[Document.Node.Name] = Set.empty
  12.328 -      private var changed_commands: Set[Command] = Set.empty
  12.329 -
  12.330 -      private var flush_time: Option[Long] = None
  12.331 -
  12.332 -      def flush_timeout: Long =
  12.333 -        flush_time match {
  12.334 -          case None => 5000L
  12.335 -          case Some(time) => (time - System.currentTimeMillis()) max 0
  12.336 -        }
  12.337 -
  12.338 -      def flush()
  12.339 -      {
  12.340 -        if (changed_assignment || !changed_nodes.isEmpty || !changed_commands.isEmpty)
  12.341 -          commands_changed_buffer !
  12.342 -            Session.Commands_Changed(changed_assignment, changed_nodes, changed_commands)
  12.343 -        changed_assignment = false
  12.344 -        changed_nodes = Set.empty
  12.345 -        changed_commands = Set.empty
  12.346 -        flush_time = None
  12.347 -      }
  12.348 -
  12.349 -      def invoke(assign: Boolean, commands: List[Command])
  12.350 -      {
  12.351 -        changed_assignment |= assign
  12.352 -        for (command <- commands) {
  12.353 -          changed_nodes += command.node_name
  12.354 -          changed_commands += command
  12.355 -        }
  12.356 -        val now = System.currentTimeMillis()
  12.357 -        flush_time match {
  12.358 -          case None => flush_time = Some(now + output_delay.ms)
  12.359 -          case Some(time) => if (now >= time) flush()
  12.360 -        }
  12.361 -      }
  12.362 -    }
  12.363 -
  12.364 -
  12.365      /* raw edits */
  12.366  
  12.367      def handle_raw_edits(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text])
  12.368      //{{{
  12.369      {
  12.370 +      require(prover.isDefined)
  12.371 +
  12.372        prover.get.discontinue_execution()
  12.373  
  12.374 -      val previous = global_state().history.tip.version
  12.375 +      val previous = global_state.value.history.tip.version
  12.376        val version = Future.promise[Document.Version]
  12.377 -      val change = global_state >>> (_.continue_history(previous, edits, version))
  12.378 +      global_state.change(_.continue_history(previous, edits, version))
  12.379  
  12.380 -      raw_edits.event(Session.Raw_Edits(doc_blobs, edits))
  12.381 -      change_parser ! Text_Edits(previous, doc_blobs, edits, version)
  12.382 +      raw_edits.post(Session.Raw_Edits(doc_blobs, edits))
  12.383 +      change_parser.send(Text_Edits(previous, doc_blobs, edits, version))
  12.384      }
  12.385      //}}}
  12.386  
  12.387 @@ -372,23 +388,25 @@
  12.388      def handle_change(change: Session.Change)
  12.389      //{{{
  12.390      {
  12.391 +      require(prover.isDefined)
  12.392 +
  12.393        def id_command(command: Command)
  12.394        {
  12.395          for {
  12.396            digest <- command.blobs_digests
  12.397 -          if !global_state().defined_blob(digest)
  12.398 +          if !global_state.value.defined_blob(digest)
  12.399          } {
  12.400            change.doc_blobs.get(digest) match {
  12.401              case Some(blob) =>
  12.402 -              global_state >> (_.define_blob(digest))
  12.403 +              global_state.change(_.define_blob(digest))
  12.404                prover.get.define_blob(digest, blob.bytes)
  12.405              case None =>
  12.406                System.err.println("Missing blob for SHA1 digest " + digest)
  12.407            }
  12.408          }
  12.409  
  12.410 -        if (!global_state().defined_command(command.id)) {
  12.411 -          global_state >> (_.define_command(command))
  12.412 +        if (!global_state.value.defined_command(command.id)) {
  12.413 +          global_state.change(_.define_command(command))
  12.414            prover.get.define_command(command)
  12.415          }
  12.416        }
  12.417 @@ -397,8 +415,8 @@
  12.418            edit foreach { case (c1, c2) => c1 foreach id_command; c2 foreach id_command }
  12.419        }
  12.420  
  12.421 -      val assignment = global_state().the_assignment(change.previous).check_finished
  12.422 -      global_state >> (_.define_version(change.version, assignment))
  12.423 +      val assignment = global_state.value.the_assignment(change.previous).check_finished
  12.424 +      global_state.change(_.define_version(change.version, assignment))
  12.425        prover.get.update(change.previous.id, change.version.id, change.doc_edits)
  12.426        resources.commit(change)
  12.427      }
  12.428 @@ -413,14 +431,14 @@
  12.429        def bad_output()
  12.430        {
  12.431          if (verbose)
  12.432 -          System.err.println("Ignoring prover output: " + output.message.toString)
  12.433 +          System.err.println("Ignoring bad prover output: " + output.message.toString)
  12.434        }
  12.435  
  12.436        def accumulate(state_id: Document_ID.Generic, message: XML.Elem)
  12.437        {
  12.438          try {
  12.439 -          val st = global_state >>> (_.accumulate(state_id, message))
  12.440 -          delay_commands_changed.invoke(false, List(st.command))
  12.441 +          val st = global_state.change_result(_.accumulate(state_id, message))
  12.442 +          change_buffer.invoke(false, List(st.command))
  12.443          }
  12.444          catch {
  12.445            case _: Document.State.Fail => bad_output()
  12.446 @@ -432,10 +450,10 @@
  12.447            val handled = _protocol_handlers.invoke(msg)
  12.448            if (!handled) {
  12.449              msg.properties match {
  12.450 -              case Markup.Protocol_Handler(name) =>
  12.451 +              case Markup.Protocol_Handler(name) if prover.isDefined =>
  12.452                  _protocol_handlers = _protocol_handlers.add(prover.get, name)
  12.453  
  12.454 -              case Protocol.Command_Timing(state_id, timing) =>
  12.455 +              case Protocol.Command_Timing(state_id, timing) if prover.isDefined =>
  12.456                  val message = XML.elem(Markup.STATUS, List(XML.Elem(Markup.Timing(timing), Nil)))
  12.457                  accumulate(state_id, prover.get.xml_cache.elem(message))
  12.458  
  12.459 @@ -443,31 +461,32 @@
  12.460                  msg.text match {
  12.461                    case Protocol.Assign_Update(id, update) =>
  12.462                      try {
  12.463 -                      val cmds = global_state >>> (_.assign(id, update))
  12.464 -                      delay_commands_changed.invoke(true, cmds)
  12.465 +                      val cmds = global_state.change_result(_.assign(id, update))
  12.466 +                      change_buffer.invoke(true, cmds)
  12.467                      }
  12.468                      catch { case _: Document.State.Fail => bad_output() }
  12.469 +                    postponed_changes.flush()
  12.470                    case _ => bad_output()
  12.471                  }
  12.472                  // FIXME separate timeout event/message!?
  12.473 -                if (prover.isDefined && System.currentTimeMillis() > prune_next) {
  12.474 -                  val old_versions = global_state >>> (_.prune_history(prune_size))
  12.475 +                if (prover.isDefined && Time.now() > prune_next) {
  12.476 +                  val old_versions = global_state.change_result(_.prune_history(prune_size))
  12.477                    if (!old_versions.isEmpty) prover.get.remove_versions(old_versions)
  12.478 -                  prune_next = System.currentTimeMillis() + prune_delay.ms
  12.479 +                  prune_next = Time.now() + prune_delay
  12.480                  }
  12.481  
  12.482                case Markup.Removed_Versions =>
  12.483                  msg.text match {
  12.484                    case Protocol.Removed(removed) =>
  12.485                      try {
  12.486 -                      global_state >> (_.removed_versions(removed))
  12.487 +                      global_state.change(_.removed_versions(removed))
  12.488                      }
  12.489                      catch { case _: Document.State.Fail => bad_output() }
  12.490                    case _ => bad_output()
  12.491                  }
  12.492  
  12.493                case Markup.ML_Statistics(props) =>
  12.494 -                statistics.event(Session.Statistics(props))
  12.495 +                statistics.post(Session.Statistics(props))
  12.496  
  12.497                case Markup.Task_Statistics(props) =>
  12.498                  // FIXME
  12.499 @@ -484,114 +503,108 @@
  12.500                phase = Session.Ready
  12.501  
  12.502              case Markup.Return_Code(rc) if output.is_exit =>
  12.503 +              prover = None
  12.504                if (rc == 0) phase = Session.Inactive
  12.505                else phase = Session.Failed
  12.506  
  12.507 -            case _ => raw_output_messages.event(output)
  12.508 +            case _ => raw_output_messages.post(output)
  12.509            }
  12.510          }
  12.511      }
  12.512      //}}}
  12.513  
  12.514  
  12.515 -    /* main loop */
  12.516 +    /* main thread */
  12.517  
  12.518 -    //{{{
  12.519 -    var finished = false
  12.520 -    while (!finished) {
  12.521 -      receiveWithin(delay_commands_changed.flush_timeout) {
  12.522 -        case TIMEOUT => delay_commands_changed.flush()
  12.523 -
  12.524 -        case Start(name, args) if prover.isEmpty =>
  12.525 -          if (phase == Session.Inactive || phase == Session.Failed) {
  12.526 -            phase = Session.Startup
  12.527 -            prover = Some(resources.start_prover(receiver.invoke _, name, args))
  12.528 -          }
  12.529 +    Consumer_Thread.fork[Any]("Session.manager", daemon = true)
  12.530 +    {
  12.531 +      case arg: Any =>
  12.532 +        //{{{
  12.533 +        arg match {
  12.534 +          case Start(name, args) if prover.isEmpty =>
  12.535 +            if (phase == Session.Inactive || phase == Session.Failed) {
  12.536 +              phase = Session.Startup
  12.537 +              prover = Some(resources.start_prover(receiver.invoke _, name, args))
  12.538 +            }
  12.539  
  12.540 -        case Stop =>
  12.541 -          if (phase == Session.Ready) {
  12.542 -            _protocol_handlers = _protocol_handlers.stop(prover.get)
  12.543 -            global_state >> (_ => Document.State.init)  // FIXME event bus!?
  12.544 -            phase = Session.Shutdown
  12.545 -            prover.get.terminate
  12.546 -            prover = None
  12.547 -            phase = Session.Inactive
  12.548 -          }
  12.549 -          finished = true
  12.550 -          receiver.cancel()
  12.551 -          reply(())
  12.552 +          case Stop =>
  12.553 +            if (prover.isDefined && is_ready) {
  12.554 +              _protocol_handlers = _protocol_handlers.stop(prover.get)
  12.555 +              global_state.change(_ => Document.State.init)  // FIXME event bus!?
  12.556 +              phase = Session.Shutdown
  12.557 +              prover.get.terminate
  12.558 +            }
  12.559  
  12.560 -        case Update_Options(options) =>
  12.561 -          if (prover.isDefined && is_ready) {
  12.562 -            prover.get.options(options)
  12.563 -            handle_raw_edits(Document.Blobs.empty, Nil)
  12.564 -          }
  12.565 -          global_options.event(Session.Global_Options(options))
  12.566 -          reply(())
  12.567 +          case Update_Options(options) =>
  12.568 +            if (prover.isDefined && is_ready) {
  12.569 +              prover.get.options(options)
  12.570 +              handle_raw_edits(Document.Blobs.empty, Nil)
  12.571 +            }
  12.572 +            global_options.post(Session.Global_Options(options))
  12.573 +
  12.574 +          case Cancel_Exec(exec_id) if prover.isDefined =>
  12.575 +            prover.get.cancel_exec(exec_id)
  12.576  
  12.577 -        case Cancel_Exec(exec_id) if prover.isDefined =>
  12.578 -          prover.get.cancel_exec(exec_id)
  12.579 +          case Session.Raw_Edits(doc_blobs, edits) if prover.isDefined =>
  12.580 +            handle_raw_edits(doc_blobs, edits)
  12.581  
  12.582 -        case Session.Raw_Edits(doc_blobs, edits) if prover.isDefined =>
  12.583 -          handle_raw_edits(doc_blobs, edits)
  12.584 -          reply(())
  12.585 +          case Session.Dialog_Result(id, serial, result) if prover.isDefined =>
  12.586 +            prover.get.dialog_result(serial, result)
  12.587 +            handle_output(new Prover.Output(Protocol.Dialog_Result(id, serial, result)))
  12.588  
  12.589 -        case Session.Dialog_Result(id, serial, result) if prover.isDefined =>
  12.590 -          prover.get.dialog_result(serial, result)
  12.591 -          handle_output(new Prover.Output(Protocol.Dialog_Result(id, serial, result)))
  12.592 +          case Protocol_Command(name, args) if prover.isDefined =>
  12.593 +            prover.get.protocol_command(name, args:_*)
  12.594  
  12.595 -        case Protocol_Command(name, args) if prover.isDefined =>
  12.596 -          prover.get.protocol_command(name, args:_*)
  12.597 +          case Messages(msgs) =>
  12.598 +            msgs foreach {
  12.599 +              case input: Prover.Input =>
  12.600 +                all_messages.post(input)
  12.601  
  12.602 -        case Messages(msgs) =>
  12.603 -          msgs foreach {
  12.604 -            case input: Prover.Input =>
  12.605 -              all_messages.event(input)
  12.606 +              case output: Prover.Output =>
  12.607 +                if (output.is_stdout || output.is_stderr) raw_output_messages.post(output)
  12.608 +                else handle_output(output)
  12.609 +                if (output.is_syslog) syslog_messages.post(output)
  12.610 +                all_messages.post(output)
  12.611 +            }
  12.612  
  12.613 -            case output: Prover.Output =>
  12.614 -              if (output.is_stdout || output.is_stderr) raw_output_messages.event(output)
  12.615 -              else handle_output(output)
  12.616 -              if (output.is_syslog) syslog_messages.event(output)
  12.617 -              all_messages.event(output)
  12.618 -          }
  12.619 -
  12.620 -        case change: Session.Change
  12.621 -        if prover.isDefined && global_state().is_assigned(change.previous) =>
  12.622 -          handle_change(change)
  12.623 -
  12.624 -        case bad if !bad.isInstanceOf[Session.Change] =>
  12.625 -          System.err.println("session_actor: ignoring bad message " + bad)
  12.626 -      }
  12.627 +          case change: Session.Change if prover.isDefined =>
  12.628 +            if (global_state.value.is_assigned(change.previous))
  12.629 +              handle_change(change)
  12.630 +            else postponed_changes.store(change)
  12.631 +        }
  12.632 +        true
  12.633 +        //}}}
  12.634      }
  12.635 -    //}}}
  12.636    }
  12.637  
  12.638  
  12.639    /* actions */
  12.640  
  12.641    def start(name: String, args: List[String])
  12.642 -  {
  12.643 -    session_actor ! Start(name, args)
  12.644 -  }
  12.645 +  { manager.send(Start(name, args)) }
  12.646  
  12.647    def stop()
  12.648    {
  12.649 -    commands_changed_buffer !? Stop
  12.650 -    change_parser !? Stop
  12.651 -    session_actor !? Stop
  12.652 +    manager.send_wait(Stop)
  12.653 +    receiver.shutdown()
  12.654 +    change_parser.shutdown()
  12.655 +    change_buffer.shutdown()
  12.656 +    manager.shutdown()
  12.657 +    dispatcher.shutdown()
  12.658    }
  12.659  
  12.660    def protocol_command(name: String, args: String*)
  12.661 -  { session_actor ! Protocol_Command(name, args.toList) }
  12.662 +  { manager.send(Protocol_Command(name, args.toList)) }
  12.663  
  12.664 -  def cancel_exec(exec_id: Document_ID.Exec) { session_actor ! Cancel_Exec(exec_id) }
  12.665 +  def cancel_exec(exec_id: Document_ID.Exec)
  12.666 +  { manager.send(Cancel_Exec(exec_id)) }
  12.667  
  12.668    def update(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text])
  12.669 -  { if (!edits.isEmpty) session_actor !? Session.Raw_Edits(doc_blobs, edits) }
  12.670 +  { if (!edits.isEmpty) manager.send_wait(Session.Raw_Edits(doc_blobs, edits)) }
  12.671  
  12.672    def update_options(options: Options)
  12.673 -  { session_actor !? Update_Options(options) }
  12.674 +  { manager.send_wait(Update_Options(options)) }
  12.675  
  12.676    def dialog_result(id: Document_ID.Generic, serial: Long, result: String)
  12.677 -  { session_actor ! Session.Dialog_Result(id, serial, result) }
  12.678 +  { manager.send(Session.Dialog_Result(id, serial, result)) }
  12.679  }
    13.1 --- a/src/Pure/System/event_bus.scala	Fri Apr 25 12:09:15 2014 +0200
    13.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.3 @@ -1,37 +0,0 @@
    13.4 -/*  Title:      Pure/System/event_bus.scala
    13.5 -    Module:     PIDE
    13.6 -    Author:     Makarius
    13.7 -
    13.8 -Generic event bus with multiple receiving actors.
    13.9 -*/
   13.10 -
   13.11 -package isabelle
   13.12 -
   13.13 -
   13.14 -import scala.actors.Actor, Actor._
   13.15 -import scala.collection.mutable.ListBuffer
   13.16 -
   13.17 -
   13.18 -class Event_Bus[Event]
   13.19 -{
   13.20 -  /* receivers */
   13.21 -
   13.22 -  private val receivers = new ListBuffer[Actor]
   13.23 -
   13.24 -  def += (r: Actor) { synchronized { receivers += r } }
   13.25 -  def + (r: Actor): Event_Bus[Event] = { this += r; this }
   13.26 -
   13.27 -  def += (f: Event => Unit) {
   13.28 -    this += actor { loop { react { case x => f(x.asInstanceOf[Event]) } } }
   13.29 -  }
   13.30 -
   13.31 -  def + (f: Event => Unit): Event_Bus[Event] = { this += f; this }
   13.32 -
   13.33 -  def -= (r: Actor) { synchronized { receivers -= r } }
   13.34 -  def - (r: Actor) = { this -= r; this }
   13.35 -
   13.36 -
   13.37 -  /* event invocation */
   13.38 -
   13.39 -  def event(x: Event) { synchronized { receivers.foreach(_ ! x) } }
   13.40 -}
    14.1 --- a/src/Pure/System/isabelle_process.scala	Fri Apr 25 12:09:15 2014 +0200
    14.2 +++ b/src/Pure/System/isabelle_process.scala	Fri Apr 25 14:39:11 2014 +0200
    14.3 @@ -8,12 +8,7 @@
    14.4  package isabelle
    14.5  
    14.6  
    14.7 -import java.util.concurrent.LinkedBlockingQueue
    14.8 -import java.io.{BufferedReader, BufferedWriter, InputStreamReader, OutputStreamWriter,
    14.9 -  InputStream, OutputStream, BufferedOutputStream, IOException}
   14.10 -
   14.11 -import scala.actors.Actor
   14.12 -import Actor._
   14.13 +import java.io.{InputStream, OutputStream, BufferedOutputStream, IOException}
   14.14  
   14.15  
   14.16  class Isabelle_Process(
   14.17 @@ -55,22 +50,6 @@
   14.18    }
   14.19  
   14.20  
   14.21 -  /* command input actor */
   14.22 -
   14.23 -  private case class Input_Chunks(chunks: List[Bytes])
   14.24 -
   14.25 -  private case object Close
   14.26 -  private def close(p: (Thread, Actor))
   14.27 -  {
   14.28 -    if (p != null && p._1.isAlive) {
   14.29 -      p._2 ! Close
   14.30 -      p._1.join
   14.31 -    }
   14.32 -  }
   14.33 -
   14.34 -  @volatile private var command_input: (Thread, Actor) = null
   14.35 -
   14.36 -
   14.37  
   14.38    /** process manager **/
   14.39  
   14.40 @@ -126,16 +105,15 @@
   14.41      else {
   14.42        val (command_stream, message_stream) = system_channel.rendezvous()
   14.43  
   14.44 -      val stdout = physical_output_actor(false)
   14.45 -      val stderr = physical_output_actor(true)
   14.46 -      command_input = input_actor(command_stream)
   14.47 -      val message = message_actor(message_stream)
   14.48 +      command_input_init(command_stream)
   14.49 +      val stdout = physical_output(false)
   14.50 +      val stderr = physical_output(true)
   14.51 +      val message = message_output(message_stream)
   14.52  
   14.53        val rc = process_result.join
   14.54        system_output("process terminated")
   14.55 -      close(command_input)
   14.56 -      for ((thread, _) <- List(stdout, stderr, command_input, message))
   14.57 -        thread.join
   14.58 +      command_input_close()
   14.59 +      for (thread <- List(stdout, stderr, message)) thread.join
   14.60        system_output("process_manager terminated")
   14.61        exit_message(rc)
   14.62      }
   14.63 @@ -155,24 +133,54 @@
   14.64  
   14.65    def terminate()
   14.66    {
   14.67 -    close(command_input)
   14.68 +    command_input_close()
   14.69      system_output("Terminating Isabelle process")
   14.70      terminate_process()
   14.71    }
   14.72  
   14.73  
   14.74  
   14.75 -  /** stream actors **/
   14.76 +  /** process streams **/
   14.77 +
   14.78 +  /* command input */
   14.79 +
   14.80 +  private var command_input: Option[Consumer_Thread[List[Bytes]]] = None
   14.81 +
   14.82 +  private def command_input_close(): Unit = command_input.foreach(_.shutdown)
   14.83 +
   14.84 +  private def command_input_init(raw_stream: OutputStream)
   14.85 +  {
   14.86 +    val name = "command_input"
   14.87 +    val stream = new BufferedOutputStream(raw_stream)
   14.88 +    command_input =
   14.89 +      Some(
   14.90 +        Consumer_Thread.fork(name)(
   14.91 +          consume =
   14.92 +            {
   14.93 +              case chunks =>
   14.94 +                try {
   14.95 +                  Bytes(chunks.map(_.length).mkString("", ",", "\n")).write(stream)
   14.96 +                  chunks.foreach(_.write(stream))
   14.97 +                  stream.flush
   14.98 +                  true
   14.99 +                }
  14.100 +                catch { case e: IOException => system_output(name + ": " + e.getMessage); false }
  14.101 +            },
  14.102 +          finish = { case () => stream.close; system_output(name + " terminated") }
  14.103 +        )
  14.104 +      )
  14.105 +  }
  14.106 +
  14.107  
  14.108    /* physical output */
  14.109  
  14.110 -  private def physical_output_actor(err: Boolean): (Thread, Actor) =
  14.111 +  private def physical_output(err: Boolean): Thread =
  14.112    {
  14.113      val (name, reader, markup) =
  14.114        if (err) ("standard_error", process.stderr, Markup.STDERR)
  14.115        else ("standard_output", process.stdout, Markup.STDOUT)
  14.116  
  14.117 -    Simple_Thread.actor(name) {
  14.118 +    Simple_Thread.fork(name) {
  14.119        try {
  14.120          var result = new StringBuilder(100)
  14.121          var finished = false
  14.122 @@ -202,45 +210,15 @@
  14.123    }
  14.124  
  14.125  
  14.126 -  /* command input */
  14.127 -
  14.128 -  private def input_actor(raw_stream: OutputStream): (Thread, Actor) =
  14.129 -  {
  14.130 -    val name = "command_input"
  14.131 -    Simple_Thread.actor(name) {
  14.132 -      try {
  14.133 -        val stream = new BufferedOutputStream(raw_stream)
  14.134 -        var finished = false
  14.135 -        while (!finished) {
  14.136 -          //{{{
  14.137 -          receive {
  14.138 -            case Input_Chunks(chunks) =>
  14.139 -              Bytes(chunks.map(_.length).mkString("", ",", "\n")).write(stream)
  14.140 -              chunks.foreach(_.write(stream))
  14.141 -              stream.flush
  14.142 -            case Close =>
  14.143 -              stream.close
  14.144 -              finished = true
  14.145 -            case bad => System.err.println(name + ": ignoring bad message " + bad)
  14.146 -          }
  14.147 -          //}}}
  14.148 -        }
  14.149 -      }
  14.150 -      catch { case e: IOException => system_output(name + ": " + e.getMessage) }
  14.151 -      system_output(name + " terminated")
  14.152 -    }
  14.153 -  }
  14.154 -
  14.155 -
  14.156    /* message output */
  14.157  
  14.158 -  private def message_actor(stream: InputStream): (Thread, Actor) =
  14.159 +  private def message_output(stream: InputStream): Thread =
  14.160    {
  14.161      class EOF extends Exception
  14.162      class Protocol_Error(msg: String) extends Exception(msg)
  14.163  
  14.164      val name = "message_output"
  14.165 -    Simple_Thread.actor(name) {
  14.166 +    Simple_Thread.fork(name) {
  14.167        val default_buffer = new Array[Byte](65536)
  14.168        var c = -1
  14.169  
  14.170 @@ -328,7 +306,10 @@
  14.171    /** protocol commands **/
  14.172  
  14.173    def protocol_command_bytes(name: String, args: Bytes*): Unit =
  14.174 -    command_input._2 ! Input_Chunks(Bytes(name) :: args.toList)
  14.175 +    command_input match {
  14.176 +      case Some(thread) => thread.send(Bytes(name) :: args.toList)
  14.177 +      case None => error("Uninitialized command input thread")
  14.178 +    }
  14.179  
  14.180    def protocol_command(name: String, args: String*)
  14.181    {
    15.1 --- a/src/Pure/Tools/simplifier_trace.scala	Fri Apr 25 12:09:15 2014 +0200
    15.2 +++ b/src/Pure/Tools/simplifier_trace.scala	Fri Apr 25 14:39:11 2014 +0200
    15.3 @@ -7,7 +7,6 @@
    15.4  package isabelle
    15.5  
    15.6  
    15.7 -import scala.actors.Actor._
    15.8  import scala.annotation.tailrec
    15.9  import scala.collection.immutable.SortedMap
   15.10  
   15.11 @@ -102,23 +101,21 @@
   15.12    case object Event
   15.13  
   15.14  
   15.15 -  /* manager actor */
   15.16 +  /* manager thread */
   15.17  
   15.18 -  private case class Handle_Results(session: Session, id: Document_ID.Command, results: Command.Results)
   15.19 -  private case class Generate_Trace(results: Command.Results)
   15.20 +  private case class Handle_Results(
   15.21 +    session: Session, id: Document_ID.Command, results: Command.Results, slot: Promise[Context])
   15.22 +  private case class Generate_Trace(results: Command.Results, slot: Promise[Trace])
   15.23    private case class Cancel(serial: Long)
   15.24    private object Clear_Memory
   15.25 -  private object Stop
   15.26    case class Reply(session: Session, serial: Long, answer: Answer)
   15.27  
   15.28    case class Question(data: Item.Data, answers: List[Answer], default_answer: Answer)
   15.29  
   15.30    case class Context(
   15.31      last_serial: Long = 0L,
   15.32 -    questions: SortedMap[Long, Question] = SortedMap.empty
   15.33 -  )
   15.34 +    questions: SortedMap[Long, Question] = SortedMap.empty)
   15.35    {
   15.36 -
   15.37      def +(q: Question): Context =
   15.38        copy(questions = questions + ((q.data.serial, q)))
   15.39  
   15.40 @@ -127,7 +124,6 @@
   15.41  
   15.42      def with_serial(s: Long): Context =
   15.43        copy(last_serial = Math.max(last_serial, s))
   15.44 -
   15.45    }
   15.46  
   15.47    case class Trace(entries: List[Item.Data])
   15.48 @@ -141,18 +137,27 @@
   15.49    }
   15.50  
   15.51    def handle_results(session: Session, id: Document_ID.Command, results: Command.Results): Context =
   15.52 -    (manager !? Handle_Results(session, id, results)).asInstanceOf[Context]
   15.53 +  {
   15.54 +    val slot = Future.promise[Context]
   15.55 +    manager.send(Handle_Results(session, id, results, slot))
   15.56 +    slot.join
   15.57 +  }
   15.58  
   15.59    def generate_trace(results: Command.Results): Trace =
   15.60 -    (manager !? Generate_Trace(results)).asInstanceOf[Trace]
   15.61 +  {
   15.62 +    val slot = Future.promise[Trace]
   15.63 +    manager.send(Generate_Trace(results, slot))
   15.64 +    slot.join
   15.65 +  }
   15.66  
   15.67    def clear_memory() =
   15.68 -    manager ! Clear_Memory
   15.69 +    manager.send(Clear_Memory)
   15.70  
   15.71    def send_reply(session: Session, serial: Long, answer: Answer) =
   15.72 -    manager ! Reply(session, serial, answer)
   15.73 +    manager.send(Reply(session, serial, answer))
   15.74  
   15.75 -  private val manager = actor {
   15.76 +  private lazy val manager: Consumer_Thread[Any] =
   15.77 +  {
   15.78      var contexts = Map.empty[Document_ID.Command, Context]
   15.79  
   15.80      var memory_children = Map.empty[Long, Set[Long]]
   15.81 @@ -175,124 +180,125 @@
   15.82  
   15.83      def do_reply(session: Session, serial: Long, answer: Answer)
   15.84      {
   15.85 -      session.protocol_command("Simplifier_Trace.reply", Properties.Value.Long(serial), answer.name)
   15.86 +      session.protocol_command(
   15.87 +        "Simplifier_Trace.reply", Properties.Value.Long(serial), answer.name)
   15.88      }
   15.89  
   15.90 -    loop {
   15.91 -      react {
   15.92 -        case Handle_Results(session, id, results) =>
   15.93 -          var new_context = contexts.getOrElse(id, Context())
   15.94 -          var new_serial = new_context.last_serial
   15.95 +    Consumer_Thread.fork[Any]("Simplifier_Trace.manager", daemon = true)(
   15.96 +      consume = (arg: Any) =>
   15.97 +      {
   15.98 +        arg match {
   15.99 +          case Handle_Results(session, id, results, slot) =>
  15.100 +            var new_context = contexts.getOrElse(id, Context())
  15.101 +            var new_serial = new_context.last_serial
  15.102  
  15.103 -          for ((serial, result) <- results.iterator if serial > new_context.last_serial)
  15.104 -          {
  15.105 -            result match {
  15.106 -              case Item(markup, data) =>
  15.107 -                memory_children += (data.parent -> (memory_children.getOrElse(data.parent, Set.empty) + serial))
  15.108 -
  15.109 -                markup match {
  15.110 +            for ((serial, result) <- results.iterator if serial > new_context.last_serial)
  15.111 +            {
  15.112 +              result match {
  15.113 +                case Item(markup, data) =>
  15.114 +                  memory_children +=
  15.115 +                    (data.parent -> (memory_children.getOrElse(data.parent, Set.empty) + serial))
  15.116  
  15.117 -                  case Markup.SIMP_TRACE_STEP =>
  15.118 -                    val index = Index.of_data(data)
  15.119 -                    memory.get(index) match {
  15.120 -                      case Some(answer) if data.memory =>
  15.121 -                        do_reply(session, serial, answer)
  15.122 -                      case _ =>
  15.123 -                        new_context += Question(data, Answer.step.all, Answer.step.default)
  15.124 -                    }
  15.125 +                  markup match {
  15.126  
  15.127 -                  case Markup.SIMP_TRACE_HINT =>
  15.128 -                    data.props match {
  15.129 -                      case Success(false) =>
  15.130 -                        results.get(data.parent) match {
  15.131 -                          case Some(Item(Markup.SIMP_TRACE_STEP, _)) =>
  15.132 -                            new_context += Question(data, Answer.hint_fail.all, Answer.hint_fail.default)
  15.133 -                          case _ =>
  15.134 -                            // unknown, better send a default reply
  15.135 -                            do_reply(session, data.serial, Answer.hint_fail.default)
  15.136 -                        }
  15.137 -                      case _ =>
  15.138 -                    }
  15.139 +                    case Markup.SIMP_TRACE_STEP =>
  15.140 +                      val index = Index.of_data(data)
  15.141 +                      memory.get(index) match {
  15.142 +                        case Some(answer) if data.memory =>
  15.143 +                          do_reply(session, serial, answer)
  15.144 +                        case _ =>
  15.145 +                          new_context += Question(data, Answer.step.all, Answer.step.default)
  15.146 +                      }
  15.147  
  15.148 -                  case Markup.SIMP_TRACE_IGNORE =>
  15.149 -                    // At this point, we know that the parent of this 'IGNORE' entry is a 'STEP'
  15.150 -                    // entry, and that that 'STEP' entry is about to be replayed. Hence, we need
  15.151 -                    // to selectively purge the replies which have been memorized, going down from
  15.152 -                    // the parent to all leaves.
  15.153 -
  15.154 -                    @tailrec
  15.155 -                    def purge(queue: Vector[Long]): Unit =
  15.156 -                      queue match {
  15.157 -                        case s +: rest =>
  15.158 -                          for (Item(Markup.SIMP_TRACE_STEP, data) <- results.get(s))
  15.159 -                            memory -= Index.of_data(data)
  15.160 -                          val children = memory_children.getOrElse(s, Set.empty)
  15.161 -                          memory_children -= s
  15.162 -                          purge(rest ++ children.toVector)
  15.163 +                    case Markup.SIMP_TRACE_HINT =>
  15.164 +                      data.props match {
  15.165 +                        case Success(false) =>
  15.166 +                          results.get(data.parent) match {
  15.167 +                            case Some(Item(Markup.SIMP_TRACE_STEP, _)) =>
  15.168 +                              new_context +=
  15.169 +                                Question(data, Answer.hint_fail.all, Answer.hint_fail.default)
  15.170 +                            case _ =>
  15.171 +                              // unknown, better send a default reply
  15.172 +                              do_reply(session, data.serial, Answer.hint_fail.default)
  15.173 +                          }
  15.174                          case _ =>
  15.175                        }
  15.176  
  15.177 -                    purge(Vector(data.parent))
  15.178 +                    case Markup.SIMP_TRACE_IGNORE =>
  15.179 +                      // At this point, we know that the parent of this 'IGNORE' entry is a 'STEP'
  15.180 +                      // entry, and that that 'STEP' entry is about to be replayed. Hence, we need
  15.181 +                      // to selectively purge the replies which have been memorized, going down from
  15.182 +                      // the parent to all leaves.
  15.183  
  15.184 -                  case _ =>
  15.185 -                }
  15.186 +                      @tailrec
  15.187 +                      def purge(queue: Vector[Long]): Unit =
  15.188 +                        queue match {
  15.189 +                          case s +: rest =>
  15.190 +                            for (Item(Markup.SIMP_TRACE_STEP, data) <- results.get(s))
  15.191 +                              memory -= Index.of_data(data)
  15.192 +                            val children = memory_children.getOrElse(s, Set.empty)
  15.193 +                            memory_children -= s
  15.194 +                            purge(rest ++ children.toVector)
  15.195 +                          case _ =>
  15.196 +                        }
  15.197  
  15.198 -              case _ =>
  15.199 +                      purge(Vector(data.parent))
  15.200 +
  15.201 +                    case _ =>
  15.202 +                  }
  15.203 +
  15.204 +                case _ =>
  15.205 +              }
  15.206 +
  15.207 +              new_serial = serial
  15.208              }
  15.209  
  15.210 -            new_serial = serial
  15.211 -          }
  15.212 +            new_context = new_context.with_serial(new_serial)
  15.213 +            contexts += (id -> new_context)
  15.214 +            slot.fulfill(new_context)
  15.215  
  15.216 -          new_context = new_context.with_serial(new_serial)
  15.217 -          contexts += (id -> new_context)
  15.218 -          reply(new_context)
  15.219 -
  15.220 -        case Generate_Trace(results) =>
  15.221 -          // Since there are potentially lots of trace messages, we do not cache them here again.
  15.222 -          // Instead, everytime the trace is being requested, we re-assemble it based on the
  15.223 -          // current results.
  15.224 +          case Generate_Trace(results, slot) =>
  15.225 +            // Since there are potentially lots of trace messages, we do not cache them here again.
  15.226 +            // Instead, everytime the trace is being requested, we re-assemble it based on the
  15.227 +            // current results.
  15.228  
  15.229 -          val items =
  15.230 -            (for { (_, Item(_, data)) <- results.iterator }
  15.231 -              yield data).toList
  15.232 +            val items =
  15.233 +              (for { (_, Item(_, data)) <- results.iterator }
  15.234 +                yield data).toList
  15.235  
  15.236 -          reply(Trace(items))
  15.237 +            slot.fulfill(Trace(items))
  15.238  
  15.239 -        case Cancel(serial) =>
  15.240 -          find_question(serial) match {
  15.241 -            case Some((id, _)) =>
  15.242 -              do_cancel(serial, id)
  15.243 -            case None =>
  15.244 -          }
  15.245 +          case Cancel(serial) =>
  15.246 +            find_question(serial) match {
  15.247 +              case Some((id, _)) =>
  15.248 +                do_cancel(serial, id)
  15.249 +              case None =>
  15.250 +            }
  15.251  
  15.252 -        case Clear_Memory =>
  15.253 -          memory_children = Map.empty
  15.254 -          memory = Map.empty
  15.255 -
  15.256 -        case Stop =>
  15.257 -          contexts = Map.empty
  15.258 -          exit("Simplifier_Trace: manager actor stopped")
  15.259 +          case Clear_Memory =>
  15.260 +            memory_children = Map.empty
  15.261 +            memory = Map.empty
  15.262  
  15.263 -        case Reply(session, serial, answer) =>
  15.264 -          find_question(serial) match {
  15.265 -            case Some((id, Question(data, _, _))) =>
  15.266 -              if (data.markup == Markup.SIMP_TRACE_STEP && data.memory)
  15.267 -              {
  15.268 -                val index = Index.of_data(data)
  15.269 -                memory += (index -> answer)
  15.270 -              }
  15.271 -              do_cancel(serial, id)
  15.272 -            case None =>
  15.273 -              System.err.println("send_reply: unknown serial " + serial)
  15.274 -          }
  15.275 +          case Reply(session, serial, answer) =>
  15.276 +            find_question(serial) match {
  15.277 +              case Some((id, Question(data, _, _))) =>
  15.278 +                if (data.markup == Markup.SIMP_TRACE_STEP && data.memory)
  15.279 +                {
  15.280 +                  val index = Index.of_data(data)
  15.281 +                  memory += (index -> answer)
  15.282 +                }
  15.283 +                do_cancel(serial, id)
  15.284 +              case None =>
  15.285 +                System.err.println("send_reply: unknown serial " + serial)
  15.286 +            }
  15.287  
  15.288 -          do_reply(session, serial, answer)
  15.289 -          session.trace_events.event(Event)
  15.290 -
  15.291 -        case bad =>
  15.292 -          System.err.println("context_manager: bad message " + bad)
  15.293 -      }
  15.294 -    }
  15.295 +            do_reply(session, serial, answer)
  15.296 +            session.trace_events.post(Event)
  15.297 +        }
  15.298 +        true
  15.299 +      },
  15.300 +      finish = () => contexts = Map.empty
  15.301 +    )
  15.302    }
  15.303  
  15.304  
  15.305 @@ -300,10 +306,12 @@
  15.306  
  15.307    class Handler extends Session.Protocol_Handler
  15.308    {
  15.309 +    assert(manager.is_active)
  15.310 +
  15.311      private def cancel(prover: Prover, msg: Prover.Protocol_Output): Boolean =
  15.312        msg.properties match {
  15.313          case Markup.Simp_Trace_Cancel(serial) =>
  15.314 -          manager ! Cancel(serial)
  15.315 +          manager.send(Cancel(serial))
  15.316            true
  15.317          case _ =>
  15.318            false
  15.319 @@ -311,8 +319,8 @@
  15.320  
  15.321      override def stop(prover: Prover) =
  15.322      {
  15.323 -      manager ! Clear_Memory
  15.324 -      manager ! Stop
  15.325 +      manager.send(Clear_Memory)
  15.326 +      manager.shutdown()
  15.327      }
  15.328  
  15.329      val functions = Map(Markup.SIMP_TRACE_CANCEL -> cancel _)
    16.1 --- a/src/Pure/build-jars	Fri Apr 25 12:09:15 2014 +0200
    16.2 +++ b/src/Pure/build-jars	Fri Apr 25 14:39:11 2014 +0200
    16.3 @@ -9,10 +9,12 @@
    16.4  ## sources
    16.5  
    16.6  declare -a SOURCES=(
    16.7 +  Concurrent/consumer_thread.scala
    16.8    Concurrent/counter.scala
    16.9    Concurrent/future.scala
   16.10 +  Concurrent/mailbox.scala
   16.11    Concurrent/simple_thread.scala
   16.12 -  Concurrent/volatile.scala
   16.13 +  Concurrent/synchronized.scala
   16.14    General/antiquote.scala
   16.15    General/bytes.scala
   16.16    General/completion.scala
   16.17 @@ -62,7 +64,6 @@
   16.18    PIDE/xml.scala
   16.19    PIDE/yxml.scala
   16.20    System/command_line.scala
   16.21 -  System/event_bus.scala
   16.22    System/interrupt.scala
   16.23    System/invoke_scala.scala
   16.24    System/isabelle_charset.scala
    17.1 --- a/src/Pure/library.scala	Fri Apr 25 12:09:15 2014 +0200
    17.2 +++ b/src/Pure/library.scala	Fri Apr 25 14:39:11 2014 +0200
    17.3 @@ -153,6 +153,14 @@
    17.4    }
    17.5  
    17.6  
    17.7 +  /* canonical list operations */
    17.8 +
    17.9 +  def member[A, B](xs: List[A])(x: B): Boolean = xs.exists(_ == x)
   17.10 +  def insert[A](x: A)(xs: List[A]): List[A] = if (xs.contains(x)) xs else x :: xs
   17.11 +  def remove[A, B](x: B)(xs: List[A]): List[A] = if (member(xs)(x)) xs.filterNot(_ == x) else xs
   17.12 +  def update[A](x: A)(xs: List[A]): List[A] = x :: remove(x)(xs)
   17.13 +
   17.14 +
   17.15    /* Java futures */
   17.16  
   17.17    def future_value[A](x: A) = new JFuture[A]
    18.1 --- a/src/Tools/jEdit/etc/settings	Fri Apr 25 12:09:15 2014 +0200
    18.2 +++ b/src/Tools/jEdit/etc/settings	Fri Apr 25 14:39:11 2014 +0200
    18.3 @@ -4,9 +4,9 @@
    18.4  JEDIT_SETTINGS="$ISABELLE_HOME_USER/jedit"
    18.5  
    18.6  JEDIT_OPTIONS="-reuseview -noserver -nobackground -log=9"
    18.7 -#JEDIT_JAVA_OPTIONS="-Xms128m -Xmx512m -Xss1m -Dactors.corePoolSize=4 -Dactors.enableForkJoin=false"
    18.8 -JEDIT_JAVA_OPTIONS="-Xms128m -Xmx1024m -Xss2m -Dactors.corePoolSize=4 -Dactors.enableForkJoin=false"
    18.9 -#JEDIT_JAVA_OPTIONS="-Xms512m -Xmx4096m -Xss8m -Dactors.corePoolSize=4 -Dactors.enableForkJoin=false"
   18.10 +#JEDIT_JAVA_OPTIONS="-Xms128m -Xmx512m -Xss1m -Dscala.concurrent.context.minThreads=1 -Dscala.concurrent.context.numThreads=x0.5 -Dscala.concurrent.context.maxThreads=8"
   18.11 +JEDIT_JAVA_OPTIONS="-Xms128m -Xmx1024m -Xss2m -Dscala.concurrent.context.minThreads=1 -Dscala.concurrent.context.numThreads=x0.5 -Dscala.concurrent.context.maxThreads=8"
   18.12 +#JEDIT_JAVA_OPTIONS="-Xms512m -Xmx4096m -Xss8m -Dscala.concurrent.context.minThreads=1 -Dscala.concurrent.context.numThreads=x0.5 -Dscala.concurrent.context.maxThreads=8"
   18.13  JEDIT_SYSTEM_OPTIONS="-Dawt.useSystemAAFontSettings=on -Dswing.aatext=true -Dapple.laf.useScreenMenuBar=true -Dapple.awt.application.name=Isabelle -Dscala.repl.no-threads=true"
   18.14  
   18.15  ISABELLE_JEDIT_OPTIONS=""
    19.1 --- a/src/Tools/jEdit/src/document_view.scala	Fri Apr 25 12:09:15 2014 +0200
    19.2 +++ b/src/Tools/jEdit/src/document_view.scala	Fri Apr 25 14:39:11 2014 +0200
    19.3 @@ -10,8 +10,6 @@
    19.4  
    19.5  import isabelle._
    19.6  
    19.7 -import scala.actors.Actor._
    19.8 -
    19.9  import java.awt.Graphics2D
   19.10  import java.awt.event.KeyEvent
   19.11  import javax.swing.event.{CaretListener, CaretEvent}
   19.12 @@ -176,7 +174,7 @@
   19.13  
   19.14    private val delay_caret_update =
   19.15      Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) {
   19.16 -      session.caret_focus.event(Session.Caret_Focus)
   19.17 +      session.caret_focus.post(Session.Caret_Focus)
   19.18      }
   19.19  
   19.20    private val caret_listener = new CaretListener {
   19.21 @@ -193,60 +191,54 @@
   19.22    }
   19.23  
   19.24  
   19.25 -  /* main actor */
   19.26 +  /* main */
   19.27  
   19.28 -  private val main_actor = actor {
   19.29 -    loop {
   19.30 -      react {
   19.31 -        case _: Session.Raw_Edits =>
   19.32 -          Swing_Thread.later {
   19.33 -            overview.delay_repaint.postpone(PIDE.options.seconds("editor_input_delay"))
   19.34 -          }
   19.35 +  private val main =
   19.36 +    Session.Consumer[Any](getClass.getName) {
   19.37 +      case _: Session.Raw_Edits =>
   19.38 +        Swing_Thread.later {
   19.39 +          overview.delay_repaint.postpone(PIDE.options.seconds("editor_input_delay"))
   19.40 +        }
   19.41  
   19.42 -        case changed: Session.Commands_Changed =>
   19.43 -          val buffer = model.buffer
   19.44 -          Swing_Thread.later {
   19.45 -            JEdit_Lib.buffer_lock(buffer) {
   19.46 -              if (model.buffer == text_area.getBuffer) {
   19.47 -                val snapshot = model.snapshot()
   19.48 +      case changed: Session.Commands_Changed =>
   19.49 +        val buffer = model.buffer
   19.50 +        Swing_Thread.later {
   19.51 +          JEdit_Lib.buffer_lock(buffer) {
   19.52 +            if (model.buffer == text_area.getBuffer) {
   19.53 +              val snapshot = model.snapshot()
   19.54  
   19.55 -                val load_changed =
   19.56 -                  snapshot.load_commands.exists(changed.commands.contains)
   19.57 +              val load_changed =
   19.58 +                snapshot.load_commands.exists(changed.commands.contains)
   19.59  
   19.60 -                if (changed.assignment || load_changed ||
   19.61 -                    (changed.nodes.contains(model.node_name) &&
   19.62 -                     changed.commands.exists(snapshot.node.commands.contains)))
   19.63 -                  Swing_Thread.later { overview.delay_repaint.invoke() }
   19.64 +              if (changed.assignment || load_changed ||
   19.65 +                  (changed.nodes.contains(model.node_name) &&
   19.66 +                   changed.commands.exists(snapshot.node.commands.contains)))
   19.67 +                Swing_Thread.later { overview.delay_repaint.invoke() }
   19.68  
   19.69 -                val visible_lines = text_area.getVisibleLines
   19.70 -                if (visible_lines > 0) {
   19.71 -                  if (changed.assignment || load_changed)
   19.72 -                    text_area.invalidateScreenLineRange(0, visible_lines)
   19.73 -                  else {
   19.74 -                    val visible_range = JEdit_Lib.visible_range(text_area).get
   19.75 -                    val visible_iterator =
   19.76 -                      snapshot.node.command_iterator(snapshot.revert(visible_range)).map(_._1)
   19.77 -                    if (visible_iterator.exists(changed.commands)) {
   19.78 -                      for {
   19.79 -                        line <- (0 until visible_lines).iterator
   19.80 -                        start = text_area.getScreenLineStartOffset(line) if start >= 0
   19.81 -                        end = text_area.getScreenLineEndOffset(line) if end >= 0
   19.82 -                        range = Text.Range(start, end)
   19.83 -                        line_cmds = snapshot.node.command_iterator(snapshot.revert(range)).map(_._1)
   19.84 -                        if line_cmds.exists(changed.commands)
   19.85 -                      } text_area.invalidateScreenLineRange(line, line)
   19.86 -                    }
   19.87 +              val visible_lines = text_area.getVisibleLines
   19.88 +              if (visible_lines > 0) {
   19.89 +                if (changed.assignment || load_changed)
   19.90 +                  text_area.invalidateScreenLineRange(0, visible_lines)
   19.91 +                else {
   19.92 +                  val visible_range = JEdit_Lib.visible_range(text_area).get
   19.93 +                  val visible_iterator =
   19.94 +                    snapshot.node.command_iterator(snapshot.revert(visible_range)).map(_._1)
   19.95 +                  if (visible_iterator.exists(changed.commands)) {
   19.96 +                    for {
   19.97 +                      line <- (0 until visible_lines).iterator
   19.98 +                      start = text_area.getScreenLineStartOffset(line) if start >= 0
   19.99 +                      end = text_area.getScreenLineEndOffset(line) if end >= 0
  19.100 +                      range = Text.Range(start, end)
  19.101 +                      line_cmds = snapshot.node.command_iterator(snapshot.revert(range)).map(_._1)
  19.102 +                      if line_cmds.exists(changed.commands)
  19.103 +                    } text_area.invalidateScreenLineRange(line, line)
  19.104                    }
  19.105                  }
  19.106                }
  19.107              }
  19.108            }
  19.109 -
  19.110 -        case bad =>
  19.111 -          System.err.println("command_change_actor: ignoring bad message " + bad)
  19.112 -      }
  19.113 +        }
  19.114      }
  19.115 -  }
  19.116  
  19.117  
  19.118    /* activation */
  19.119 @@ -261,16 +253,16 @@
  19.120      text_area.addKeyListener(key_listener)
  19.121      text_area.addCaretListener(caret_listener)
  19.122      text_area.addLeftOfScrollBar(overview)
  19.123 -    session.raw_edits += main_actor
  19.124 -    session.commands_changed += main_actor
  19.125 +    session.raw_edits += main
  19.126 +    session.commands_changed += main
  19.127    }
  19.128  
  19.129    private def deactivate()
  19.130    {
  19.131      val painter = text_area.getPainter
  19.132  
  19.133 -    session.raw_edits -= main_actor
  19.134 -    session.commands_changed -= main_actor
  19.135 +    session.raw_edits -= main
  19.136 +    session.commands_changed -= main
  19.137      text_area.removeLeftOfScrollBar(overview); overview.delay_repaint.revoke()
  19.138      text_area.removeCaretListener(caret_listener); delay_caret_update.revoke()
  19.139      text_area.removeKeyListener(key_listener)
    20.1 --- a/src/Tools/jEdit/src/find_dockable.scala	Fri Apr 25 12:09:15 2014 +0200
    20.2 +++ b/src/Tools/jEdit/src/find_dockable.scala	Fri Apr 25 14:39:11 2014 +0200
    20.3 @@ -9,8 +9,6 @@
    20.4  
    20.5  import isabelle._
    20.6  
    20.7 -import scala.actors.Actor._
    20.8 -
    20.9  import scala.swing.{Button, Component, TextField, CheckBox, Label, ComboBox}
   20.10  import scala.swing.event.ButtonClicked
   20.11  
   20.12 @@ -68,23 +66,16 @@
   20.13    })
   20.14  
   20.15  
   20.16 -  /* main actor */
   20.17 +  /* main */
   20.18  
   20.19 -  private val main_actor = actor {
   20.20 -    loop {
   20.21 -      react {
   20.22 -        case _: Session.Global_Options =>
   20.23 -          Swing_Thread.later { handle_resize() }
   20.24 -
   20.25 -        case bad =>
   20.26 -          System.err.println("Find_Dockable: ignoring bad message " + bad)
   20.27 -      }
   20.28 +  private val main =
   20.29 +    Session.Consumer[Session.Global_Options](getClass.getName) {
   20.30 +      case _: Session.Global_Options => Swing_Thread.later { handle_resize() }
   20.31      }
   20.32 -  }
   20.33  
   20.34    override def init()
   20.35    {
   20.36 -    PIDE.session.global_options += main_actor
   20.37 +    PIDE.session.global_options += main
   20.38      handle_resize()
   20.39      find_theorems.activate()
   20.40    }
   20.41 @@ -92,7 +83,7 @@
   20.42    override def exit()
   20.43    {
   20.44      find_theorems.deactivate()
   20.45 -    PIDE.session.global_options -= main_actor
   20.46 +    PIDE.session.global_options -= main
   20.47      delay_resize.revoke()
   20.48    }
   20.49  
    21.1 --- a/src/Tools/jEdit/src/info_dockable.scala	Fri Apr 25 12:09:15 2014 +0200
    21.2 +++ b/src/Tools/jEdit/src/info_dockable.scala	Fri Apr 25 14:39:11 2014 +0200
    21.3 @@ -9,8 +9,6 @@
    21.4  
    21.5  import isabelle._
    21.6  
    21.7 -import scala.actors.Actor._
    21.8 -
    21.9  import scala.swing.Button
   21.10  import scala.swing.event.ButtonClicked
   21.11  
   21.12 @@ -97,30 +95,24 @@
   21.13    add(controls.peer, BorderLayout.NORTH)
   21.14  
   21.15  
   21.16 -  /* main actor */
   21.17 +  /* main */
   21.18  
   21.19 -  private val main_actor = actor {
   21.20 -    loop {
   21.21 -      react {
   21.22 -        case _: Session.Global_Options =>
   21.23 -          Swing_Thread.later { handle_resize() }
   21.24 -
   21.25 -        case bad => System.err.println("Info_Dockable: ignoring bad message " + bad)
   21.26 -      }
   21.27 +  private val main =
   21.28 +    Session.Consumer[Session.Global_Options](getClass.getName) {
   21.29 +      case _: Session.Global_Options => Swing_Thread.later { handle_resize() }
   21.30      }
   21.31 -  }
   21.32  
   21.33    override def init()
   21.34    {
   21.35      GUI.parent_window(this).map(_.addWindowFocusListener(window_focus_listener))
   21.36 -    PIDE.session.global_options += main_actor
   21.37 +    PIDE.session.global_options += main
   21.38      handle_resize()
   21.39    }
   21.40  
   21.41    override def exit()
   21.42    {
   21.43      GUI.parent_window(this).map(_.removeWindowFocusListener(window_focus_listener))
   21.44 -    PIDE.session.global_options -= main_actor
   21.45 +    PIDE.session.global_options -= main
   21.46      delay_resize.revoke()
   21.47    }
   21.48  }
    22.1 --- a/src/Tools/jEdit/src/jedit_lib.scala	Fri Apr 25 12:09:15 2014 +0200
    22.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Fri Apr 25 14:39:11 2014 +0200
    22.3 @@ -215,9 +215,12 @@
    22.4      val buffer = text_area.getBuffer
    22.5      buffer_range(buffer).try_restrict(range) match {
    22.6        case Some(range1) if !range1.is_singularity =>
    22.7 -        text_area.invalidateLineRange(
    22.8 -          buffer.getLineOfOffset(range1.start),
    22.9 -          buffer.getLineOfOffset(range1.stop))
   22.10 +        try {
   22.11 +          text_area.invalidateLineRange(
   22.12 +            buffer.getLineOfOffset(range1.start),
   22.13 +            buffer.getLineOfOffset(range1.stop))
   22.14 +        }
   22.15 +        catch { case _: ArrayIndexOutOfBoundsException => }
   22.16        case _ =>
   22.17      }
   22.18    }
    23.1 --- a/src/Tools/jEdit/src/monitor_dockable.scala	Fri Apr 25 12:09:15 2014 +0200
    23.2 +++ b/src/Tools/jEdit/src/monitor_dockable.scala	Fri Apr 25 14:39:11 2014 +0200
    23.3 @@ -9,7 +9,6 @@
    23.4  
    23.5  import isabelle._
    23.6  
    23.7 -import scala.actors.Actor._
    23.8  import scala.swing.{TextArea, ScrollPane, Component}
    23.9  
   23.10  import org.jfree.chart.ChartPanel
   23.11 @@ -35,23 +34,18 @@
   23.12    set_content(new ChartPanel(chart))
   23.13  
   23.14  
   23.15 -  /* main actor */
   23.16 +  /* main */
   23.17  
   23.18 -  private val main_actor = actor {
   23.19 -    loop {
   23.20 -      react {
   23.21 -        case Session.Statistics(props) =>
   23.22 -          Swing_Thread.later {
   23.23 -            rev_stats ::= props
   23.24 -            delay_update.invoke()
   23.25 -          }
   23.26 +  private val main =
   23.27 +    Session.Consumer[Session.Statistics](getClass.getName) {
   23.28 +      case stats =>
   23.29 +        Swing_Thread.later {
   23.30 +          rev_stats ::= stats.props
   23.31 +          delay_update.invoke()
   23.32 +        }
   23.33 +    }
   23.34  
   23.35 -        case bad => System.err.println("Monitor_Dockable: ignoring bad message " + bad)
   23.36 -      }
   23.37 -    }
   23.38 -  }
   23.39 -
   23.40 -  override def init() { PIDE.session.statistics += main_actor }
   23.41 -  override def exit() { PIDE.session.statistics -= main_actor }
   23.42 +  override def init() { PIDE.session.statistics += main }
   23.43 +  override def exit() { PIDE.session.statistics -= main }
   23.44  }
   23.45  
    24.1 --- a/src/Tools/jEdit/src/output_dockable.scala	Fri Apr 25 12:09:15 2014 +0200
    24.2 +++ b/src/Tools/jEdit/src/output_dockable.scala	Fri Apr 25 14:39:11 2014 +0200
    24.3 @@ -9,8 +9,6 @@
    24.4  
    24.5  import isabelle._
    24.6  
    24.7 -import scala.actors.Actor._
    24.8 -
    24.9  import scala.swing.{Button, CheckBox}
   24.10  import scala.swing.event.ButtonClicked
   24.11  
   24.12 @@ -82,39 +80,34 @@
   24.13    }
   24.14  
   24.15  
   24.16 -  /* main actor */
   24.17 +  /* main */
   24.18  
   24.19 -  private val main_actor = actor {
   24.20 -    loop {
   24.21 -      react {
   24.22 -        case _: Session.Global_Options =>
   24.23 -          Swing_Thread.later { handle_resize() }
   24.24 +  private val main =
   24.25 +    Session.Consumer[Any](getClass.getName) {
   24.26 +      case _: Session.Global_Options =>
   24.27 +        Swing_Thread.later { handle_resize() }
   24.28  
   24.29 -        case changed: Session.Commands_Changed =>
   24.30 -          val restriction = if (changed.assignment) None else Some(changed.commands)
   24.31 -          Swing_Thread.later { handle_update(do_update, restriction) }
   24.32 +      case changed: Session.Commands_Changed =>
   24.33 +        val restriction = if (changed.assignment) None else Some(changed.commands)
   24.34 +        Swing_Thread.later { handle_update(do_update, restriction) }
   24.35  
   24.36 -        case Session.Caret_Focus =>
   24.37 -          Swing_Thread.later { handle_update(do_update, None) }
   24.38 -
   24.39 -        case bad => System.err.println("Output_Dockable: ignoring bad message " + bad)
   24.40 -      }
   24.41 +      case Session.Caret_Focus =>
   24.42 +        Swing_Thread.later { handle_update(do_update, None) }
   24.43      }
   24.44 -  }
   24.45  
   24.46    override def init()
   24.47    {
   24.48 -    PIDE.session.global_options += main_actor
   24.49 -    PIDE.session.commands_changed += main_actor
   24.50 -    PIDE.session.caret_focus += main_actor
   24.51 +    PIDE.session.global_options += main
   24.52 +    PIDE.session.commands_changed += main
   24.53 +    PIDE.session.caret_focus += main
   24.54      handle_update(true, None)
   24.55    }
   24.56  
   24.57    override def exit()
   24.58    {
   24.59 -    PIDE.session.global_options -= main_actor
   24.60 -    PIDE.session.commands_changed -= main_actor
   24.61 -    PIDE.session.caret_focus -= main_actor
   24.62 +    PIDE.session.global_options -= main
   24.63 +    PIDE.session.commands_changed -= main
   24.64 +    PIDE.session.caret_focus -= main
   24.65      delay_resize.revoke()
   24.66    }
   24.67  
    25.1 --- a/src/Tools/jEdit/src/plugin.scala	Fri Apr 25 12:09:15 2014 +0200
    25.2 +++ b/src/Tools/jEdit/src/plugin.scala	Fri Apr 25 14:39:11 2014 +0200
    25.3 @@ -22,8 +22,6 @@
    25.4  
    25.5  import org.gjt.sp.util.SyntaxUtilities
    25.6  
    25.7 -import scala.actors.Actor._
    25.8 -
    25.9  
   25.10  object PIDE
   25.11  {
   25.12 @@ -174,7 +172,7 @@
   25.13  
   25.14    def options_changed()
   25.15    {
   25.16 -    PIDE.session.global_options.event(Session.Global_Options(PIDE.options.value))
   25.17 +    PIDE.session.global_options.post(Session.Global_Options(PIDE.options.value))
   25.18      Swing_Thread.later { delay_load.invoke() }
   25.19    }
   25.20  
   25.21 @@ -244,34 +242,27 @@
   25.22      }
   25.23  
   25.24  
   25.25 -  /* session manager */
   25.26 +  /* session phase */
   25.27  
   25.28 -  private val session_manager = actor {
   25.29 -    loop {
   25.30 -      react {
   25.31 -        case phase: Session.Phase =>
   25.32 -          phase match {
   25.33 -            case Session.Inactive | Session.Failed =>
   25.34 -              Swing_Thread.later {
   25.35 -                GUI.error_dialog(jEdit.getActiveView, "Prover process terminated",
   25.36 -                    "Isabelle Syslog", GUI.scrollable_text(PIDE.session.current_syslog()))
   25.37 -              }
   25.38 +  private val session_phase =
   25.39 +    Session.Consumer[Session.Phase](getClass.getName) {
   25.40 +      case Session.Inactive | Session.Failed =>
   25.41 +        Swing_Thread.later {
   25.42 +          GUI.error_dialog(jEdit.getActiveView, "Prover process terminated",
   25.43 +              "Isabelle Syslog", GUI.scrollable_text(PIDE.session.current_syslog()))
   25.44 +        }
   25.45  
   25.46 -            case Session.Ready =>
   25.47 -              PIDE.session.update_options(PIDE.options.value)
   25.48 -              PIDE.init_models()
   25.49 -              Swing_Thread.later { delay_load.invoke() }
   25.50 +      case Session.Ready =>
   25.51 +        PIDE.session.update_options(PIDE.options.value)
   25.52 +        PIDE.init_models()
   25.53 +        Swing_Thread.later { delay_load.invoke() }
   25.54  
   25.55 -            case Session.Shutdown =>
   25.56 -              PIDE.exit_models(JEdit_Lib.jedit_buffers().toList)
   25.57 -              Swing_Thread.later { delay_load.revoke() }
   25.58 +      case Session.Shutdown =>
   25.59 +        PIDE.exit_models(JEdit_Lib.jedit_buffers().toList)
   25.60 +        Swing_Thread.later { delay_load.revoke() }
   25.61  
   25.62 -            case _ =>
   25.63 -          }
   25.64 -        case bad => System.err.println("session_manager: ignoring bad message " + bad)
   25.65 -      }
   25.66 +      case _ =>
   25.67      }
   25.68 -  }
   25.69  
   25.70  
   25.71    /* main plugin plumbing */
   25.72 @@ -366,7 +357,7 @@
   25.73          override def reparse_limit = PIDE.options.int("editor_reparse_limit")
   25.74        }
   25.75  
   25.76 -      PIDE.session.phase_changed += session_manager
   25.77 +      PIDE.session.phase_changed += session_phase
   25.78        PIDE.startup_failure = None
   25.79      }
   25.80      catch {
   25.81 @@ -385,7 +376,7 @@
   25.82        PIDE.completion_history.value.save()
   25.83      }
   25.84  
   25.85 -    PIDE.session.phase_changed -= session_manager
   25.86 +    PIDE.session.phase_changed -= session_phase
   25.87      PIDE.exit_models(JEdit_Lib.jedit_buffers().toList)
   25.88      PIDE.session.stop()
   25.89    }
    26.1 --- a/src/Tools/jEdit/src/pretty_text_area.scala	Fri Apr 25 12:09:15 2014 +0200
    26.2 +++ b/src/Tools/jEdit/src/pretty_text_area.scala	Fri Apr 25 14:39:11 2014 +0200
    26.3 @@ -36,7 +36,7 @@
    26.4      val nodes1 = nodes0 + (node_name -> nodes0(node_name).update_commands(Linear_Set(command)))
    26.5      val version1 = Document.Version.make(version0.syntax, nodes1)
    26.6      val state1 =
    26.7 -      state0.continue_history(Future.value(version0), edits, Future.value(version1))._2
    26.8 +      state0.continue_history(Future.value(version0), edits, Future.value(version1))
    26.9          .define_version(version1, state0.the_assignment(version0))
   26.10          .assign(version1.id, List(command.id -> List(Document_ID.make())))._2
   26.11  
    27.1 --- a/src/Tools/jEdit/src/protocol_dockable.scala	Fri Apr 25 12:09:15 2014 +0200
    27.2 +++ b/src/Tools/jEdit/src/protocol_dockable.scala	Fri Apr 25 14:39:11 2014 +0200
    27.3 @@ -9,7 +9,6 @@
    27.4  
    27.5  import isabelle._
    27.6  
    27.7 -import scala.actors.Actor._
    27.8  import scala.swing.{TextArea, ScrollPane}
    27.9  
   27.10  import org.gjt.sp.jedit.View
   27.11 @@ -21,22 +20,17 @@
   27.12    set_content(new ScrollPane(text_area))
   27.13  
   27.14  
   27.15 -  /* main actor */
   27.16 +  /* main */
   27.17  
   27.18 -  private val main_actor = actor {
   27.19 -    loop {
   27.20 -      react {
   27.21 -        case input: Prover.Input =>
   27.22 -          Swing_Thread.later { text_area.append(input.toString + "\n\n") }
   27.23 +  private val main =
   27.24 +    Session.Consumer[Prover.Message](getClass.getName) {
   27.25 +      case input: Prover.Input =>
   27.26 +        Swing_Thread.later { text_area.append(input.toString + "\n\n") }
   27.27  
   27.28 -        case output: Prover.Output =>
   27.29 -          Swing_Thread.later { text_area.append(output.message.toString + "\n\n") }
   27.30 -
   27.31 -        case bad => System.err.println("Protocol_Dockable: ignoring bad message " + bad)
   27.32 -      }
   27.33 +      case output: Prover.Output =>
   27.34 +        Swing_Thread.later { text_area.append(output.message.toString + "\n\n") }
   27.35      }
   27.36 -  }
   27.37  
   27.38 -  override def init() { PIDE.session.all_messages += main_actor }
   27.39 -  override def exit() { PIDE.session.all_messages -= main_actor }
   27.40 +  override def init() { PIDE.session.all_messages += main }
   27.41 +  override def exit() { PIDE.session.all_messages -= main }
   27.42  }
    28.1 --- a/src/Tools/jEdit/src/raw_output_dockable.scala	Fri Apr 25 12:09:15 2014 +0200
    28.2 +++ b/src/Tools/jEdit/src/raw_output_dockable.scala	Fri Apr 25 14:39:11 2014 +0200
    28.3 @@ -9,7 +9,6 @@
    28.4  
    28.5  import isabelle._
    28.6  
    28.7 -import scala.actors.Actor._
    28.8  import scala.swing.{TextArea, ScrollPane}
    28.9  
   28.10  import org.gjt.sp.jedit.View
   28.11 @@ -21,22 +20,17 @@
   28.12    set_content(new ScrollPane(text_area))
   28.13  
   28.14  
   28.15 -  /* main actor */
   28.16 +  /* main */
   28.17  
   28.18 -  private val main_actor = actor {
   28.19 -    loop {
   28.20 -      react {
   28.21 -        case output: Prover.Output =>
   28.22 -          Swing_Thread.later {
   28.23 -            text_area.append(XML.content(output.message))
   28.24 -            if (!output.is_stdout && !output.is_stderr) text_area.append("\n")
   28.25 -          }
   28.26 +  private val main =
   28.27 +    Session.Consumer[Prover.Output](getClass.getName) {
   28.28 +      case output: Prover.Output =>
   28.29 +        Swing_Thread.later {
   28.30 +          text_area.append(XML.content(output.message))
   28.31 +          if (!output.is_stdout && !output.is_stderr) text_area.append("\n")
   28.32 +        }
   28.33 +    }
   28.34  
   28.35 -        case bad => System.err.println("Raw_Output_Dockable: ignoring bad message " + bad)
   28.36 -      }
   28.37 -    }
   28.38 -  }
   28.39 -
   28.40 -  override def init() { PIDE.session.raw_output_messages += main_actor }
   28.41 -  override def exit() { PIDE.session.raw_output_messages -= main_actor }
   28.42 +  override def init() { PIDE.session.raw_output_messages += main }
   28.43 +  override def exit() { PIDE.session.raw_output_messages -= main }
   28.44  }
    29.1 --- a/src/Tools/jEdit/src/simplifier_trace_dockable.scala	Fri Apr 25 12:09:15 2014 +0200
    29.2 +++ b/src/Tools/jEdit/src/simplifier_trace_dockable.scala	Fri Apr 25 14:39:11 2014 +0200
    29.3 @@ -9,7 +9,6 @@
    29.4  
    29.5  import isabelle._
    29.6  
    29.7 -import scala.actors.Actor._
    29.8  import scala.swing.{Button, CheckBox, Orientation, Separator}
    29.9  import scala.swing.event.ButtonClicked
   29.10  
   29.11 @@ -127,32 +126,31 @@
   29.12    }
   29.13  
   29.14  
   29.15 -  /* main actor */
   29.16 +  /* main */
   29.17 +
   29.18 +  private val main =
   29.19 +    Session.Consumer[Any](getClass.getName) {
   29.20 +      case _: Session.Global_Options =>
   29.21 +        Swing_Thread.later { handle_resize() }
   29.22  
   29.23 -  private val main_actor = actor {
   29.24 -    loop {
   29.25 -      react {
   29.26 -        case _: Session.Global_Options =>
   29.27 -          Swing_Thread.later { handle_resize() }
   29.28 -        case changed: Session.Commands_Changed =>
   29.29 -          Swing_Thread.later { handle_update(do_update) }
   29.30 -        case Session.Caret_Focus =>
   29.31 -          Swing_Thread.later { handle_update(do_update) }
   29.32 -        case Simplifier_Trace.Event =>
   29.33 -          Swing_Thread.later { handle_update(do_update) }
   29.34 -        case bad => System.err.println("Simplifier_Trace_Dockable: ignoring bad message " + bad)
   29.35 -      }
   29.36 +      case changed: Session.Commands_Changed =>
   29.37 +        Swing_Thread.later { handle_update(do_update) }
   29.38 +
   29.39 +      case Session.Caret_Focus =>
   29.40 +        Swing_Thread.later { handle_update(do_update) }
   29.41 +
   29.42 +      case Simplifier_Trace.Event =>
   29.43 +        Swing_Thread.later { handle_update(do_update) }
   29.44      }
   29.45 -  }
   29.46  
   29.47    override def init()
   29.48    {
   29.49      Swing_Thread.require {}
   29.50  
   29.51 -    PIDE.session.global_options += main_actor
   29.52 -    PIDE.session.commands_changed += main_actor
   29.53 -    PIDE.session.caret_focus += main_actor
   29.54 -    PIDE.session.trace_events += main_actor
   29.55 +    PIDE.session.global_options += main
   29.56 +    PIDE.session.commands_changed += main
   29.57 +    PIDE.session.caret_focus += main
   29.58 +    PIDE.session.trace_events += main
   29.59      handle_update(true)
   29.60    }
   29.61  
   29.62 @@ -160,10 +158,10 @@
   29.63    {
   29.64      Swing_Thread.require {}
   29.65  
   29.66 -    PIDE.session.global_options -= main_actor
   29.67 -    PIDE.session.commands_changed -= main_actor
   29.68 -    PIDE.session.caret_focus -= main_actor
   29.69 -    PIDE.session.trace_events -= main_actor
   29.70 +    PIDE.session.global_options -= main
   29.71 +    PIDE.session.commands_changed -= main
   29.72 +    PIDE.session.caret_focus -= main
   29.73 +    PIDE.session.trace_events -= main
   29.74      delay_resize.revoke()
   29.75    }
   29.76  
    30.1 --- a/src/Tools/jEdit/src/sledgehammer_dockable.scala	Fri Apr 25 12:09:15 2014 +0200
    30.2 +++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala	Fri Apr 25 14:39:11 2014 +0200
    30.3 @@ -9,8 +9,6 @@
    30.4  
    30.5  import isabelle._
    30.6  
    30.7 -import scala.actors.Actor._
    30.8 -
    30.9  import scala.swing.{Button, Component, Label, TextField, CheckBox}
   30.10  import scala.swing.event.ButtonClicked
   30.11  
   30.12 @@ -135,23 +133,16 @@
   30.13    override def focusOnDefaultComponent { provers.requestFocus }
   30.14  
   30.15  
   30.16 -  /* main actor */
   30.17 +  /* main */
   30.18  
   30.19 -  private val main_actor = actor {
   30.20 -    loop {
   30.21 -      react {
   30.22 -        case _: Session.Global_Options =>
   30.23 -          Swing_Thread.later { update_provers(); handle_resize() }
   30.24 -
   30.25 -        case bad =>
   30.26 -          System.err.println("Sledgehammer_Dockable: ignoring bad message " + bad)
   30.27 -      }
   30.28 +  private val main =
   30.29 +    Session.Consumer[Session.Global_Options](getClass.getName) {
   30.30 +      case _: Session.Global_Options => Swing_Thread.later { update_provers(); handle_resize() }
   30.31      }
   30.32 -  }
   30.33  
   30.34    override def init()
   30.35    {
   30.36 -    PIDE.session.global_options += main_actor
   30.37 +    PIDE.session.global_options += main
   30.38      update_provers()
   30.39      handle_resize()
   30.40      sledgehammer.activate()
   30.41 @@ -160,7 +151,7 @@
   30.42    override def exit()
   30.43    {
   30.44      sledgehammer.deactivate()
   30.45 -    PIDE.session.global_options -= main_actor
   30.46 +    PIDE.session.global_options -= main
   30.47      delay_resize.revoke()
   30.48    }
   30.49  }
    31.1 --- a/src/Tools/jEdit/src/syslog_dockable.scala	Fri Apr 25 12:09:15 2014 +0200
    31.2 +++ b/src/Tools/jEdit/src/syslog_dockable.scala	Fri Apr 25 14:39:11 2014 +0200
    31.3 @@ -9,7 +9,6 @@
    31.4  
    31.5  import isabelle._
    31.6  
    31.7 -import scala.actors.Actor._
    31.8  import scala.swing.TextArea
    31.9  
   31.10  import org.gjt.sp.jedit.View
   31.11 @@ -32,27 +31,22 @@
   31.12    set_content(syslog)
   31.13  
   31.14  
   31.15 -  /* main actor */
   31.16 +  /* main */
   31.17  
   31.18 -  private val main_actor = actor {
   31.19 -    loop {
   31.20 -      react {
   31.21 -        case output: Prover.Output =>
   31.22 -          if (output.is_syslog) Swing_Thread.later { update_syslog() }
   31.23 -
   31.24 -        case bad => System.err.println("Syslog_Dockable: ignoring bad message " + bad)
   31.25 -      }
   31.26 +  private val main =
   31.27 +    Session.Consumer[Prover.Output](getClass.getName) {
   31.28 +      case output =>
   31.29 +        if (output.is_syslog) Swing_Thread.later { update_syslog() }
   31.30      }
   31.31 -  }
   31.32  
   31.33    override def init()
   31.34    {
   31.35 -    PIDE.session.syslog_messages += main_actor
   31.36 +    PIDE.session.syslog_messages += main
   31.37      update_syslog()
   31.38    }
   31.39  
   31.40    override def exit()
   31.41    {
   31.42 -    PIDE.session.syslog_messages -= main_actor
   31.43 +    PIDE.session.syslog_messages -= main
   31.44    }
   31.45  }
    32.1 --- a/src/Tools/jEdit/src/theories_dockable.scala	Fri Apr 25 12:09:15 2014 +0200
    32.2 +++ b/src/Tools/jEdit/src/theories_dockable.scala	Fri Apr 25 14:39:11 2014 +0200
    32.3 @@ -9,7 +9,6 @@
    32.4  
    32.5  import isabelle._
    32.6  
    32.7 -import scala.actors.Actor._
    32.8  import scala.swing.{Button, TextArea, Label, ListView, Alignment,
    32.9    ScrollPane, Component, CheckBox, BorderPanel}
   32.10  import scala.swing.event.{MouseClicked, MouseMoved}
   32.11 @@ -216,35 +215,30 @@
   32.12    }
   32.13  
   32.14  
   32.15 -  /* main actor */
   32.16 +  /* main */
   32.17  
   32.18 -  private val main_actor = actor {
   32.19 -    loop {
   32.20 -      react {
   32.21 -        case phase: Session.Phase =>
   32.22 -          Swing_Thread.later { handle_phase(phase) }
   32.23 +  private val main =
   32.24 +    Session.Consumer[Any](getClass.getName) {
   32.25 +      case phase: Session.Phase =>
   32.26 +        Swing_Thread.later { handle_phase(phase) }
   32.27  
   32.28 -        case _: Session.Global_Options =>
   32.29 -          Swing_Thread.later {
   32.30 -            continuous_checking.load()
   32.31 -            logic.load ()
   32.32 -            update_nodes_required()
   32.33 -            status.repaint()
   32.34 -          }
   32.35 +      case _: Session.Global_Options =>
   32.36 +        Swing_Thread.later {
   32.37 +          continuous_checking.load()
   32.38 +          logic.load ()
   32.39 +          update_nodes_required()
   32.40 +          status.repaint()
   32.41 +        }
   32.42  
   32.43 -        case changed: Session.Commands_Changed =>
   32.44 -          Swing_Thread.later { handle_update(Some(changed.nodes)) }
   32.45 -
   32.46 -        case bad => System.err.println("Theories_Dockable: ignoring bad message " + bad)
   32.47 -      }
   32.48 +      case changed: Session.Commands_Changed =>
   32.49 +        Swing_Thread.later { handle_update(Some(changed.nodes)) }
   32.50      }
   32.51 -  }
   32.52  
   32.53    override def init()
   32.54    {
   32.55 -    PIDE.session.phase_changed += main_actor
   32.56 -    PIDE.session.global_options += main_actor
   32.57 -    PIDE.session.commands_changed += main_actor
   32.58 +    PIDE.session.phase_changed += main
   32.59 +    PIDE.session.global_options += main
   32.60 +    PIDE.session.commands_changed += main
   32.61  
   32.62      handle_phase(PIDE.session.phase)
   32.63      handle_update()
   32.64 @@ -252,8 +246,8 @@
   32.65  
   32.66    override def exit()
   32.67    {
   32.68 -    PIDE.session.phase_changed -= main_actor
   32.69 -    PIDE.session.global_options -= main_actor
   32.70 -    PIDE.session.commands_changed -= main_actor
   32.71 +    PIDE.session.phase_changed -= main
   32.72 +    PIDE.session.global_options -= main
   32.73 +    PIDE.session.commands_changed -= main
   32.74    }
   32.75  }
    33.1 --- a/src/Tools/jEdit/src/timing_dockable.scala	Fri Apr 25 12:09:15 2014 +0200
    33.2 +++ b/src/Tools/jEdit/src/timing_dockable.scala	Fri Apr 25 14:39:11 2014 +0200
    33.3 @@ -9,7 +9,6 @@
    33.4  
    33.5  import isabelle._
    33.6  
    33.7 -import scala.actors.Actor._
    33.8  import scala.swing.{Label, ListView, Alignment, ScrollPane, Component, TextField}
    33.9  import scala.swing.event.{MouseClicked, ValueChanged}
   33.10  
   33.11 @@ -200,27 +199,22 @@
   33.12    }
   33.13  
   33.14  
   33.15 -  /* main actor */
   33.16 +  /* main */
   33.17  
   33.18 -  private val main_actor = actor {
   33.19 -    loop {
   33.20 -      react {
   33.21 -        case changed: Session.Commands_Changed =>
   33.22 -          Swing_Thread.later { handle_update(Some(changed.nodes)) }
   33.23 -
   33.24 -        case bad => System.err.println("Timing_Dockable: ignoring bad message " + bad)
   33.25 -      }
   33.26 +  private val main =
   33.27 +    Session.Consumer[Session.Commands_Changed](getClass.getName) {
   33.28 +      case changed =>
   33.29 +        Swing_Thread.later { handle_update(Some(changed.nodes)) }
   33.30      }
   33.31 -  }
   33.32  
   33.33    override def init()
   33.34    {
   33.35 -    PIDE.session.commands_changed += main_actor
   33.36 +    PIDE.session.commands_changed += main
   33.37      handle_update()
   33.38    }
   33.39  
   33.40    override def exit()
   33.41    {
   33.42 -    PIDE.session.commands_changed -= main_actor
   33.43 +    PIDE.session.commands_changed -= main
   33.44    }
   33.45  }