src/Pure/Tools/simplifier_trace.scala
changeset 56718 096139bcfadd
parent 56717 d96b10ec397c
child 56782 433cf57550fa
     1.1 --- a/src/Pure/Tools/simplifier_trace.scala	Fri Apr 25 12:59:33 2014 +0200
     1.2 +++ b/src/Pure/Tools/simplifier_trace.scala	Fri Apr 25 13:29:56 2014 +0200
     1.3 @@ -7,7 +7,6 @@
     1.4  package isabelle
     1.5  
     1.6  
     1.7 -import scala.actors.Actor._
     1.8  import scala.annotation.tailrec
     1.9  import scala.collection.immutable.SortedMap
    1.10  
    1.11 @@ -102,14 +101,13 @@
    1.12    case object Event
    1.13  
    1.14  
    1.15 -  /* manager actor */
    1.16 +  /* manager thread */
    1.17  
    1.18    private case class Handle_Results(
    1.19 -    session: Session, id: Document_ID.Command, results: Command.Results)
    1.20 -  private case class Generate_Trace(results: Command.Results)
    1.21 +    session: Session, id: Document_ID.Command, results: Command.Results, slot: Promise[Context])
    1.22 +  private case class Generate_Trace(results: Command.Results, slot: Promise[Trace])
    1.23    private case class Cancel(serial: Long)
    1.24    private object Clear_Memory
    1.25 -  private object Stop
    1.26    case class Reply(session: Session, serial: Long, answer: Answer)
    1.27  
    1.28    case class Question(data: Item.Data, answers: List[Answer], default_answer: Answer)
    1.29 @@ -139,18 +137,27 @@
    1.30    }
    1.31  
    1.32    def handle_results(session: Session, id: Document_ID.Command, results: Command.Results): Context =
    1.33 -    (manager !? Handle_Results(session, id, results)).asInstanceOf[Context]
    1.34 +  {
    1.35 +    val slot = Future.promise[Context]
    1.36 +    manager.send(Handle_Results(session, id, results, slot))
    1.37 +    slot.join
    1.38 +  }
    1.39  
    1.40    def generate_trace(results: Command.Results): Trace =
    1.41 -    (manager !? Generate_Trace(results)).asInstanceOf[Trace]
    1.42 +  {
    1.43 +    val slot = Future.promise[Trace]
    1.44 +    manager.send(Generate_Trace(results, slot))
    1.45 +    slot.join
    1.46 +  }
    1.47  
    1.48    def clear_memory() =
    1.49 -    manager ! Clear_Memory
    1.50 +    manager.send(Clear_Memory)
    1.51  
    1.52    def send_reply(session: Session, serial: Long, answer: Answer) =
    1.53 -    manager ! Reply(session, serial, answer)
    1.54 +    manager.send(Reply(session, serial, answer))
    1.55  
    1.56 -  private val manager = actor {
    1.57 +  private lazy val manager: Consumer_Thread[Any] =
    1.58 +  {
    1.59      var contexts = Map.empty[Document_ID.Command, Context]
    1.60  
    1.61      var memory_children = Map.empty[Long, Set[Long]]
    1.62 @@ -177,123 +184,121 @@
    1.63          "Simplifier_Trace.reply", Properties.Value.Long(serial), answer.name)
    1.64      }
    1.65  
    1.66 -    loop {
    1.67 -      react {
    1.68 -        case Handle_Results(session, id, results) =>
    1.69 -          var new_context = contexts.getOrElse(id, Context())
    1.70 -          var new_serial = new_context.last_serial
    1.71 +    Consumer_Thread.fork[Any]("Simplifier_Trace.manager", daemon = true)(
    1.72 +      consume = (arg: Any) =>
    1.73 +      {
    1.74 +        arg match {
    1.75 +          case Handle_Results(session, id, results, slot) =>
    1.76 +            var new_context = contexts.getOrElse(id, Context())
    1.77 +            var new_serial = new_context.last_serial
    1.78  
    1.79 -          for ((serial, result) <- results.iterator if serial > new_context.last_serial)
    1.80 -          {
    1.81 -            result match {
    1.82 -              case Item(markup, data) =>
    1.83 -                memory_children +=
    1.84 -                  (data.parent -> (memory_children.getOrElse(data.parent, Set.empty) + serial))
    1.85 -
    1.86 -                markup match {
    1.87 +            for ((serial, result) <- results.iterator if serial > new_context.last_serial)
    1.88 +            {
    1.89 +              result match {
    1.90 +                case Item(markup, data) =>
    1.91 +                  memory_children +=
    1.92 +                    (data.parent -> (memory_children.getOrElse(data.parent, Set.empty) + serial))
    1.93  
    1.94 -                  case Markup.SIMP_TRACE_STEP =>
    1.95 -                    val index = Index.of_data(data)
    1.96 -                    memory.get(index) match {
    1.97 -                      case Some(answer) if data.memory =>
    1.98 -                        do_reply(session, serial, answer)
    1.99 -                      case _ =>
   1.100 -                        new_context += Question(data, Answer.step.all, Answer.step.default)
   1.101 -                    }
   1.102 +                  markup match {
   1.103  
   1.104 -                  case Markup.SIMP_TRACE_HINT =>
   1.105 -                    data.props match {
   1.106 -                      case Success(false) =>
   1.107 -                        results.get(data.parent) match {
   1.108 -                          case Some(Item(Markup.SIMP_TRACE_STEP, _)) =>
   1.109 -                            new_context +=
   1.110 -                              Question(data, Answer.hint_fail.all, Answer.hint_fail.default)
   1.111 -                          case _ =>
   1.112 -                            // unknown, better send a default reply
   1.113 -                            do_reply(session, data.serial, Answer.hint_fail.default)
   1.114 -                        }
   1.115 -                      case _ =>
   1.116 -                    }
   1.117 +                    case Markup.SIMP_TRACE_STEP =>
   1.118 +                      val index = Index.of_data(data)
   1.119 +                      memory.get(index) match {
   1.120 +                        case Some(answer) if data.memory =>
   1.121 +                          do_reply(session, serial, answer)
   1.122 +                        case _ =>
   1.123 +                          new_context += Question(data, Answer.step.all, Answer.step.default)
   1.124 +                      }
   1.125  
   1.126 -                  case Markup.SIMP_TRACE_IGNORE =>
   1.127 -                    // At this point, we know that the parent of this 'IGNORE' entry is a 'STEP'
   1.128 -                    // entry, and that that 'STEP' entry is about to be replayed. Hence, we need
   1.129 -                    // to selectively purge the replies which have been memorized, going down from
   1.130 -                    // the parent to all leaves.
   1.131 -
   1.132 -                    @tailrec
   1.133 -                    def purge(queue: Vector[Long]): Unit =
   1.134 -                      queue match {
   1.135 -                        case s +: rest =>
   1.136 -                          for (Item(Markup.SIMP_TRACE_STEP, data) <- results.get(s))
   1.137 -                            memory -= Index.of_data(data)
   1.138 -                          val children = memory_children.getOrElse(s, Set.empty)
   1.139 -                          memory_children -= s
   1.140 -                          purge(rest ++ children.toVector)
   1.141 +                    case Markup.SIMP_TRACE_HINT =>
   1.142 +                      data.props match {
   1.143 +                        case Success(false) =>
   1.144 +                          results.get(data.parent) match {
   1.145 +                            case Some(Item(Markup.SIMP_TRACE_STEP, _)) =>
   1.146 +                              new_context +=
   1.147 +                                Question(data, Answer.hint_fail.all, Answer.hint_fail.default)
   1.148 +                            case _ =>
   1.149 +                              // unknown, better send a default reply
   1.150 +                              do_reply(session, data.serial, Answer.hint_fail.default)
   1.151 +                          }
   1.152                          case _ =>
   1.153                        }
   1.154  
   1.155 -                    purge(Vector(data.parent))
   1.156 +                    case Markup.SIMP_TRACE_IGNORE =>
   1.157 +                      // At this point, we know that the parent of this 'IGNORE' entry is a 'STEP'
   1.158 +                      // entry, and that that 'STEP' entry is about to be replayed. Hence, we need
   1.159 +                      // to selectively purge the replies which have been memorized, going down from
   1.160 +                      // the parent to all leaves.
   1.161  
   1.162 -                  case _ =>
   1.163 -                }
   1.164 +                      @tailrec
   1.165 +                      def purge(queue: Vector[Long]): Unit =
   1.166 +                        queue match {
   1.167 +                          case s +: rest =>
   1.168 +                            for (Item(Markup.SIMP_TRACE_STEP, data) <- results.get(s))
   1.169 +                              memory -= Index.of_data(data)
   1.170 +                            val children = memory_children.getOrElse(s, Set.empty)
   1.171 +                            memory_children -= s
   1.172 +                            purge(rest ++ children.toVector)
   1.173 +                          case _ =>
   1.174 +                        }
   1.175  
   1.176 -              case _ =>
   1.177 +                      purge(Vector(data.parent))
   1.178 +
   1.179 +                    case _ =>
   1.180 +                  }
   1.181 +
   1.182 +                case _ =>
   1.183 +              }
   1.184 +
   1.185 +              new_serial = serial
   1.186              }
   1.187  
   1.188 -            new_serial = serial
   1.189 -          }
   1.190 +            new_context = new_context.with_serial(new_serial)
   1.191 +            contexts += (id -> new_context)
   1.192 +            slot.fulfill(new_context)
   1.193  
   1.194 -          new_context = new_context.with_serial(new_serial)
   1.195 -          contexts += (id -> new_context)
   1.196 -          reply(new_context)
   1.197 -
   1.198 -        case Generate_Trace(results) =>
   1.199 -          // Since there are potentially lots of trace messages, we do not cache them here again.
   1.200 -          // Instead, everytime the trace is being requested, we re-assemble it based on the
   1.201 -          // current results.
   1.202 +          case Generate_Trace(results, slot) =>
   1.203 +            // Since there are potentially lots of trace messages, we do not cache them here again.
   1.204 +            // Instead, everytime the trace is being requested, we re-assemble it based on the
   1.205 +            // current results.
   1.206  
   1.207 -          val items =
   1.208 -            (for { (_, Item(_, data)) <- results.iterator }
   1.209 -              yield data).toList
   1.210 +            val items =
   1.211 +              (for { (_, Item(_, data)) <- results.iterator }
   1.212 +                yield data).toList
   1.213  
   1.214 -          reply(Trace(items))
   1.215 +            slot.fulfill(Trace(items))
   1.216  
   1.217 -        case Cancel(serial) =>
   1.218 -          find_question(serial) match {
   1.219 -            case Some((id, _)) =>
   1.220 -              do_cancel(serial, id)
   1.221 -            case None =>
   1.222 -          }
   1.223 +          case Cancel(serial) =>
   1.224 +            find_question(serial) match {
   1.225 +              case Some((id, _)) =>
   1.226 +                do_cancel(serial, id)
   1.227 +              case None =>
   1.228 +            }
   1.229  
   1.230 -        case Clear_Memory =>
   1.231 -          memory_children = Map.empty
   1.232 -          memory = Map.empty
   1.233 -
   1.234 -        case Stop =>
   1.235 -          contexts = Map.empty
   1.236 -          exit("Simplifier_Trace: manager actor stopped")
   1.237 +          case Clear_Memory =>
   1.238 +            memory_children = Map.empty
   1.239 +            memory = Map.empty
   1.240  
   1.241 -        case Reply(session, serial, answer) =>
   1.242 -          find_question(serial) match {
   1.243 -            case Some((id, Question(data, _, _))) =>
   1.244 -              if (data.markup == Markup.SIMP_TRACE_STEP && data.memory)
   1.245 -              {
   1.246 -                val index = Index.of_data(data)
   1.247 -                memory += (index -> answer)
   1.248 -              }
   1.249 -              do_cancel(serial, id)
   1.250 -            case None =>
   1.251 -              System.err.println("send_reply: unknown serial " + serial)
   1.252 -          }
   1.253 +          case Reply(session, serial, answer) =>
   1.254 +            find_question(serial) match {
   1.255 +              case Some((id, Question(data, _, _))) =>
   1.256 +                if (data.markup == Markup.SIMP_TRACE_STEP && data.memory)
   1.257 +                {
   1.258 +                  val index = Index.of_data(data)
   1.259 +                  memory += (index -> answer)
   1.260 +                }
   1.261 +                do_cancel(serial, id)
   1.262 +              case None =>
   1.263 +                System.err.println("send_reply: unknown serial " + serial)
   1.264 +            }
   1.265  
   1.266 -          do_reply(session, serial, answer)
   1.267 -          session.trace_events.post(Event)
   1.268 -
   1.269 -        case bad =>
   1.270 -          System.err.println("context_manager: bad message " + bad)
   1.271 -      }
   1.272 -    }
   1.273 +            do_reply(session, serial, answer)
   1.274 +            session.trace_events.post(Event)
   1.275 +        }
   1.276 +        true
   1.277 +      },
   1.278 +      finish = () => contexts = Map.empty
   1.279 +    )
   1.280    }
   1.281  
   1.282  
   1.283 @@ -301,10 +306,12 @@
   1.284  
   1.285    class Handler extends Session.Protocol_Handler
   1.286    {
   1.287 +    assert(manager.is_active)
   1.288 +
   1.289      private def cancel(prover: Prover, msg: Prover.Protocol_Output): Boolean =
   1.290        msg.properties match {
   1.291          case Markup.Simp_Trace_Cancel(serial) =>
   1.292 -          manager ! Cancel(serial)
   1.293 +          manager.send(Cancel(serial))
   1.294            true
   1.295          case _ =>
   1.296            false
   1.297 @@ -312,8 +319,8 @@
   1.298  
   1.299      override def stop(prover: Prover) =
   1.300      {
   1.301 -      manager ! Clear_Memory
   1.302 -      manager ! Stop
   1.303 +      manager.send(Clear_Memory)
   1.304 +      manager.shutdown()
   1.305      }
   1.306  
   1.307      val functions = Map(Markup.SIMP_TRACE_CANCEL -> cancel _)