src/Pure/System/session.scala
changeset 52111 1fd184eaa310
parent 52084 573e80625c78
child 52113 2d2b049429f3
     1.1 --- a/src/Pure/System/session.scala	Wed May 22 08:46:39 2013 +0200
     1.2 +++ b/src/Pure/System/session.scala	Wed May 22 14:10:45 2013 +0200
     1.3 @@ -37,6 +37,68 @@
     1.4    case object Ready extends Phase
     1.5    case object Shutdown extends Phase  // transient
     1.6    //}}}
     1.7 +
     1.8 +
     1.9 +  /* protocol handlers */
    1.10 +
    1.11 +  type Prover = Isabelle_Process with Protocol
    1.12 +
    1.13 +  abstract class Protocol_Handler
    1.14 +  {
    1.15 +    def stop(prover: Prover): Unit = {}
    1.16 +    val functions: Map[String, (Prover, Isabelle_Process.Output) => Boolean]
    1.17 +  }
    1.18 +
    1.19 +  class Protocol_Handlers(
    1.20 +    handlers: Map[String, Session.Protocol_Handler] = Map.empty,
    1.21 +    functions: Map[String, Isabelle_Process.Output => Boolean] = Map.empty)
    1.22 +  {
    1.23 +    def add(prover: Prover, name: String): Protocol_Handlers =
    1.24 +    {
    1.25 +      val (handlers1, functions1) =
    1.26 +        handlers.get(name) match {
    1.27 +          case Some(old_handler) =>
    1.28 +            System.err.println("Redefining protocol handler: " + name)
    1.29 +            old_handler.stop(prover)
    1.30 +            (handlers - name, functions -- old_handler.functions.keys)
    1.31 +          case None => (handlers, functions)
    1.32 +        }
    1.33 +
    1.34 +      val (handlers2, functions2) =
    1.35 +        try {
    1.36 +          val new_handler = Class.forName(name).newInstance.asInstanceOf[Protocol_Handler]
    1.37 +          val new_functions =
    1.38 +            for ((a, f) <- new_handler.functions.toList) yield
    1.39 +              (a, (output: Isabelle_Process.Output) => f(prover, output))
    1.40 +
    1.41 +          val dups = for ((a, _) <- new_functions if functions1.isDefinedAt(a)) yield a
    1.42 +          if (!dups.isEmpty) error("Duplicate protocol functions: " + commas_quote(dups))
    1.43 +
    1.44 +          (handlers1 + (name -> new_handler), functions1 ++ new_functions)
    1.45 +        }
    1.46 +        catch {
    1.47 +          case exn: Throwable =>
    1.48 +            System.err.println("Failed to initialize protocol handler: " +
    1.49 +              name + "\n" + Exn.message(exn))
    1.50 +            (handlers1, functions1)
    1.51 +        }
    1.52 +
    1.53 +      new Protocol_Handlers(handlers2, functions2)
    1.54 +    }
    1.55 +
    1.56 +    def invoke(output: Isabelle_Process.Output): Boolean =
    1.57 +      output.properties match {
    1.58 +        case Markup.Function(a) if functions.isDefinedAt(a) =>
    1.59 +          try { functions(a)(output) }
    1.60 +          catch {
    1.61 +            case exn: Throwable =>
    1.62 +              System.err.println("Failed invocation of protocol function: " +
    1.63 +                quote(a) + "\n" + Exn.message(exn))
    1.64 +            false
    1.65 +          }
    1.66 +        case _ => false
    1.67 +      }
    1.68 +  }
    1.69  }
    1.70  
    1.71  
    1.72 @@ -176,16 +238,15 @@
    1.73      previous: Document.Version,
    1.74      version: Document.Version)
    1.75    private case class Messages(msgs: List[Isabelle_Process.Message])
    1.76 -  private case class Finished_Scala(id: String, tag: Invoke_Scala.Tag.Value, result: String)
    1.77    private case class Update_Options(options: Options)
    1.78  
    1.79    private val (_, session_actor) = Simple_Thread.actor("session_actor", daemon = true)
    1.80    {
    1.81      val this_actor = self
    1.82  
    1.83 -    var prune_next = System.currentTimeMillis() + prune_delay.ms
    1.84 +    var protocol_handlers = new Session.Protocol_Handlers()
    1.85  
    1.86 -    var futures = Map.empty[String, java.util.concurrent.Future[Unit]]
    1.87 +    var prune_next = System.currentTimeMillis() + prune_delay.ms
    1.88  
    1.89  
    1.90      /* buffered prover messages */
    1.91 @@ -222,7 +283,7 @@
    1.92        def cancel() { timer.cancel() }
    1.93      }
    1.94  
    1.95 -    var prover: Option[Isabelle_Process with Protocol] = None
    1.96 +    var prover: Option[Session.Prover] = None
    1.97  
    1.98  
    1.99      /* delayed command changes */
   1.100 @@ -318,73 +379,68 @@
   1.101          }
   1.102        }
   1.103  
   1.104 -      output.properties match {
   1.105 +      if (output.is_protocol) {
   1.106 +        val handled = protocol_handlers.invoke(output)
   1.107 +        if (!handled) {
   1.108 +          output.properties match {
   1.109 +            case Markup.Protocol_Handler(name) =>
   1.110 +              protocol_handlers = protocol_handlers.add(prover.get, name)
   1.111  
   1.112 -        case Position.Id(state_id) if !output.is_protocol =>
   1.113 -          accumulate(state_id, output.message)
   1.114 -
   1.115 -        case Protocol.Command_Timing(state_id, timing) if output.is_protocol =>
   1.116 -          val message = XML.elem(Markup.STATUS, List(XML.Elem(Markup.Timing(timing), Nil)))
   1.117 -          accumulate(state_id, prover.get.xml_cache.elem(message))
   1.118 +            case Protocol.Command_Timing(state_id, timing) =>
   1.119 +              val message = XML.elem(Markup.STATUS, List(XML.Elem(Markup.Timing(timing), Nil)))
   1.120 +              accumulate(state_id, prover.get.xml_cache.elem(message))
   1.121  
   1.122 -        case Markup.Assign_Execs if output.is_protocol =>
   1.123 -          XML.content(output.body) match {
   1.124 -            case Protocol.Assign(id, assign) =>
   1.125 -              try {
   1.126 -                val cmds = global_state >>> (_.assign(id, assign))
   1.127 -                delay_commands_changed.invoke(true, cmds)
   1.128 +            case Markup.Assign_Execs =>
   1.129 +              XML.content(output.body) match {
   1.130 +                case Protocol.Assign(id, assign) =>
   1.131 +                  try {
   1.132 +                    val cmds = global_state >>> (_.assign(id, assign))
   1.133 +                    delay_commands_changed.invoke(true, cmds)
   1.134 +                  }
   1.135 +                  catch { case _: Document.State.Fail => bad_output() }
   1.136 +                case _ => bad_output()
   1.137 +              }
   1.138 +              // FIXME separate timeout event/message!?
   1.139 +              if (prover.isDefined && System.currentTimeMillis() > prune_next) {
   1.140 +                val old_versions = global_state >>> (_.prune_history(prune_size))
   1.141 +                if (!old_versions.isEmpty) prover.get.remove_versions(old_versions)
   1.142 +                prune_next = System.currentTimeMillis() + prune_delay.ms
   1.143                }
   1.144 -              catch { case _: Document.State.Fail => bad_output() }
   1.145 +
   1.146 +            case Markup.Removed_Versions =>
   1.147 +              XML.content(output.body) match {
   1.148 +                case Protocol.Removed(removed) =>
   1.149 +                  try {
   1.150 +                    global_state >> (_.removed_versions(removed))
   1.151 +                  }
   1.152 +                  catch { case _: Document.State.Fail => bad_output() }
   1.153 +                case _ => bad_output()
   1.154 +              }
   1.155 +
   1.156 +            case Markup.ML_Statistics(props) =>
   1.157 +              statistics.event(Session.Statistics(props))
   1.158 +
   1.159 +            case Markup.Task_Statistics(props) =>
   1.160 +              // FIXME
   1.161 +
   1.162              case _ => bad_output()
   1.163            }
   1.164 -          // FIXME separate timeout event/message!?
   1.165 -          if (prover.isDefined && System.currentTimeMillis() > prune_next) {
   1.166 -            val old_versions = global_state >>> (_.prune_history(prune_size))
   1.167 -            if (!old_versions.isEmpty) prover.get.remove_versions(old_versions)
   1.168 -            prune_next = System.currentTimeMillis() + prune_delay.ms
   1.169 -          }
   1.170 -
   1.171 -        case Markup.Removed_Versions if output.is_protocol =>
   1.172 -          XML.content(output.body) match {
   1.173 -            case Protocol.Removed(removed) =>
   1.174 -              try {
   1.175 -                global_state >> (_.removed_versions(removed))
   1.176 -              }
   1.177 -              catch { case _: Document.State.Fail => bad_output() }
   1.178 -            case _ => bad_output()
   1.179 -          }
   1.180 +        }
   1.181 +      }
   1.182 +      else {
   1.183 +        output.properties match {
   1.184 +          case Position.Id(state_id) =>
   1.185 +            accumulate(state_id, output.message)
   1.186  
   1.187 -        case Markup.Invoke_Scala(name, id) if output.is_protocol =>
   1.188 -          futures += (id ->
   1.189 -            default_thread_pool.submit(() =>
   1.190 -              {
   1.191 -                val arg = XML.content(output.body)
   1.192 -                val (tag, result) = Invoke_Scala.method(name, arg)
   1.193 -                this_actor ! Finished_Scala(id, tag, result)
   1.194 -              }))
   1.195 +          case _ if output.is_init =>
   1.196 +            phase = Session.Ready
   1.197  
   1.198 -        case Markup.Cancel_Scala(id) if output.is_protocol =>
   1.199 -          futures.get(id) match {
   1.200 -            case Some(future) =>
   1.201 -              future.cancel(true)
   1.202 -              this_actor ! Finished_Scala(id, Invoke_Scala.Tag.INTERRUPT, "")
   1.203 -            case None =>
   1.204 -          }
   1.205 -
   1.206 -        case Markup.ML_Statistics(props) if output.is_protocol =>
   1.207 -          statistics.event(Session.Statistics(props))
   1.208 +          case Markup.Return_Code(rc) if output.is_exit =>
   1.209 +            if (rc == 0) phase = Session.Inactive
   1.210 +            else phase = Session.Failed
   1.211  
   1.212 -        case Markup.Task_Statistics(props) if output.is_protocol =>
   1.213 -          // FIXME
   1.214 -
   1.215 -        case _ if output.is_init =>
   1.216 -          phase = Session.Ready
   1.217 -
   1.218 -        case Markup.Return_Code(rc) if output.is_exit =>
   1.219 -          if (rc == 0) phase = Session.Inactive
   1.220 -          else phase = Session.Failed
   1.221 -
   1.222 -        case _ => bad_output()
   1.223 +          case _ => bad_output()
   1.224 +        }
   1.225        }
   1.226      }
   1.227      //}}}
   1.228 @@ -455,12 +511,6 @@
   1.229          if prover.isDefined && global_state().is_assigned(change.previous) =>
   1.230            handle_change(change)
   1.231  
   1.232 -        case Finished_Scala(id, tag, result) if prover.isDefined =>
   1.233 -          if (futures.isDefinedAt(id)) {
   1.234 -            prover.get.invoke_scala(id, tag, result)
   1.235 -            futures -= id
   1.236 -          }
   1.237 -
   1.238          case bad if !bad.isInstanceOf[Change] =>
   1.239            System.err.println("session_actor: ignoring bad message " + bad)
   1.240        }