clarified module arrangement;
authorwenzelm
Tue Mar 18 18:09:31 2014 +0100 (2014-03-18)
changeset 56210c7c85cdb725d
parent 56209 3c89e21d9be2
child 56211 3250d70c8d0b
clarified module arrangement;
src/Pure/PIDE/session.ML
src/Pure/PIDE/session.scala
src/Pure/ROOT
src/Pure/ROOT.ML
src/Pure/System/session.ML
src/Pure/System/session.scala
src/Pure/build-jars
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/PIDE/session.ML	Tue Mar 18 18:09:31 2014 +0100
     1.3 @@ -0,0 +1,80 @@
     1.4 +(*  Title:      Pure/PIDE/session.ML
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +Prover session: persistent state of logic image.
     1.8 +*)
     1.9 +
    1.10 +signature SESSION =
    1.11 +sig
    1.12 +  val name: unit -> string
    1.13 +  val welcome: unit -> string
    1.14 +  val init: bool -> bool -> Path.T -> string -> bool -> string -> (string * string) list ->
    1.15 +    string -> string * string -> bool * string -> bool -> unit
    1.16 +  val finish: unit -> unit
    1.17 +  val protocol_handler: string -> unit
    1.18 +  val init_protocol_handlers: unit -> unit
    1.19 +end;
    1.20 +
    1.21 +structure Session: SESSION =
    1.22 +struct
    1.23 +
    1.24 +(** session identification -- not thread-safe **)
    1.25 +
    1.26 +val session = Unsynchronized.ref {chapter = "Pure", name = "Pure"};
    1.27 +val session_finished = Unsynchronized.ref false;
    1.28 +
    1.29 +fun name () = "Isabelle/" ^ #name (! session);
    1.30 +
    1.31 +fun welcome () =
    1.32 +  if Distribution.is_official then
    1.33 +    "Welcome to " ^ name () ^ " (" ^ Distribution.version ^ ")"
    1.34 +  else "Unofficial version of " ^ name () ^ " (" ^ Distribution.version ^ ")";
    1.35 +
    1.36 +
    1.37 +(* init *)
    1.38 +
    1.39 +fun init build info info_path doc doc_graph doc_output doc_variants
    1.40 +    parent (chapter, name) doc_dump verbose =
    1.41 +  if #name (! session) <> parent orelse not (! session_finished) then
    1.42 +    error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name)
    1.43 +  else
    1.44 +    let
    1.45 +      val _ = session := {chapter = chapter, name = name};
    1.46 +      val _ = session_finished := false;
    1.47 +    in
    1.48 +      Present.init build info info_path (if doc = "false" then "" else doc)
    1.49 +        doc_graph doc_output doc_variants (chapter, name)
    1.50 +        doc_dump verbose (map Thy_Info.get_theory (Thy_Info.get_names ()))
    1.51 +    end;
    1.52 +
    1.53 +
    1.54 +(* finish *)
    1.55 +
    1.56 +fun finish () =
    1.57 + (Execution.shutdown ();
    1.58 +  Thy_Info.finish ();
    1.59 +  Present.finish ();
    1.60 +  Outer_Syntax.check_syntax ();
    1.61 +  Future.shutdown ();
    1.62 +  Event_Timer.shutdown ();
    1.63 +  Future.shutdown ();
    1.64 +  session_finished := true);
    1.65 +
    1.66 +
    1.67 +
    1.68 +(** protocol handlers **)
    1.69 +
    1.70 +val protocol_handlers = Synchronized.var "protocol_handlers" ([]: string list);
    1.71 +
    1.72 +fun protocol_handler name =
    1.73 +  Synchronized.change protocol_handlers (fn handlers =>
    1.74 +   (Output.try_protocol_message (Markup.protocol_handler name) "";
    1.75 +    if not (member (op =) handlers name) then ()
    1.76 +    else warning ("Redefining protocol handler: " ^ quote name);
    1.77 +    update (op =) name handlers));
    1.78 +
    1.79 +fun init_protocol_handlers () =
    1.80 +  Synchronized.value protocol_handlers
    1.81 +  |> List.app (fn name => Output.try_protocol_message (Markup.protocol_handler name) "");
    1.82 +
    1.83 +end;
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Pure/PIDE/session.scala	Tue Mar 18 18:09:31 2014 +0100
     2.3 @@ -0,0 +1,598 @@
     2.4 +/*  Title:      Pure/PIDE/session.scala
     2.5 +    Author:     Makarius
     2.6 +    Options:    :folding=explicit:collapseFolds=1:
     2.7 +
     2.8 +PIDE editor session, potentially with running prover process.
     2.9 +*/
    2.10 +
    2.11 +package isabelle
    2.12 +
    2.13 +
    2.14 +import java.util.{Timer, TimerTask}
    2.15 +
    2.16 +import scala.collection.mutable
    2.17 +import scala.collection.immutable.Queue
    2.18 +import scala.actors.TIMEOUT
    2.19 +import scala.actors.Actor._
    2.20 +
    2.21 +
    2.22 +object Session
    2.23 +{
    2.24 +  /* events */
    2.25 +
    2.26 +  //{{{
    2.27 +  case class Statistics(props: Properties.T)
    2.28 +  case class Global_Options(options: Options)
    2.29 +  case object Caret_Focus
    2.30 +  case class Raw_Edits(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text])
    2.31 +  case class Dialog_Result(id: Document_ID.Generic, serial: Long, result: String)
    2.32 +  case class Commands_Changed(
    2.33 +    assignment: Boolean, nodes: Set[Document.Node.Name], commands: Set[Command])
    2.34 +
    2.35 +  sealed abstract class Phase
    2.36 +  case object Inactive extends Phase
    2.37 +  case object Startup extends Phase  // transient
    2.38 +  case object Failed extends Phase
    2.39 +  case object Ready extends Phase
    2.40 +  case object Shutdown extends Phase  // transient
    2.41 +  //}}}
    2.42 +
    2.43 +
    2.44 +  /* protocol handlers */
    2.45 +
    2.46 +  type Prover = Isabelle_Process with Protocol
    2.47 +
    2.48 +  abstract class Protocol_Handler
    2.49 +  {
    2.50 +    def stop(prover: Prover): Unit = {}
    2.51 +    val functions: Map[String, (Prover, Isabelle_Process.Protocol_Output) => Boolean]
    2.52 +  }
    2.53 +
    2.54 +  class Protocol_Handlers(
    2.55 +    handlers: Map[String, Session.Protocol_Handler] = Map.empty,
    2.56 +    functions: Map[String, Isabelle_Process.Protocol_Output => Boolean] = Map.empty)
    2.57 +  {
    2.58 +    def get(name: String): Option[Protocol_Handler] = handlers.get(name)
    2.59 +
    2.60 +    def add(prover: Prover, name: String): Protocol_Handlers =
    2.61 +    {
    2.62 +      val (handlers1, functions1) =
    2.63 +        handlers.get(name) match {
    2.64 +          case Some(old_handler) =>
    2.65 +            System.err.println("Redefining protocol handler: " + name)
    2.66 +            old_handler.stop(prover)
    2.67 +            (handlers - name, functions -- old_handler.functions.keys)
    2.68 +          case None => (handlers, functions)
    2.69 +        }
    2.70 +
    2.71 +      val (handlers2, functions2) =
    2.72 +        try {
    2.73 +          val new_handler = Class.forName(name).newInstance.asInstanceOf[Protocol_Handler]
    2.74 +          val new_functions =
    2.75 +            for ((a, f) <- new_handler.functions.toList) yield
    2.76 +              (a, (msg: Isabelle_Process.Protocol_Output) => f(prover, msg))
    2.77 +
    2.78 +          val dups = for ((a, _) <- new_functions if functions1.isDefinedAt(a)) yield a
    2.79 +          if (!dups.isEmpty) error("Duplicate protocol functions: " + commas_quote(dups))
    2.80 +
    2.81 +          (handlers1 + (name -> new_handler), functions1 ++ new_functions)
    2.82 +        }
    2.83 +        catch {
    2.84 +          case exn: Throwable =>
    2.85 +            System.err.println("Failed to initialize protocol handler: " +
    2.86 +              name + "\n" + Exn.message(exn))
    2.87 +            (handlers1, functions1)
    2.88 +        }
    2.89 +
    2.90 +      new Protocol_Handlers(handlers2, functions2)
    2.91 +    }
    2.92 +
    2.93 +    def invoke(msg: Isabelle_Process.Protocol_Output): Boolean =
    2.94 +      msg.properties match {
    2.95 +        case Markup.Function(a) if functions.isDefinedAt(a) =>
    2.96 +          try { functions(a)(msg) }
    2.97 +          catch {
    2.98 +            case exn: Throwable =>
    2.99 +              System.err.println("Failed invocation of protocol function: " +
   2.100 +                quote(a) + "\n" + Exn.message(exn))
   2.101 +            false
   2.102 +          }
   2.103 +        case _ => false
   2.104 +      }
   2.105 +
   2.106 +    def stop(prover: Prover): Protocol_Handlers =
   2.107 +    {
   2.108 +      for ((_, handler) <- handlers) handler.stop(prover)
   2.109 +      new Protocol_Handlers()
   2.110 +    }
   2.111 +  }
   2.112 +}
   2.113 +
   2.114 +
   2.115 +class Session(val resources: Resources)
   2.116 +{
   2.117 +  /* global flags */
   2.118 +
   2.119 +  @volatile var timing: Boolean = false
   2.120 +  @volatile var verbose: Boolean = false
   2.121 +
   2.122 +
   2.123 +  /* tuning parameters */
   2.124 +
   2.125 +  def output_delay: Time = Time.seconds(0.1)  // prover output (markup, common messages)
   2.126 +  def message_delay: Time = Time.seconds(0.1)  // prover input/output messages
   2.127 +  def prune_delay: Time = Time.seconds(60.0)  // prune history -- delete old versions
   2.128 +  def prune_size: Int = 0  // size of retained history
   2.129 +  def syslog_limit: Int = 100
   2.130 +  def reparse_limit: Int = 0
   2.131 +
   2.132 +
   2.133 +  /* pervasive event buses */
   2.134 +
   2.135 +  val statistics = new Event_Bus[Session.Statistics]
   2.136 +  val global_options = new Event_Bus[Session.Global_Options]
   2.137 +  val caret_focus = new Event_Bus[Session.Caret_Focus.type]
   2.138 +  val raw_edits = new Event_Bus[Session.Raw_Edits]
   2.139 +  val commands_changed = new Event_Bus[Session.Commands_Changed]
   2.140 +  val phase_changed = new Event_Bus[Session.Phase]
   2.141 +  val syslog_messages = new Event_Bus[Isabelle_Process.Output]
   2.142 +  val raw_output_messages = new Event_Bus[Isabelle_Process.Output]
   2.143 +  val all_messages = new Event_Bus[Isabelle_Process.Message]  // potential bottle-neck
   2.144 +  val trace_events = new Event_Bus[Simplifier_Trace.Event.type]
   2.145 +
   2.146 +
   2.147 +  /** buffered command changes (delay_first discipline) **/
   2.148 +
   2.149 +  //{{{
   2.150 +  private case object Stop
   2.151 +
   2.152 +  private val (_, commands_changed_buffer) =
   2.153 +    Simple_Thread.actor("commands_changed_buffer", daemon = true)
   2.154 +  {
   2.155 +    var finished = false
   2.156 +    while (!finished) {
   2.157 +      receive {
   2.158 +        case Stop => finished = true; reply(())
   2.159 +        case changed: Session.Commands_Changed => commands_changed.event(changed)
   2.160 +        case bad => System.err.println("commands_changed_buffer: ignoring bad message " + bad)
   2.161 +      }
   2.162 +    }
   2.163 +  }
   2.164 +  //}}}
   2.165 +
   2.166 +
   2.167 +  /** pipelined change parsing **/
   2.168 +
   2.169 +  //{{{
   2.170 +  private case class Text_Edits(
   2.171 +    previous: Future[Document.Version],
   2.172 +    doc_blobs: Document.Blobs,
   2.173 +    text_edits: List[Document.Edit_Text],
   2.174 +    version_result: Promise[Document.Version])
   2.175 +
   2.176 +  private val (_, change_parser) = Simple_Thread.actor("change_parser", daemon = true)
   2.177 +  {
   2.178 +    var finished = false
   2.179 +    while (!finished) {
   2.180 +      receive {
   2.181 +        case Stop => finished = true; reply(())
   2.182 +
   2.183 +        case Text_Edits(previous, doc_blobs, text_edits, version_result) =>
   2.184 +          val prev = previous.get_finished
   2.185 +          val (syntax_changed, doc_edits, version) =
   2.186 +            Timing.timeit("text_edits", timing) {
   2.187 +              resources.text_edits(reparse_limit, prev, doc_blobs, text_edits)
   2.188 +            }
   2.189 +          version_result.fulfill(version)
   2.190 +          sender ! Change(doc_blobs, syntax_changed, doc_edits, prev, version)
   2.191 +
   2.192 +        case bad => System.err.println("change_parser: ignoring bad message " + bad)
   2.193 +      }
   2.194 +    }
   2.195 +  }
   2.196 +  //}}}
   2.197 +
   2.198 +
   2.199 +
   2.200 +  /** main protocol actor **/
   2.201 +
   2.202 +  /* global state */
   2.203 +
   2.204 +  private val syslog = Volatile(Queue.empty[XML.Elem])
   2.205 +  def current_syslog(): String = cat_lines(syslog().iterator.map(XML.content))
   2.206 +
   2.207 +  @volatile private var _phase: Session.Phase = Session.Inactive
   2.208 +  private def phase_=(new_phase: Session.Phase)
   2.209 +  {
   2.210 +    _phase = new_phase
   2.211 +    phase_changed.event(new_phase)
   2.212 +  }
   2.213 +  def phase = _phase
   2.214 +  def is_ready: Boolean = phase == Session.Ready
   2.215 +
   2.216 +  private val global_state = Volatile(Document.State.init)
   2.217 +  def current_state(): Document.State = global_state()
   2.218 +
   2.219 +  def recent_syntax(): Outer_Syntax =
   2.220 +  {
   2.221 +    val version = current_state().recent_finished.version.get_finished
   2.222 +    if (version.is_init) resources.base_syntax
   2.223 +    else version.syntax
   2.224 +  }
   2.225 +
   2.226 +  def snapshot(name: Document.Node.Name = Document.Node.Name.empty,
   2.227 +      pending_edits: List[Text.Edit] = Nil): Document.Snapshot =
   2.228 +    global_state().snapshot(name, pending_edits)
   2.229 +
   2.230 +
   2.231 +  /* protocol handlers */
   2.232 +
   2.233 +  @volatile private var _protocol_handlers = new Session.Protocol_Handlers()
   2.234 +
   2.235 +  def protocol_handler(name: String): Option[Session.Protocol_Handler] =
   2.236 +    _protocol_handlers.get(name)
   2.237 +
   2.238 +
   2.239 +  /* theory files */
   2.240 +
   2.241 +  def header_edit(name: Document.Node.Name, header: Document.Node.Header): Document.Edit_Text =
   2.242 +  {
   2.243 +    val header1 =
   2.244 +      if (resources.loaded_theories(name.theory))
   2.245 +        header.error("Cannot update finished theory " + quote(name.theory))
   2.246 +      else header
   2.247 +    (name, Document.Node.Deps(header1))
   2.248 +  }
   2.249 +
   2.250 +
   2.251 +  /* actor messages */
   2.252 +
   2.253 +  private case class Start(args: List[String])
   2.254 +  private case class Cancel_Exec(exec_id: Document_ID.Exec)
   2.255 +  private case class Change(
   2.256 +    doc_blobs: Document.Blobs,
   2.257 +    syntax_changed: Boolean,
   2.258 +    doc_edits: List[Document.Edit_Command],
   2.259 +    previous: Document.Version,
   2.260 +    version: Document.Version)
   2.261 +  private case class Protocol_Command(name: String, args: List[String])
   2.262 +  private case class Messages(msgs: List[Isabelle_Process.Message])
   2.263 +  private case class Update_Options(options: Options)
   2.264 +
   2.265 +  private val (_, session_actor) = Simple_Thread.actor("session_actor", daemon = true)
   2.266 +  {
   2.267 +    val this_actor = self
   2.268 +
   2.269 +    var prune_next = System.currentTimeMillis() + prune_delay.ms
   2.270 +
   2.271 +
   2.272 +    /* buffered prover messages */
   2.273 +
   2.274 +    object receiver
   2.275 +    {
   2.276 +      private var buffer = new mutable.ListBuffer[Isabelle_Process.Message]
   2.277 +
   2.278 +      private def flush(): Unit = synchronized {
   2.279 +        if (!buffer.isEmpty) {
   2.280 +          val msgs = buffer.toList
   2.281 +          this_actor ! Messages(msgs)
   2.282 +          buffer = new mutable.ListBuffer[Isabelle_Process.Message]
   2.283 +        }
   2.284 +      }
   2.285 +      def invoke(msg: Isabelle_Process.Message): Unit = synchronized {
   2.286 +        msg match {
   2.287 +          case _: Isabelle_Process.Input =>
   2.288 +            buffer += msg
   2.289 +          case output: Isabelle_Process.Protocol_Output if output.properties == Markup.Flush =>
   2.290 +            flush()
   2.291 +          case output: Isabelle_Process.Output =>
   2.292 +            buffer += msg
   2.293 +            if (output.is_syslog)
   2.294 +              syslog >> (queue =>
   2.295 +                {
   2.296 +                  val queue1 = queue.enqueue(output.message)
   2.297 +                  if (queue1.length > syslog_limit) queue1.dequeue._2 else queue1
   2.298 +                })
   2.299 +        }
   2.300 +      }
   2.301 +
   2.302 +      private val timer = new Timer("session_actor.receiver", true)
   2.303 +      timer.schedule(new TimerTask { def run = flush }, message_delay.ms, message_delay.ms)
   2.304 +
   2.305 +      def cancel() { timer.cancel() }
   2.306 +    }
   2.307 +
   2.308 +    var prover: Option[Session.Prover] = None
   2.309 +
   2.310 +
   2.311 +    /* delayed command changes */
   2.312 +
   2.313 +    object delay_commands_changed
   2.314 +    {
   2.315 +      private var changed_assignment: Boolean = false
   2.316 +      private var changed_nodes: Set[Document.Node.Name] = Set.empty
   2.317 +      private var changed_commands: Set[Command] = Set.empty
   2.318 +
   2.319 +      private var flush_time: Option[Long] = None
   2.320 +
   2.321 +      def flush_timeout: Long =
   2.322 +        flush_time match {
   2.323 +          case None => 5000L
   2.324 +          case Some(time) => (time - System.currentTimeMillis()) max 0
   2.325 +        }
   2.326 +
   2.327 +      def flush()
   2.328 +      {
   2.329 +        if (changed_assignment || !changed_nodes.isEmpty || !changed_commands.isEmpty)
   2.330 +          commands_changed_buffer !
   2.331 +            Session.Commands_Changed(changed_assignment, changed_nodes, changed_commands)
   2.332 +        changed_assignment = false
   2.333 +        changed_nodes = Set.empty
   2.334 +        changed_commands = Set.empty
   2.335 +        flush_time = None
   2.336 +      }
   2.337 +
   2.338 +      def invoke(assign: Boolean, commands: List[Command])
   2.339 +      {
   2.340 +        changed_assignment |= assign
   2.341 +        for (command <- commands) {
   2.342 +          changed_nodes += command.node_name
   2.343 +          changed_commands += command
   2.344 +        }
   2.345 +        val now = System.currentTimeMillis()
   2.346 +        flush_time match {
   2.347 +          case None => flush_time = Some(now + output_delay.ms)
   2.348 +          case Some(time) => if (now >= time) flush()
   2.349 +        }
   2.350 +      }
   2.351 +    }
   2.352 +
   2.353 +
   2.354 +    /* raw edits */
   2.355 +
   2.356 +    def handle_raw_edits(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text])
   2.357 +    //{{{
   2.358 +    {
   2.359 +      prover.get.discontinue_execution()
   2.360 +
   2.361 +      val previous = global_state().history.tip.version
   2.362 +      val version = Future.promise[Document.Version]
   2.363 +      val change = global_state >>> (_.continue_history(previous, edits, version))
   2.364 +
   2.365 +      raw_edits.event(Session.Raw_Edits(doc_blobs, edits))
   2.366 +      change_parser ! Text_Edits(previous, doc_blobs, edits, version)
   2.367 +    }
   2.368 +    //}}}
   2.369 +
   2.370 +
   2.371 +    /* resulting changes */
   2.372 +
   2.373 +    def handle_change(change: Change)
   2.374 +    //{{{
   2.375 +    {
   2.376 +      val Change(doc_blobs, syntax_changed, doc_edits, previous, version) = change
   2.377 +
   2.378 +      def id_command(command: Command)
   2.379 +      {
   2.380 +        for {
   2.381 +          digest <- command.blobs_digests
   2.382 +          if !global_state().defined_blob(digest)
   2.383 +        } {
   2.384 +          doc_blobs.get(digest) match {
   2.385 +            case Some(blob) =>
   2.386 +              global_state >> (_.define_blob(digest))
   2.387 +              prover.get.define_blob(blob)
   2.388 +            case None =>
   2.389 +              System.err.println("Missing blob for SHA1 digest " + digest)
   2.390 +          }
   2.391 +        }
   2.392 +
   2.393 +        if (!global_state().defined_command(command.id)) {
   2.394 +          global_state >> (_.define_command(command))
   2.395 +          prover.get.define_command(command)
   2.396 +        }
   2.397 +      }
   2.398 +      doc_edits foreach {
   2.399 +        case (_, edit) =>
   2.400 +          edit foreach { case (c1, c2) => c1 foreach id_command; c2 foreach id_command }
   2.401 +      }
   2.402 +
   2.403 +      val assignment = global_state().the_assignment(previous).check_finished
   2.404 +      global_state >> (_.define_version(version, assignment))
   2.405 +      prover.get.update(previous.id, version.id, doc_edits)
   2.406 +
   2.407 +      if (syntax_changed) resources.syntax_changed()
   2.408 +    }
   2.409 +    //}}}
   2.410 +
   2.411 +
   2.412 +    /* prover output */
   2.413 +
   2.414 +    def handle_output(output: Isabelle_Process.Output)
   2.415 +    //{{{
   2.416 +    {
   2.417 +      def bad_output()
   2.418 +      {
   2.419 +        if (verbose)
   2.420 +          System.err.println("Ignoring prover output: " + output.message.toString)
   2.421 +      }
   2.422 +
   2.423 +      def accumulate(state_id: Document_ID.Generic, message: XML.Elem)
   2.424 +      {
   2.425 +        try {
   2.426 +          val st = global_state >>> (_.accumulate(state_id, message))
   2.427 +          delay_commands_changed.invoke(false, List(st.command))
   2.428 +        }
   2.429 +        catch {
   2.430 +          case _: Document.State.Fail => bad_output()
   2.431 +        }
   2.432 +      }
   2.433 +
   2.434 +      output match {
   2.435 +        case msg: Isabelle_Process.Protocol_Output =>
   2.436 +          val handled = _protocol_handlers.invoke(msg)
   2.437 +          if (!handled) {
   2.438 +            msg.properties match {
   2.439 +              case Markup.Protocol_Handler(name) =>
   2.440 +                _protocol_handlers = _protocol_handlers.add(prover.get, name)
   2.441 +
   2.442 +              case Protocol.Command_Timing(state_id, timing) =>
   2.443 +                val message = XML.elem(Markup.STATUS, List(XML.Elem(Markup.Timing(timing), Nil)))
   2.444 +                accumulate(state_id, prover.get.xml_cache.elem(message))
   2.445 +
   2.446 +              case Markup.Assign_Update =>
   2.447 +                msg.text match {
   2.448 +                  case Protocol.Assign_Update(id, update) =>
   2.449 +                    try {
   2.450 +                      val cmds = global_state >>> (_.assign(id, update))
   2.451 +                      delay_commands_changed.invoke(true, cmds)
   2.452 +                    }
   2.453 +                    catch { case _: Document.State.Fail => bad_output() }
   2.454 +                  case _ => bad_output()
   2.455 +                }
   2.456 +                // FIXME separate timeout event/message!?
   2.457 +                if (prover.isDefined && System.currentTimeMillis() > prune_next) {
   2.458 +                  val old_versions = global_state >>> (_.prune_history(prune_size))
   2.459 +                  if (!old_versions.isEmpty) prover.get.remove_versions(old_versions)
   2.460 +                  prune_next = System.currentTimeMillis() + prune_delay.ms
   2.461 +                }
   2.462 +
   2.463 +              case Markup.Removed_Versions =>
   2.464 +                msg.text match {
   2.465 +                  case Protocol.Removed(removed) =>
   2.466 +                    try {
   2.467 +                      global_state >> (_.removed_versions(removed))
   2.468 +                    }
   2.469 +                    catch { case _: Document.State.Fail => bad_output() }
   2.470 +                  case _ => bad_output()
   2.471 +                }
   2.472 +
   2.473 +              case Markup.ML_Statistics(props) =>
   2.474 +                statistics.event(Session.Statistics(props))
   2.475 +
   2.476 +              case Markup.Task_Statistics(props) =>
   2.477 +                // FIXME
   2.478 +
   2.479 +              case _ => bad_output()
   2.480 +            }
   2.481 +          }
   2.482 +        case _ =>
   2.483 +          output.properties match {
   2.484 +            case Position.Id(state_id) =>
   2.485 +              accumulate(state_id, output.message)
   2.486 +
   2.487 +            case _ if output.is_init =>
   2.488 +              phase = Session.Ready
   2.489 +
   2.490 +            case Markup.Return_Code(rc) if output.is_exit =>
   2.491 +              if (rc == 0) phase = Session.Inactive
   2.492 +              else phase = Session.Failed
   2.493 +
   2.494 +            case _ => raw_output_messages.event(output)
   2.495 +          }
   2.496 +        }
   2.497 +    }
   2.498 +    //}}}
   2.499 +
   2.500 +
   2.501 +    /* main loop */
   2.502 +
   2.503 +    //{{{
   2.504 +    var finished = false
   2.505 +    while (!finished) {
   2.506 +      receiveWithin(delay_commands_changed.flush_timeout) {
   2.507 +        case TIMEOUT => delay_commands_changed.flush()
   2.508 +
   2.509 +        case Start(args) if prover.isEmpty =>
   2.510 +          if (phase == Session.Inactive || phase == Session.Failed) {
   2.511 +            phase = Session.Startup
   2.512 +            prover = Some(new Isabelle_Process(receiver.invoke _, args) with Protocol)
   2.513 +          }
   2.514 +
   2.515 +        case Stop =>
   2.516 +          if (phase == Session.Ready) {
   2.517 +            _protocol_handlers = _protocol_handlers.stop(prover.get)
   2.518 +            global_state >> (_ => Document.State.init)  // FIXME event bus!?
   2.519 +            phase = Session.Shutdown
   2.520 +            prover.get.terminate
   2.521 +            prover = None
   2.522 +            phase = Session.Inactive
   2.523 +          }
   2.524 +          finished = true
   2.525 +          receiver.cancel()
   2.526 +          reply(())
   2.527 +
   2.528 +        case Update_Options(options) if prover.isDefined =>
   2.529 +          if (is_ready) {
   2.530 +            prover.get.options(options)
   2.531 +            handle_raw_edits(Document.Blobs.empty, Nil)
   2.532 +          }
   2.533 +          global_options.event(Session.Global_Options(options))
   2.534 +          reply(())
   2.535 +
   2.536 +        case Cancel_Exec(exec_id) if prover.isDefined =>
   2.537 +          prover.get.cancel_exec(exec_id)
   2.538 +
   2.539 +        case Session.Raw_Edits(doc_blobs, edits) if prover.isDefined =>
   2.540 +          handle_raw_edits(doc_blobs, edits)
   2.541 +          reply(())
   2.542 +
   2.543 +        case Session.Dialog_Result(id, serial, result) if prover.isDefined =>
   2.544 +          prover.get.dialog_result(serial, result)
   2.545 +          handle_output(new Isabelle_Process.Output(Protocol.Dialog_Result(id, serial, result)))
   2.546 +
   2.547 +        case Protocol_Command(name, args) if prover.isDefined =>
   2.548 +          prover.get.protocol_command(name, args:_*)
   2.549 +
   2.550 +        case Messages(msgs) =>
   2.551 +          msgs foreach {
   2.552 +            case input: Isabelle_Process.Input =>
   2.553 +              all_messages.event(input)
   2.554 +
   2.555 +            case output: Isabelle_Process.Output =>
   2.556 +              if (output.is_stdout || output.is_stderr) raw_output_messages.event(output)
   2.557 +              else handle_output(output)
   2.558 +              if (output.is_syslog) syslog_messages.event(output)
   2.559 +              all_messages.event(output)
   2.560 +          }
   2.561 +
   2.562 +        case change: Change
   2.563 +        if prover.isDefined && global_state().is_assigned(change.previous) =>
   2.564 +          handle_change(change)
   2.565 +
   2.566 +        case bad if !bad.isInstanceOf[Change] =>
   2.567 +          System.err.println("session_actor: ignoring bad message " + bad)
   2.568 +      }
   2.569 +    }
   2.570 +    //}}}
   2.571 +  }
   2.572 +
   2.573 +
   2.574 +  /* actions */
   2.575 +
   2.576 +  def start(args: List[String])
   2.577 +  {
   2.578 +    session_actor ! Start(args)
   2.579 +  }
   2.580 +
   2.581 +  def stop()
   2.582 +  {
   2.583 +    commands_changed_buffer !? Stop
   2.584 +    change_parser !? Stop
   2.585 +    session_actor !? Stop
   2.586 +  }
   2.587 +
   2.588 +  def protocol_command(name: String, args: String*)
   2.589 +  { session_actor ! Protocol_Command(name, args.toList) }
   2.590 +
   2.591 +  def cancel_exec(exec_id: Document_ID.Exec) { session_actor ! Cancel_Exec(exec_id) }
   2.592 +
   2.593 +  def update(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text])
   2.594 +  { if (!edits.isEmpty) session_actor !? Session.Raw_Edits(doc_blobs, edits) }
   2.595 +
   2.596 +  def update_options(options: Options)
   2.597 +  { session_actor !? Update_Options(options) }
   2.598 +
   2.599 +  def dialog_result(id: Document_ID.Generic, serial: Long, result: String)
   2.600 +  { session_actor ! Session.Dialog_Result(id, serial, result) }
   2.601 +}
     3.1 --- a/src/Pure/ROOT	Tue Mar 18 17:53:40 2014 +0100
     3.2 +++ b/src/Pure/ROOT	Tue Mar 18 18:09:31 2014 +0100
     3.3 @@ -162,6 +162,7 @@
     3.4      "PIDE/protocol.ML"
     3.5      "PIDE/query_operation.ML"
     3.6      "PIDE/resources.ML"
     3.7 +    "PIDE/session.ML"
     3.8      "PIDE/xml.ML"
     3.9      "PIDE/yxml.ML"
    3.10      "Proof/extraction.ML"
    3.11 @@ -190,7 +191,6 @@
    3.12      "System/isar.ML"
    3.13      "System/message_channel.ML"
    3.14      "System/options.ML"
    3.15 -    "System/session.ML"
    3.16      "System/system_channel.ML"
    3.17      "Thy/html.ML"
    3.18      "Thy/latex.ML"
     4.1 --- a/src/Pure/ROOT.ML	Tue Mar 18 17:53:40 2014 +0100
     4.2 +++ b/src/Pure/ROOT.ML	Tue Mar 18 18:09:31 2014 +0100
     4.3 @@ -294,7 +294,7 @@
     4.4  
     4.5  (* Isabelle/Isar system *)
     4.6  
     4.7 -use "System/session.ML";
     4.8 +use "PIDE/session.ML";
     4.9  use "System/command_line.ML";
    4.10  use "System/system_channel.ML";
    4.11  use "System/message_channel.ML";
     5.1 --- a/src/Pure/System/session.ML	Tue Mar 18 17:53:40 2014 +0100
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,79 +0,0 @@
     5.4 -(*  Title:      Pure/System/session.ML
     5.5 -    Author:     Makarius
     5.6 -
     5.7 -Session management -- internal state of logic images.
     5.8 -*)
     5.9 -
    5.10 -signature SESSION =
    5.11 -sig
    5.12 -  val name: unit -> string
    5.13 -  val welcome: unit -> string
    5.14 -  val init: bool -> bool -> Path.T -> string -> bool -> string -> (string * string) list ->
    5.15 -    string -> string * string -> bool * string -> bool -> unit
    5.16 -  val finish: unit -> unit
    5.17 -  val protocol_handler: string -> unit
    5.18 -  val init_protocol_handlers: unit -> unit
    5.19 -end;
    5.20 -
    5.21 -structure Session: SESSION =
    5.22 -struct
    5.23 -
    5.24 -(** session identification -- not thread-safe **)
    5.25 -
    5.26 -val session = Unsynchronized.ref {chapter = "Pure", name = "Pure"};
    5.27 -val session_finished = Unsynchronized.ref false;
    5.28 -
    5.29 -fun name () = "Isabelle/" ^ #name (! session);
    5.30 -
    5.31 -fun welcome () =
    5.32 -  if Distribution.is_official then
    5.33 -    "Welcome to " ^ name () ^ " (" ^ Distribution.version ^ ")"
    5.34 -  else "Unofficial version of " ^ name () ^ " (" ^ Distribution.version ^ ")";
    5.35 -
    5.36 -
    5.37 -(* init *)
    5.38 -
    5.39 -fun init build info info_path doc doc_graph doc_output doc_variants
    5.40 -    parent (chapter, name) doc_dump verbose =
    5.41 -  if #name (! session) <> parent orelse not (! session_finished) then
    5.42 -    error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name)
    5.43 -  else
    5.44 -    let
    5.45 -      val _ = session := {chapter = chapter, name = name};
    5.46 -      val _ = session_finished := false;
    5.47 -    in
    5.48 -      Present.init build info info_path (if doc = "false" then "" else doc)
    5.49 -        doc_graph doc_output doc_variants (chapter, name)
    5.50 -        doc_dump verbose (map Thy_Info.get_theory (Thy_Info.get_names ()))
    5.51 -    end;
    5.52 -
    5.53 -
    5.54 -(* finish *)
    5.55 -
    5.56 -fun finish () =
    5.57 - (Execution.shutdown ();
    5.58 -  Thy_Info.finish ();
    5.59 -  Present.finish ();
    5.60 -  Outer_Syntax.check_syntax ();
    5.61 -  Future.shutdown ();
    5.62 -  Event_Timer.shutdown ();
    5.63 -  Future.shutdown ();
    5.64 -  session_finished := true);
    5.65 -
    5.66 -
    5.67 -(** protocol handlers **)
    5.68 -
    5.69 -val protocol_handlers = Synchronized.var "protocol_handlers" ([]: string list);
    5.70 -
    5.71 -fun protocol_handler name =
    5.72 -  Synchronized.change protocol_handlers (fn handlers =>
    5.73 -   (Output.try_protocol_message (Markup.protocol_handler name) "";
    5.74 -    if not (member (op =) handlers name) then ()
    5.75 -    else warning ("Redefining protocol handler: " ^ quote name);
    5.76 -    update (op =) name handlers));
    5.77 -
    5.78 -fun init_protocol_handlers () =
    5.79 -  Synchronized.value protocol_handlers
    5.80 -  |> List.app (fn name => Output.try_protocol_message (Markup.protocol_handler name) "");
    5.81 -
    5.82 -end;
     6.1 --- a/src/Pure/System/session.scala	Tue Mar 18 17:53:40 2014 +0100
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,598 +0,0 @@
     6.4 -/*  Title:      Pure/System/session.scala
     6.5 -    Author:     Makarius
     6.6 -    Options:    :folding=explicit:collapseFolds=1:
     6.7 -
     6.8 -Main Isabelle/Scala session, potentially with running prover process.
     6.9 -*/
    6.10 -
    6.11 -package isabelle
    6.12 -
    6.13 -
    6.14 -import java.util.{Timer, TimerTask}
    6.15 -
    6.16 -import scala.collection.mutable
    6.17 -import scala.collection.immutable.Queue
    6.18 -import scala.actors.TIMEOUT
    6.19 -import scala.actors.Actor._
    6.20 -
    6.21 -
    6.22 -object Session
    6.23 -{
    6.24 -  /* events */
    6.25 -
    6.26 -  //{{{
    6.27 -  case class Statistics(props: Properties.T)
    6.28 -  case class Global_Options(options: Options)
    6.29 -  case object Caret_Focus
    6.30 -  case class Raw_Edits(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text])
    6.31 -  case class Dialog_Result(id: Document_ID.Generic, serial: Long, result: String)
    6.32 -  case class Commands_Changed(
    6.33 -    assignment: Boolean, nodes: Set[Document.Node.Name], commands: Set[Command])
    6.34 -
    6.35 -  sealed abstract class Phase
    6.36 -  case object Inactive extends Phase
    6.37 -  case object Startup extends Phase  // transient
    6.38 -  case object Failed extends Phase
    6.39 -  case object Ready extends Phase
    6.40 -  case object Shutdown extends Phase  // transient
    6.41 -  //}}}
    6.42 -
    6.43 -
    6.44 -  /* protocol handlers */
    6.45 -
    6.46 -  type Prover = Isabelle_Process with Protocol
    6.47 -
    6.48 -  abstract class Protocol_Handler
    6.49 -  {
    6.50 -    def stop(prover: Prover): Unit = {}
    6.51 -    val functions: Map[String, (Prover, Isabelle_Process.Protocol_Output) => Boolean]
    6.52 -  }
    6.53 -
    6.54 -  class Protocol_Handlers(
    6.55 -    handlers: Map[String, Session.Protocol_Handler] = Map.empty,
    6.56 -    functions: Map[String, Isabelle_Process.Protocol_Output => Boolean] = Map.empty)
    6.57 -  {
    6.58 -    def get(name: String): Option[Protocol_Handler] = handlers.get(name)
    6.59 -
    6.60 -    def add(prover: Prover, name: String): Protocol_Handlers =
    6.61 -    {
    6.62 -      val (handlers1, functions1) =
    6.63 -        handlers.get(name) match {
    6.64 -          case Some(old_handler) =>
    6.65 -            System.err.println("Redefining protocol handler: " + name)
    6.66 -            old_handler.stop(prover)
    6.67 -            (handlers - name, functions -- old_handler.functions.keys)
    6.68 -          case None => (handlers, functions)
    6.69 -        }
    6.70 -
    6.71 -      val (handlers2, functions2) =
    6.72 -        try {
    6.73 -          val new_handler = Class.forName(name).newInstance.asInstanceOf[Protocol_Handler]
    6.74 -          val new_functions =
    6.75 -            for ((a, f) <- new_handler.functions.toList) yield
    6.76 -              (a, (msg: Isabelle_Process.Protocol_Output) => f(prover, msg))
    6.77 -
    6.78 -          val dups = for ((a, _) <- new_functions if functions1.isDefinedAt(a)) yield a
    6.79 -          if (!dups.isEmpty) error("Duplicate protocol functions: " + commas_quote(dups))
    6.80 -
    6.81 -          (handlers1 + (name -> new_handler), functions1 ++ new_functions)
    6.82 -        }
    6.83 -        catch {
    6.84 -          case exn: Throwable =>
    6.85 -            System.err.println("Failed to initialize protocol handler: " +
    6.86 -              name + "\n" + Exn.message(exn))
    6.87 -            (handlers1, functions1)
    6.88 -        }
    6.89 -
    6.90 -      new Protocol_Handlers(handlers2, functions2)
    6.91 -    }
    6.92 -
    6.93 -    def invoke(msg: Isabelle_Process.Protocol_Output): Boolean =
    6.94 -      msg.properties match {
    6.95 -        case Markup.Function(a) if functions.isDefinedAt(a) =>
    6.96 -          try { functions(a)(msg) }
    6.97 -          catch {
    6.98 -            case exn: Throwable =>
    6.99 -              System.err.println("Failed invocation of protocol function: " +
   6.100 -                quote(a) + "\n" + Exn.message(exn))
   6.101 -            false
   6.102 -          }
   6.103 -        case _ => false
   6.104 -      }
   6.105 -
   6.106 -    def stop(prover: Prover): Protocol_Handlers =
   6.107 -    {
   6.108 -      for ((_, handler) <- handlers) handler.stop(prover)
   6.109 -      new Protocol_Handlers()
   6.110 -    }
   6.111 -  }
   6.112 -}
   6.113 -
   6.114 -
   6.115 -class Session(val resources: Resources)
   6.116 -{
   6.117 -  /* global flags */
   6.118 -
   6.119 -  @volatile var timing: Boolean = false
   6.120 -  @volatile var verbose: Boolean = false
   6.121 -
   6.122 -
   6.123 -  /* tuning parameters */
   6.124 -
   6.125 -  def output_delay: Time = Time.seconds(0.1)  // prover output (markup, common messages)
   6.126 -  def message_delay: Time = Time.seconds(0.1)  // prover input/output messages
   6.127 -  def prune_delay: Time = Time.seconds(60.0)  // prune history -- delete old versions
   6.128 -  def prune_size: Int = 0  // size of retained history
   6.129 -  def syslog_limit: Int = 100
   6.130 -  def reparse_limit: Int = 0
   6.131 -
   6.132 -
   6.133 -  /* pervasive event buses */
   6.134 -
   6.135 -  val statistics = new Event_Bus[Session.Statistics]
   6.136 -  val global_options = new Event_Bus[Session.Global_Options]
   6.137 -  val caret_focus = new Event_Bus[Session.Caret_Focus.type]
   6.138 -  val raw_edits = new Event_Bus[Session.Raw_Edits]
   6.139 -  val commands_changed = new Event_Bus[Session.Commands_Changed]
   6.140 -  val phase_changed = new Event_Bus[Session.Phase]
   6.141 -  val syslog_messages = new Event_Bus[Isabelle_Process.Output]
   6.142 -  val raw_output_messages = new Event_Bus[Isabelle_Process.Output]
   6.143 -  val all_messages = new Event_Bus[Isabelle_Process.Message]  // potential bottle-neck
   6.144 -  val trace_events = new Event_Bus[Simplifier_Trace.Event.type]
   6.145 -
   6.146 -
   6.147 -  /** buffered command changes (delay_first discipline) **/
   6.148 -
   6.149 -  //{{{
   6.150 -  private case object Stop
   6.151 -
   6.152 -  private val (_, commands_changed_buffer) =
   6.153 -    Simple_Thread.actor("commands_changed_buffer", daemon = true)
   6.154 -  {
   6.155 -    var finished = false
   6.156 -    while (!finished) {
   6.157 -      receive {
   6.158 -        case Stop => finished = true; reply(())
   6.159 -        case changed: Session.Commands_Changed => commands_changed.event(changed)
   6.160 -        case bad => System.err.println("commands_changed_buffer: ignoring bad message " + bad)
   6.161 -      }
   6.162 -    }
   6.163 -  }
   6.164 -  //}}}
   6.165 -
   6.166 -
   6.167 -  /** pipelined change parsing **/
   6.168 -
   6.169 -  //{{{
   6.170 -  private case class Text_Edits(
   6.171 -    previous: Future[Document.Version],
   6.172 -    doc_blobs: Document.Blobs,
   6.173 -    text_edits: List[Document.Edit_Text],
   6.174 -    version_result: Promise[Document.Version])
   6.175 -
   6.176 -  private val (_, change_parser) = Simple_Thread.actor("change_parser", daemon = true)
   6.177 -  {
   6.178 -    var finished = false
   6.179 -    while (!finished) {
   6.180 -      receive {
   6.181 -        case Stop => finished = true; reply(())
   6.182 -
   6.183 -        case Text_Edits(previous, doc_blobs, text_edits, version_result) =>
   6.184 -          val prev = previous.get_finished
   6.185 -          val (syntax_changed, doc_edits, version) =
   6.186 -            Timing.timeit("text_edits", timing) {
   6.187 -              resources.text_edits(reparse_limit, prev, doc_blobs, text_edits)
   6.188 -            }
   6.189 -          version_result.fulfill(version)
   6.190 -          sender ! Change(doc_blobs, syntax_changed, doc_edits, prev, version)
   6.191 -
   6.192 -        case bad => System.err.println("change_parser: ignoring bad message " + bad)
   6.193 -      }
   6.194 -    }
   6.195 -  }
   6.196 -  //}}}
   6.197 -
   6.198 -
   6.199 -
   6.200 -  /** main protocol actor **/
   6.201 -
   6.202 -  /* global state */
   6.203 -
   6.204 -  private val syslog = Volatile(Queue.empty[XML.Elem])
   6.205 -  def current_syslog(): String = cat_lines(syslog().iterator.map(XML.content))
   6.206 -
   6.207 -  @volatile private var _phase: Session.Phase = Session.Inactive
   6.208 -  private def phase_=(new_phase: Session.Phase)
   6.209 -  {
   6.210 -    _phase = new_phase
   6.211 -    phase_changed.event(new_phase)
   6.212 -  }
   6.213 -  def phase = _phase
   6.214 -  def is_ready: Boolean = phase == Session.Ready
   6.215 -
   6.216 -  private val global_state = Volatile(Document.State.init)
   6.217 -  def current_state(): Document.State = global_state()
   6.218 -
   6.219 -  def recent_syntax(): Outer_Syntax =
   6.220 -  {
   6.221 -    val version = current_state().recent_finished.version.get_finished
   6.222 -    if (version.is_init) resources.base_syntax
   6.223 -    else version.syntax
   6.224 -  }
   6.225 -
   6.226 -  def snapshot(name: Document.Node.Name = Document.Node.Name.empty,
   6.227 -      pending_edits: List[Text.Edit] = Nil): Document.Snapshot =
   6.228 -    global_state().snapshot(name, pending_edits)
   6.229 -
   6.230 -
   6.231 -  /* protocol handlers */
   6.232 -
   6.233 -  @volatile private var _protocol_handlers = new Session.Protocol_Handlers()
   6.234 -
   6.235 -  def protocol_handler(name: String): Option[Session.Protocol_Handler] =
   6.236 -    _protocol_handlers.get(name)
   6.237 -
   6.238 -
   6.239 -  /* theory files */
   6.240 -
   6.241 -  def header_edit(name: Document.Node.Name, header: Document.Node.Header): Document.Edit_Text =
   6.242 -  {
   6.243 -    val header1 =
   6.244 -      if (resources.loaded_theories(name.theory))
   6.245 -        header.error("Cannot update finished theory " + quote(name.theory))
   6.246 -      else header
   6.247 -    (name, Document.Node.Deps(header1))
   6.248 -  }
   6.249 -
   6.250 -
   6.251 -  /* actor messages */
   6.252 -
   6.253 -  private case class Start(args: List[String])
   6.254 -  private case class Cancel_Exec(exec_id: Document_ID.Exec)
   6.255 -  private case class Change(
   6.256 -    doc_blobs: Document.Blobs,
   6.257 -    syntax_changed: Boolean,
   6.258 -    doc_edits: List[Document.Edit_Command],
   6.259 -    previous: Document.Version,
   6.260 -    version: Document.Version)
   6.261 -  private case class Protocol_Command(name: String, args: List[String])
   6.262 -  private case class Messages(msgs: List[Isabelle_Process.Message])
   6.263 -  private case class Update_Options(options: Options)
   6.264 -
   6.265 -  private val (_, session_actor) = Simple_Thread.actor("session_actor", daemon = true)
   6.266 -  {
   6.267 -    val this_actor = self
   6.268 -
   6.269 -    var prune_next = System.currentTimeMillis() + prune_delay.ms
   6.270 -
   6.271 -
   6.272 -    /* buffered prover messages */
   6.273 -
   6.274 -    object receiver
   6.275 -    {
   6.276 -      private var buffer = new mutable.ListBuffer[Isabelle_Process.Message]
   6.277 -
   6.278 -      private def flush(): Unit = synchronized {
   6.279 -        if (!buffer.isEmpty) {
   6.280 -          val msgs = buffer.toList
   6.281 -          this_actor ! Messages(msgs)
   6.282 -          buffer = new mutable.ListBuffer[Isabelle_Process.Message]
   6.283 -        }
   6.284 -      }
   6.285 -      def invoke(msg: Isabelle_Process.Message): Unit = synchronized {
   6.286 -        msg match {
   6.287 -          case _: Isabelle_Process.Input =>
   6.288 -            buffer += msg
   6.289 -          case output: Isabelle_Process.Protocol_Output if output.properties == Markup.Flush =>
   6.290 -            flush()
   6.291 -          case output: Isabelle_Process.Output =>
   6.292 -            buffer += msg
   6.293 -            if (output.is_syslog)
   6.294 -              syslog >> (queue =>
   6.295 -                {
   6.296 -                  val queue1 = queue.enqueue(output.message)
   6.297 -                  if (queue1.length > syslog_limit) queue1.dequeue._2 else queue1
   6.298 -                })
   6.299 -        }
   6.300 -      }
   6.301 -
   6.302 -      private val timer = new Timer("session_actor.receiver", true)
   6.303 -      timer.schedule(new TimerTask { def run = flush }, message_delay.ms, message_delay.ms)
   6.304 -
   6.305 -      def cancel() { timer.cancel() }
   6.306 -    }
   6.307 -
   6.308 -    var prover: Option[Session.Prover] = None
   6.309 -
   6.310 -
   6.311 -    /* delayed command changes */
   6.312 -
   6.313 -    object delay_commands_changed
   6.314 -    {
   6.315 -      private var changed_assignment: Boolean = false
   6.316 -      private var changed_nodes: Set[Document.Node.Name] = Set.empty
   6.317 -      private var changed_commands: Set[Command] = Set.empty
   6.318 -
   6.319 -      private var flush_time: Option[Long] = None
   6.320 -
   6.321 -      def flush_timeout: Long =
   6.322 -        flush_time match {
   6.323 -          case None => 5000L
   6.324 -          case Some(time) => (time - System.currentTimeMillis()) max 0
   6.325 -        }
   6.326 -
   6.327 -      def flush()
   6.328 -      {
   6.329 -        if (changed_assignment || !changed_nodes.isEmpty || !changed_commands.isEmpty)
   6.330 -          commands_changed_buffer !
   6.331 -            Session.Commands_Changed(changed_assignment, changed_nodes, changed_commands)
   6.332 -        changed_assignment = false
   6.333 -        changed_nodes = Set.empty
   6.334 -        changed_commands = Set.empty
   6.335 -        flush_time = None
   6.336 -      }
   6.337 -
   6.338 -      def invoke(assign: Boolean, commands: List[Command])
   6.339 -      {
   6.340 -        changed_assignment |= assign
   6.341 -        for (command <- commands) {
   6.342 -          changed_nodes += command.node_name
   6.343 -          changed_commands += command
   6.344 -        }
   6.345 -        val now = System.currentTimeMillis()
   6.346 -        flush_time match {
   6.347 -          case None => flush_time = Some(now + output_delay.ms)
   6.348 -          case Some(time) => if (now >= time) flush()
   6.349 -        }
   6.350 -      }
   6.351 -    }
   6.352 -
   6.353 -
   6.354 -    /* raw edits */
   6.355 -
   6.356 -    def handle_raw_edits(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text])
   6.357 -    //{{{
   6.358 -    {
   6.359 -      prover.get.discontinue_execution()
   6.360 -
   6.361 -      val previous = global_state().history.tip.version
   6.362 -      val version = Future.promise[Document.Version]
   6.363 -      val change = global_state >>> (_.continue_history(previous, edits, version))
   6.364 -
   6.365 -      raw_edits.event(Session.Raw_Edits(doc_blobs, edits))
   6.366 -      change_parser ! Text_Edits(previous, doc_blobs, edits, version)
   6.367 -    }
   6.368 -    //}}}
   6.369 -
   6.370 -
   6.371 -    /* resulting changes */
   6.372 -
   6.373 -    def handle_change(change: Change)
   6.374 -    //{{{
   6.375 -    {
   6.376 -      val Change(doc_blobs, syntax_changed, doc_edits, previous, version) = change
   6.377 -
   6.378 -      def id_command(command: Command)
   6.379 -      {
   6.380 -        for {
   6.381 -          digest <- command.blobs_digests
   6.382 -          if !global_state().defined_blob(digest)
   6.383 -        } {
   6.384 -          doc_blobs.get(digest) match {
   6.385 -            case Some(blob) =>
   6.386 -              global_state >> (_.define_blob(digest))
   6.387 -              prover.get.define_blob(blob)
   6.388 -            case None =>
   6.389 -              System.err.println("Missing blob for SHA1 digest " + digest)
   6.390 -          }
   6.391 -        }
   6.392 -
   6.393 -        if (!global_state().defined_command(command.id)) {
   6.394 -          global_state >> (_.define_command(command))
   6.395 -          prover.get.define_command(command)
   6.396 -        }
   6.397 -      }
   6.398 -      doc_edits foreach {
   6.399 -        case (_, edit) =>
   6.400 -          edit foreach { case (c1, c2) => c1 foreach id_command; c2 foreach id_command }
   6.401 -      }
   6.402 -
   6.403 -      val assignment = global_state().the_assignment(previous).check_finished
   6.404 -      global_state >> (_.define_version(version, assignment))
   6.405 -      prover.get.update(previous.id, version.id, doc_edits)
   6.406 -
   6.407 -      if (syntax_changed) resources.syntax_changed()
   6.408 -    }
   6.409 -    //}}}
   6.410 -
   6.411 -
   6.412 -    /* prover output */
   6.413 -
   6.414 -    def handle_output(output: Isabelle_Process.Output)
   6.415 -    //{{{
   6.416 -    {
   6.417 -      def bad_output()
   6.418 -      {
   6.419 -        if (verbose)
   6.420 -          System.err.println("Ignoring prover output: " + output.message.toString)
   6.421 -      }
   6.422 -
   6.423 -      def accumulate(state_id: Document_ID.Generic, message: XML.Elem)
   6.424 -      {
   6.425 -        try {
   6.426 -          val st = global_state >>> (_.accumulate(state_id, message))
   6.427 -          delay_commands_changed.invoke(false, List(st.command))
   6.428 -        }
   6.429 -        catch {
   6.430 -          case _: Document.State.Fail => bad_output()
   6.431 -        }
   6.432 -      }
   6.433 -
   6.434 -      output match {
   6.435 -        case msg: Isabelle_Process.Protocol_Output =>
   6.436 -          val handled = _protocol_handlers.invoke(msg)
   6.437 -          if (!handled) {
   6.438 -            msg.properties match {
   6.439 -              case Markup.Protocol_Handler(name) =>
   6.440 -                _protocol_handlers = _protocol_handlers.add(prover.get, name)
   6.441 -
   6.442 -              case Protocol.Command_Timing(state_id, timing) =>
   6.443 -                val message = XML.elem(Markup.STATUS, List(XML.Elem(Markup.Timing(timing), Nil)))
   6.444 -                accumulate(state_id, prover.get.xml_cache.elem(message))
   6.445 -
   6.446 -              case Markup.Assign_Update =>
   6.447 -                msg.text match {
   6.448 -                  case Protocol.Assign_Update(id, update) =>
   6.449 -                    try {
   6.450 -                      val cmds = global_state >>> (_.assign(id, update))
   6.451 -                      delay_commands_changed.invoke(true, cmds)
   6.452 -                    }
   6.453 -                    catch { case _: Document.State.Fail => bad_output() }
   6.454 -                  case _ => bad_output()
   6.455 -                }
   6.456 -                // FIXME separate timeout event/message!?
   6.457 -                if (prover.isDefined && System.currentTimeMillis() > prune_next) {
   6.458 -                  val old_versions = global_state >>> (_.prune_history(prune_size))
   6.459 -                  if (!old_versions.isEmpty) prover.get.remove_versions(old_versions)
   6.460 -                  prune_next = System.currentTimeMillis() + prune_delay.ms
   6.461 -                }
   6.462 -
   6.463 -              case Markup.Removed_Versions =>
   6.464 -                msg.text match {
   6.465 -                  case Protocol.Removed(removed) =>
   6.466 -                    try {
   6.467 -                      global_state >> (_.removed_versions(removed))
   6.468 -                    }
   6.469 -                    catch { case _: Document.State.Fail => bad_output() }
   6.470 -                  case _ => bad_output()
   6.471 -                }
   6.472 -
   6.473 -              case Markup.ML_Statistics(props) =>
   6.474 -                statistics.event(Session.Statistics(props))
   6.475 -
   6.476 -              case Markup.Task_Statistics(props) =>
   6.477 -                // FIXME
   6.478 -
   6.479 -              case _ => bad_output()
   6.480 -            }
   6.481 -          }
   6.482 -        case _ =>
   6.483 -          output.properties match {
   6.484 -            case Position.Id(state_id) =>
   6.485 -              accumulate(state_id, output.message)
   6.486 -  
   6.487 -            case _ if output.is_init =>
   6.488 -              phase = Session.Ready
   6.489 -  
   6.490 -            case Markup.Return_Code(rc) if output.is_exit =>
   6.491 -              if (rc == 0) phase = Session.Inactive
   6.492 -              else phase = Session.Failed
   6.493 -  
   6.494 -            case _ => raw_output_messages.event(output)
   6.495 -          }
   6.496 -        }
   6.497 -    }
   6.498 -    //}}}
   6.499 -
   6.500 -
   6.501 -    /* main loop */
   6.502 -
   6.503 -    //{{{
   6.504 -    var finished = false
   6.505 -    while (!finished) {
   6.506 -      receiveWithin(delay_commands_changed.flush_timeout) {
   6.507 -        case TIMEOUT => delay_commands_changed.flush()
   6.508 -
   6.509 -        case Start(args) if prover.isEmpty =>
   6.510 -          if (phase == Session.Inactive || phase == Session.Failed) {
   6.511 -            phase = Session.Startup
   6.512 -            prover = Some(new Isabelle_Process(receiver.invoke _, args) with Protocol)
   6.513 -          }
   6.514 -
   6.515 -        case Stop =>
   6.516 -          if (phase == Session.Ready) {
   6.517 -            _protocol_handlers = _protocol_handlers.stop(prover.get)
   6.518 -            global_state >> (_ => Document.State.init)  // FIXME event bus!?
   6.519 -            phase = Session.Shutdown
   6.520 -            prover.get.terminate
   6.521 -            prover = None
   6.522 -            phase = Session.Inactive
   6.523 -          }
   6.524 -          finished = true
   6.525 -          receiver.cancel()
   6.526 -          reply(())
   6.527 -
   6.528 -        case Update_Options(options) if prover.isDefined =>
   6.529 -          if (is_ready) {
   6.530 -            prover.get.options(options)
   6.531 -            handle_raw_edits(Document.Blobs.empty, Nil)
   6.532 -          }
   6.533 -          global_options.event(Session.Global_Options(options))
   6.534 -          reply(())
   6.535 -
   6.536 -        case Cancel_Exec(exec_id) if prover.isDefined =>
   6.537 -          prover.get.cancel_exec(exec_id)
   6.538 -
   6.539 -        case Session.Raw_Edits(doc_blobs, edits) if prover.isDefined =>
   6.540 -          handle_raw_edits(doc_blobs, edits)
   6.541 -          reply(())
   6.542 -
   6.543 -        case Session.Dialog_Result(id, serial, result) if prover.isDefined =>
   6.544 -          prover.get.dialog_result(serial, result)
   6.545 -          handle_output(new Isabelle_Process.Output(Protocol.Dialog_Result(id, serial, result)))
   6.546 -
   6.547 -        case Protocol_Command(name, args) if prover.isDefined =>
   6.548 -          prover.get.protocol_command(name, args:_*)
   6.549 -
   6.550 -        case Messages(msgs) =>
   6.551 -          msgs foreach {
   6.552 -            case input: Isabelle_Process.Input =>
   6.553 -              all_messages.event(input)
   6.554 -
   6.555 -            case output: Isabelle_Process.Output =>
   6.556 -              if (output.is_stdout || output.is_stderr) raw_output_messages.event(output)
   6.557 -              else handle_output(output)
   6.558 -              if (output.is_syslog) syslog_messages.event(output)
   6.559 -              all_messages.event(output)
   6.560 -          }
   6.561 -
   6.562 -        case change: Change
   6.563 -        if prover.isDefined && global_state().is_assigned(change.previous) =>
   6.564 -          handle_change(change)
   6.565 -
   6.566 -        case bad if !bad.isInstanceOf[Change] =>
   6.567 -          System.err.println("session_actor: ignoring bad message " + bad)
   6.568 -      }
   6.569 -    }
   6.570 -    //}}}
   6.571 -  }
   6.572 -
   6.573 -
   6.574 -  /* actions */
   6.575 -
   6.576 -  def start(args: List[String])
   6.577 -  {
   6.578 -    session_actor ! Start(args)
   6.579 -  }
   6.580 -
   6.581 -  def stop()
   6.582 -  {
   6.583 -    commands_changed_buffer !? Stop
   6.584 -    change_parser !? Stop
   6.585 -    session_actor !? Stop
   6.586 -  }
   6.587 -
   6.588 -  def protocol_command(name: String, args: String*)
   6.589 -  { session_actor ! Protocol_Command(name, args.toList) }
   6.590 -
   6.591 -  def cancel_exec(exec_id: Document_ID.Exec) { session_actor ! Cancel_Exec(exec_id) }
   6.592 -
   6.593 -  def update(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text])
   6.594 -  { if (!edits.isEmpty) session_actor !? Session.Raw_Edits(doc_blobs, edits) }
   6.595 -
   6.596 -  def update_options(options: Options)
   6.597 -  { session_actor !? Update_Options(options) }
   6.598 -
   6.599 -  def dialog_result(id: Document_ID.Generic, serial: Long, result: String)
   6.600 -  { session_actor ! Session.Dialog_Result(id, serial, result) }
   6.601 -}
     7.1 --- a/src/Pure/build-jars	Tue Mar 18 17:53:40 2014 +0100
     7.2 +++ b/src/Pure/build-jars	Tue Mar 18 18:09:31 2014 +0100
     7.3 @@ -54,6 +54,7 @@
     7.4    PIDE/protocol.scala
     7.5    PIDE/query_operation.scala
     7.6    PIDE/resources.scala
     7.7 +  PIDE/session.scala
     7.8    PIDE/text.scala
     7.9    PIDE/xml.scala
    7.10    PIDE/yxml.scala
    7.11 @@ -67,7 +68,6 @@
    7.12    System/isabelle_system.scala
    7.13    System/options.scala
    7.14    System/platform.scala
    7.15 -  System/session.scala
    7.16    System/system_channel.scala
    7.17    System/utf8.scala
    7.18    Thy/html.scala