src/Pure/System/session.scala
changeset 38639 f642faca303e
parent 38569 9d480f6a2589
child 38722 ba31936497c2
     1.1 --- a/src/Pure/System/session.scala	Mon Aug 23 16:50:09 2010 +0200
     1.2 +++ b/src/Pure/System/session.scala	Mon Aug 23 16:53:22 2010 +0200
     1.3 @@ -69,8 +69,8 @@
     1.4    private case class Started(timeout: Int, args: List[String])
     1.5    private case object Stop
     1.6  
     1.7 -  private lazy val session_actor = actor {
     1.8 -
     1.9 +  private val session_actor = Simple_Thread.actor("session_actor", daemon = true)
    1.10 +  {
    1.11      var prover: Isabelle_Process with Isar_Document = null
    1.12  
    1.13  
    1.14 @@ -199,8 +199,9 @@
    1.15  
    1.16      /* main loop */
    1.17  
    1.18 -    loop {
    1.19 -      react {
    1.20 +    var finished = false
    1.21 +    while (!finished) {
    1.22 +      receive {
    1.23          case Started(timeout, args) =>
    1.24            if (prover == null) {
    1.25              prover = new Isabelle_Process(system, self, args:_*) with Isar_Document
    1.26 @@ -211,10 +212,11 @@
    1.27            }
    1.28            else reply(None)
    1.29  
    1.30 -        case Stop =>  // FIXME clarify; synchronous
    1.31 +        case Stop => // FIXME synchronous!?
    1.32            if (prover != null) {
    1.33              prover.kill
    1.34              prover = null
    1.35 +            finished = true
    1.36            }
    1.37  
    1.38          case change: Document.Change if prover != null =>
    1.39 @@ -235,7 +237,7 @@
    1.40  
    1.41    /** buffered command changes (delay_first discipline) **/
    1.42  
    1.43 -  private lazy val command_change_buffer = actor
    1.44 +  private val command_change_buffer = actor
    1.45    //{{{
    1.46    {
    1.47      import scala.compat.Platform.currentTime
    1.48 @@ -286,36 +288,33 @@
    1.49  
    1.50    private case class Edit_Version(edits: List[Document.Node_Text_Edit])
    1.51  
    1.52 -  private val editor_history = new Actor
    1.53 -  {
    1.54 -    @volatile private var history = Document.History.init
    1.55 +  @volatile private var history = Document.History.init
    1.56  
    1.57 -    def snapshot(name: String, pending_edits: List[Text.Edit]): Document.Snapshot =
    1.58 -      history.snapshot(name, pending_edits, current_state())
    1.59 +  def snapshot(name: String, pending_edits: List[Text.Edit]): Document.Snapshot =
    1.60 +    history.snapshot(name, pending_edits, current_state())
    1.61  
    1.62 -    def act
    1.63 -    {
    1.64 -      loop {
    1.65 -        react {
    1.66 -          case Edit_Version(edits) =>
    1.67 -            val prev = history.tip.current
    1.68 -            val result =
    1.69 -              isabelle.Future.fork {
    1.70 -                val previous = prev.join
    1.71 -                val former_assignment = current_state().the_assignment(previous).join  // FIXME async!?
    1.72 -                Thy_Syntax.text_edits(Session.this, previous, edits)
    1.73 -              }
    1.74 -            val change = new Document.Change(prev, edits, result)
    1.75 -            history += change
    1.76 -            change.current.map(_ => session_actor ! change)
    1.77 -            reply(())
    1.78 +  private val editor_history = actor
    1.79 +  {
    1.80 +    loop {
    1.81 +      react {
    1.82 +        case Edit_Version(edits) =>
    1.83 +          val prev = history.tip.current
    1.84 +          val result =
    1.85 +            // FIXME potential denial-of-service concerning worker pool (!?!?)
    1.86 +            isabelle.Future.fork {
    1.87 +              val previous = prev.join
    1.88 +              val former_assignment = current_state().the_assignment(previous).join  // FIXME async!?
    1.89 +              Thy_Syntax.text_edits(Session.this, previous, edits)
    1.90 +            }
    1.91 +          val change = new Document.Change(prev, edits, result)
    1.92 +          history += change
    1.93 +          change.current.map(_ => session_actor ! change)
    1.94 +          reply(())
    1.95  
    1.96 -          case bad => System.err.println("editor_model: ignoring bad message " + bad)
    1.97 -        }
    1.98 +        case bad => System.err.println("editor_model: ignoring bad message " + bad)
    1.99        }
   1.100      }
   1.101    }
   1.102 -  editor_history.start
   1.103  
   1.104  
   1.105  
   1.106 @@ -326,8 +325,5 @@
   1.107  
   1.108    def stop() { session_actor ! Stop }
   1.109  
   1.110 -  def snapshot(name: String, pending_edits: List[Text.Edit]): Document.Snapshot =
   1.111 -    editor_history.snapshot(name, pending_edits)
   1.112 -
   1.113    def edit_version(edits: List[Document.Node_Text_Edit]) { editor_history !? Edit_Version(edits) }
   1.114  }