# HG changeset patch # User wenzelm # Date 1395162571 -3600 # Node ID c7c85cdb725dbfeac6048aeef520d3b0d8bf74f6 # Parent 3c89e21d9be26a71804562a57476e60c0c6f1dad clarified module arrangement; diff -r 3c89e21d9be2 -r c7c85cdb725d src/Pure/PIDE/session.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/PIDE/session.ML Tue Mar 18 18:09:31 2014 +0100 @@ -0,0 +1,80 @@ +(* Title: Pure/PIDE/session.ML + Author: Makarius + +Prover session: persistent state of logic image. +*) + +signature SESSION = +sig + val name: unit -> string + val welcome: unit -> string + val init: bool -> bool -> Path.T -> string -> bool -> string -> (string * string) list -> + string -> string * string -> bool * string -> bool -> unit + val finish: unit -> unit + val protocol_handler: string -> unit + val init_protocol_handlers: unit -> unit +end; + +structure Session: SESSION = +struct + +(** session identification -- not thread-safe **) + +val session = Unsynchronized.ref {chapter = "Pure", name = "Pure"}; +val session_finished = Unsynchronized.ref false; + +fun name () = "Isabelle/" ^ #name (! session); + +fun welcome () = + if Distribution.is_official then + "Welcome to " ^ name () ^ " (" ^ Distribution.version ^ ")" + else "Unofficial version of " ^ name () ^ " (" ^ Distribution.version ^ ")"; + + +(* init *) + +fun init build info info_path doc doc_graph doc_output doc_variants + parent (chapter, name) doc_dump verbose = + if #name (! session) <> parent orelse not (! session_finished) then + error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name) + else + let + val _ = session := {chapter = chapter, name = name}; + val _ = session_finished := false; + in + Present.init build info info_path (if doc = "false" then "" else doc) + doc_graph doc_output doc_variants (chapter, name) + doc_dump verbose (map Thy_Info.get_theory (Thy_Info.get_names ())) + end; + + +(* finish *) + +fun finish () = + (Execution.shutdown (); + Thy_Info.finish (); + Present.finish (); + Outer_Syntax.check_syntax (); + Future.shutdown (); + Event_Timer.shutdown (); + Future.shutdown (); + session_finished := true); + + + +(** protocol handlers **) + +val protocol_handlers = Synchronized.var "protocol_handlers" ([]: string list); + +fun protocol_handler name = + Synchronized.change protocol_handlers (fn handlers => + (Output.try_protocol_message (Markup.protocol_handler name) ""; + if not (member (op =) handlers name) then () + else warning ("Redefining protocol handler: " ^ quote name); + update (op =) name handlers)); + +fun init_protocol_handlers () = + Synchronized.value protocol_handlers + |> List.app (fn name => Output.try_protocol_message (Markup.protocol_handler name) ""); + +end; diff -r 3c89e21d9be2 -r c7c85cdb725d src/Pure/PIDE/session.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/PIDE/session.scala Tue Mar 18 18:09:31 2014 +0100 @@ -0,0 +1,598 @@ +/* Title: Pure/PIDE/session.scala + Author: Makarius + Options: :folding=explicit:collapseFolds=1: + +PIDE editor session, potentially with running prover process. +*/ + +package isabelle + + +import java.util.{Timer, TimerTask} + +import scala.collection.mutable +import scala.collection.immutable.Queue +import scala.actors.TIMEOUT +import scala.actors.Actor._ + + +object Session +{ + /* events */ + + //{{{ + case class Statistics(props: Properties.T) + case class Global_Options(options: Options) + case object Caret_Focus + case class Raw_Edits(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text]) + case class Dialog_Result(id: Document_ID.Generic, serial: Long, result: String) + case class Commands_Changed( + assignment: Boolean, nodes: Set[Document.Node.Name], commands: Set[Command]) + + sealed abstract class Phase + case object Inactive extends Phase + case object Startup extends Phase // transient + case object Failed extends Phase + case object Ready extends Phase + case object Shutdown extends Phase // transient + //}}} + + + /* protocol handlers */ + + type Prover = Isabelle_Process with Protocol + + abstract class Protocol_Handler + { + def stop(prover: Prover): Unit = {} + val functions: Map[String, (Prover, Isabelle_Process.Protocol_Output) => Boolean] + } + + class Protocol_Handlers( + handlers: Map[String, Session.Protocol_Handler] = Map.empty, + functions: Map[String, Isabelle_Process.Protocol_Output => Boolean] = Map.empty) + { + def get(name: String): Option[Protocol_Handler] = handlers.get(name) + + def add(prover: Prover, name: String): Protocol_Handlers = + { + val (handlers1, functions1) = + handlers.get(name) match { + case Some(old_handler) => + System.err.println("Redefining protocol handler: " + name) + old_handler.stop(prover) + (handlers - name, functions -- old_handler.functions.keys) + case None => (handlers, functions) + } + + val (handlers2, functions2) = + try { + val new_handler = Class.forName(name).newInstance.asInstanceOf[Protocol_Handler] + val new_functions = + for ((a, f) <- new_handler.functions.toList) yield + (a, (msg: Isabelle_Process.Protocol_Output) => f(prover, msg)) + + val dups = for ((a, _) <- new_functions if functions1.isDefinedAt(a)) yield a + if (!dups.isEmpty) error("Duplicate protocol functions: " + commas_quote(dups)) + + (handlers1 + (name -> new_handler), functions1 ++ new_functions) + } + catch { + case exn: Throwable => + System.err.println("Failed to initialize protocol handler: " + + name + "\n" + Exn.message(exn)) + (handlers1, functions1) + } + + new Protocol_Handlers(handlers2, functions2) + } + + def invoke(msg: Isabelle_Process.Protocol_Output): Boolean = + msg.properties match { + case Markup.Function(a) if functions.isDefinedAt(a) => + try { functions(a)(msg) } + catch { + case exn: Throwable => + System.err.println("Failed invocation of protocol function: " + + quote(a) + "\n" + Exn.message(exn)) + false + } + case _ => false + } + + def stop(prover: Prover): Protocol_Handlers = + { + for ((_, handler) <- handlers) handler.stop(prover) + new Protocol_Handlers() + } + } +} + + +class Session(val resources: Resources) +{ + /* global flags */ + + @volatile var timing: Boolean = false + @volatile var verbose: Boolean = false + + + /* tuning parameters */ + + def output_delay: Time = Time.seconds(0.1) // prover output (markup, common messages) + def message_delay: Time = Time.seconds(0.1) // prover input/output messages + def prune_delay: Time = Time.seconds(60.0) // prune history -- delete old versions + def prune_size: Int = 0 // size of retained history + def syslog_limit: Int = 100 + def reparse_limit: Int = 0 + + + /* pervasive event buses */ + + val statistics = new Event_Bus[Session.Statistics] + val global_options = new Event_Bus[Session.Global_Options] + val caret_focus = new Event_Bus[Session.Caret_Focus.type] + val raw_edits = new Event_Bus[Session.Raw_Edits] + val commands_changed = new Event_Bus[Session.Commands_Changed] + val phase_changed = new Event_Bus[Session.Phase] + val syslog_messages = new Event_Bus[Isabelle_Process.Output] + val raw_output_messages = new Event_Bus[Isabelle_Process.Output] + val all_messages = new Event_Bus[Isabelle_Process.Message] // potential bottle-neck + val trace_events = new Event_Bus[Simplifier_Trace.Event.type] + + + /** buffered command changes (delay_first discipline) **/ + + //{{{ + private case object Stop + + private val (_, commands_changed_buffer) = + Simple_Thread.actor("commands_changed_buffer", daemon = true) + { + var finished = false + while (!finished) { + receive { + case Stop => finished = true; reply(()) + case changed: Session.Commands_Changed => commands_changed.event(changed) + case bad => System.err.println("commands_changed_buffer: ignoring bad message " + bad) + } + } + } + //}}} + + + /** pipelined change parsing **/ + + //{{{ + private case class Text_Edits( + previous: Future[Document.Version], + doc_blobs: Document.Blobs, + text_edits: List[Document.Edit_Text], + version_result: Promise[Document.Version]) + + private val (_, change_parser) = Simple_Thread.actor("change_parser", daemon = true) + { + var finished = false + while (!finished) { + receive { + case Stop => finished = true; reply(()) + + case Text_Edits(previous, doc_blobs, text_edits, version_result) => + val prev = previous.get_finished + val (syntax_changed, doc_edits, version) = + Timing.timeit("text_edits", timing) { + resources.text_edits(reparse_limit, prev, doc_blobs, text_edits) + } + version_result.fulfill(version) + sender ! Change(doc_blobs, syntax_changed, doc_edits, prev, version) + + case bad => System.err.println("change_parser: ignoring bad message " + bad) + } + } + } + //}}} + + + + /** main protocol actor **/ + + /* global state */ + + private val syslog = Volatile(Queue.empty[XML.Elem]) + def current_syslog(): String = cat_lines(syslog().iterator.map(XML.content)) + + @volatile private var _phase: Session.Phase = Session.Inactive + private def phase_=(new_phase: Session.Phase) + { + _phase = new_phase + phase_changed.event(new_phase) + } + def phase = _phase + def is_ready: Boolean = phase == Session.Ready + + private val global_state = Volatile(Document.State.init) + def current_state(): Document.State = global_state() + + def recent_syntax(): Outer_Syntax = + { + val version = current_state().recent_finished.version.get_finished + if (version.is_init) resources.base_syntax + else version.syntax + } + + def snapshot(name: Document.Node.Name = Document.Node.Name.empty, + pending_edits: List[Text.Edit] = Nil): Document.Snapshot = + global_state().snapshot(name, pending_edits) + + + /* protocol handlers */ + + @volatile private var _protocol_handlers = new Session.Protocol_Handlers() + + def protocol_handler(name: String): Option[Session.Protocol_Handler] = + _protocol_handlers.get(name) + + + /* theory files */ + + def header_edit(name: Document.Node.Name, header: Document.Node.Header): Document.Edit_Text = + { + val header1 = + if (resources.loaded_theories(name.theory)) + header.error("Cannot update finished theory " + quote(name.theory)) + else header + (name, Document.Node.Deps(header1)) + } + + + /* actor messages */ + + private case class Start(args: List[String]) + private case class Cancel_Exec(exec_id: Document_ID.Exec) + private case class Change( + doc_blobs: Document.Blobs, + syntax_changed: Boolean, + doc_edits: List[Document.Edit_Command], + previous: Document.Version, + version: Document.Version) + private case class Protocol_Command(name: String, args: List[String]) + private case class Messages(msgs: List[Isabelle_Process.Message]) + private case class Update_Options(options: Options) + + private val (_, session_actor) = Simple_Thread.actor("session_actor", daemon = true) + { + val this_actor = self + + var prune_next = System.currentTimeMillis() + prune_delay.ms + + + /* buffered prover messages */ + + object receiver + { + private var buffer = new mutable.ListBuffer[Isabelle_Process.Message] + + private def flush(): Unit = synchronized { + if (!buffer.isEmpty) { + val msgs = buffer.toList + this_actor ! Messages(msgs) + buffer = new mutable.ListBuffer[Isabelle_Process.Message] + } + } + def invoke(msg: Isabelle_Process.Message): Unit = synchronized { + msg match { + case _: Isabelle_Process.Input => + buffer += msg + case output: Isabelle_Process.Protocol_Output if output.properties == Markup.Flush => + flush() + case output: Isabelle_Process.Output => + buffer += msg + if (output.is_syslog) + syslog >> (queue => + { + val queue1 = queue.enqueue(output.message) + if (queue1.length > syslog_limit) queue1.dequeue._2 else queue1 + }) + } + } + + private val timer = new Timer("session_actor.receiver", true) + timer.schedule(new TimerTask { def run = flush }, message_delay.ms, message_delay.ms) + + def cancel() { timer.cancel() } + } + + var prover: Option[Session.Prover] = None + + + /* delayed command changes */ + + object delay_commands_changed + { + private var changed_assignment: Boolean = false + private var changed_nodes: Set[Document.Node.Name] = Set.empty + private var changed_commands: Set[Command] = Set.empty + + private var flush_time: Option[Long] = None + + def flush_timeout: Long = + flush_time match { + case None => 5000L + case Some(time) => (time - System.currentTimeMillis()) max 0 + } + + def flush() + { + if (changed_assignment || !changed_nodes.isEmpty || !changed_commands.isEmpty) + commands_changed_buffer ! + Session.Commands_Changed(changed_assignment, changed_nodes, changed_commands) + changed_assignment = false + changed_nodes = Set.empty + changed_commands = Set.empty + flush_time = None + } + + def invoke(assign: Boolean, commands: List[Command]) + { + changed_assignment |= assign + for (command <- commands) { + changed_nodes += command.node_name + changed_commands += command + } + val now = System.currentTimeMillis() + flush_time match { + case None => flush_time = Some(now + output_delay.ms) + case Some(time) => if (now >= time) flush() + } + } + } + + + /* raw edits */ + + def handle_raw_edits(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text]) + //{{{ + { + prover.get.discontinue_execution() + + val previous = global_state().history.tip.version + val version = Future.promise[Document.Version] + val change = global_state >>> (_.continue_history(previous, edits, version)) + + raw_edits.event(Session.Raw_Edits(doc_blobs, edits)) + change_parser ! Text_Edits(previous, doc_blobs, edits, version) + } + //}}} + + + /* resulting changes */ + + def handle_change(change: Change) + //{{{ + { + val Change(doc_blobs, syntax_changed, doc_edits, previous, version) = change + + def id_command(command: Command) + { + for { + digest <- command.blobs_digests + if !global_state().defined_blob(digest) + } { + doc_blobs.get(digest) match { + case Some(blob) => + global_state >> (_.define_blob(digest)) + prover.get.define_blob(blob) + case None => + System.err.println("Missing blob for SHA1 digest " + digest) + } + } + + if (!global_state().defined_command(command.id)) { + global_state >> (_.define_command(command)) + prover.get.define_command(command) + } + } + doc_edits foreach { + case (_, edit) => + edit foreach { case (c1, c2) => c1 foreach id_command; c2 foreach id_command } + } + + val assignment = global_state().the_assignment(previous).check_finished + global_state >> (_.define_version(version, assignment)) + prover.get.update(previous.id, version.id, doc_edits) + + if (syntax_changed) resources.syntax_changed() + } + //}}} + + + /* prover output */ + + def handle_output(output: Isabelle_Process.Output) + //{{{ + { + def bad_output() + { + if (verbose) + System.err.println("Ignoring prover output: " + output.message.toString) + } + + def accumulate(state_id: Document_ID.Generic, message: XML.Elem) + { + try { + val st = global_state >>> (_.accumulate(state_id, message)) + delay_commands_changed.invoke(false, List(st.command)) + } + catch { + case _: Document.State.Fail => bad_output() + } + } + + output match { + case msg: Isabelle_Process.Protocol_Output => + val handled = _protocol_handlers.invoke(msg) + if (!handled) { + msg.properties match { + case Markup.Protocol_Handler(name) => + _protocol_handlers = _protocol_handlers.add(prover.get, name) + + case Protocol.Command_Timing(state_id, timing) => + val message = XML.elem(Markup.STATUS, List(XML.Elem(Markup.Timing(timing), Nil))) + accumulate(state_id, prover.get.xml_cache.elem(message)) + + case Markup.Assign_Update => + msg.text match { + case Protocol.Assign_Update(id, update) => + try { + val cmds = global_state >>> (_.assign(id, update)) + delay_commands_changed.invoke(true, cmds) + } + catch { case _: Document.State.Fail => bad_output() } + case _ => bad_output() + } + // FIXME separate timeout event/message!? + if (prover.isDefined && System.currentTimeMillis() > prune_next) { + val old_versions = global_state >>> (_.prune_history(prune_size)) + if (!old_versions.isEmpty) prover.get.remove_versions(old_versions) + prune_next = System.currentTimeMillis() + prune_delay.ms + } + + case Markup.Removed_Versions => + msg.text match { + case Protocol.Removed(removed) => + try { + global_state >> (_.removed_versions(removed)) + } + catch { case _: Document.State.Fail => bad_output() } + case _ => bad_output() + } + + case Markup.ML_Statistics(props) => + statistics.event(Session.Statistics(props)) + + case Markup.Task_Statistics(props) => + // FIXME + + case _ => bad_output() + } + } + case _ => + output.properties match { + case Position.Id(state_id) => + accumulate(state_id, output.message) + + case _ if output.is_init => + phase = Session.Ready + + case Markup.Return_Code(rc) if output.is_exit => + if (rc == 0) phase = Session.Inactive + else phase = Session.Failed + + case _ => raw_output_messages.event(output) + } + } + } + //}}} + + + /* main loop */ + + //{{{ + var finished = false + while (!finished) { + receiveWithin(delay_commands_changed.flush_timeout) { + case TIMEOUT => delay_commands_changed.flush() + + case Start(args) if prover.isEmpty => + if (phase == Session.Inactive || phase == Session.Failed) { + phase = Session.Startup + prover = Some(new Isabelle_Process(receiver.invoke _, args) with Protocol) + } + + case Stop => + if (phase == Session.Ready) { + _protocol_handlers = _protocol_handlers.stop(prover.get) + global_state >> (_ => Document.State.init) // FIXME event bus!? + phase = Session.Shutdown + prover.get.terminate + prover = None + phase = Session.Inactive + } + finished = true + receiver.cancel() + reply(()) + + case Update_Options(options) if prover.isDefined => + if (is_ready) { + prover.get.options(options) + handle_raw_edits(Document.Blobs.empty, Nil) + } + global_options.event(Session.Global_Options(options)) + reply(()) + + case Cancel_Exec(exec_id) if prover.isDefined => + prover.get.cancel_exec(exec_id) + + case Session.Raw_Edits(doc_blobs, edits) if prover.isDefined => + handle_raw_edits(doc_blobs, edits) + reply(()) + + case Session.Dialog_Result(id, serial, result) if prover.isDefined => + prover.get.dialog_result(serial, result) + handle_output(new Isabelle_Process.Output(Protocol.Dialog_Result(id, serial, result))) + + case Protocol_Command(name, args) if prover.isDefined => + prover.get.protocol_command(name, args:_*) + + case Messages(msgs) => + msgs foreach { + case input: Isabelle_Process.Input => + all_messages.event(input) + + case output: Isabelle_Process.Output => + if (output.is_stdout || output.is_stderr) raw_output_messages.event(output) + else handle_output(output) + if (output.is_syslog) syslog_messages.event(output) + all_messages.event(output) + } + + case change: Change + if prover.isDefined && global_state().is_assigned(change.previous) => + handle_change(change) + + case bad if !bad.isInstanceOf[Change] => + System.err.println("session_actor: ignoring bad message " + bad) + } + } + //}}} + } + + + /* actions */ + + def start(args: List[String]) + { + session_actor ! Start(args) + } + + def stop() + { + commands_changed_buffer !? Stop + change_parser !? Stop + session_actor !? Stop + } + + def protocol_command(name: String, args: String*) + { session_actor ! Protocol_Command(name, args.toList) } + + def cancel_exec(exec_id: Document_ID.Exec) { session_actor ! Cancel_Exec(exec_id) } + + def update(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text]) + { if (!edits.isEmpty) session_actor !? Session.Raw_Edits(doc_blobs, edits) } + + def update_options(options: Options) + { session_actor !? Update_Options(options) } + + def dialog_result(id: Document_ID.Generic, serial: Long, result: String) + { session_actor ! Session.Dialog_Result(id, serial, result) } +} diff -r 3c89e21d9be2 -r c7c85cdb725d src/Pure/ROOT --- a/src/Pure/ROOT Tue Mar 18 17:53:40 2014 +0100 +++ b/src/Pure/ROOT Tue Mar 18 18:09:31 2014 +0100 @@ -162,6 +162,7 @@ "PIDE/protocol.ML" "PIDE/query_operation.ML" "PIDE/resources.ML" + "PIDE/session.ML" "PIDE/xml.ML" "PIDE/yxml.ML" "Proof/extraction.ML" @@ -190,7 +191,6 @@ "System/isar.ML" "System/message_channel.ML" "System/options.ML" - "System/session.ML" "System/system_channel.ML" "Thy/html.ML" "Thy/latex.ML" diff -r 3c89e21d9be2 -r c7c85cdb725d src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Tue Mar 18 17:53:40 2014 +0100 +++ b/src/Pure/ROOT.ML Tue Mar 18 18:09:31 2014 +0100 @@ -294,7 +294,7 @@ (* Isabelle/Isar system *) -use "System/session.ML"; +use "PIDE/session.ML"; use "System/command_line.ML"; use "System/system_channel.ML"; use "System/message_channel.ML"; diff -r 3c89e21d9be2 -r c7c85cdb725d src/Pure/System/session.ML --- a/src/Pure/System/session.ML Tue Mar 18 17:53:40 2014 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,79 +0,0 @@ -(* Title: Pure/System/session.ML - Author: Makarius - -Session management -- internal state of logic images. -*) - -signature SESSION = -sig - val name: unit -> string - val welcome: unit -> string - val init: bool -> bool -> Path.T -> string -> bool -> string -> (string * string) list -> - string -> string * string -> bool * string -> bool -> unit - val finish: unit -> unit - val protocol_handler: string -> unit - val init_protocol_handlers: unit -> unit -end; - -structure Session: SESSION = -struct - -(** session identification -- not thread-safe **) - -val session = Unsynchronized.ref {chapter = "Pure", name = "Pure"}; -val session_finished = Unsynchronized.ref false; - -fun name () = "Isabelle/" ^ #name (! session); - -fun welcome () = - if Distribution.is_official then - "Welcome to " ^ name () ^ " (" ^ Distribution.version ^ ")" - else "Unofficial version of " ^ name () ^ " (" ^ Distribution.version ^ ")"; - - -(* init *) - -fun init build info info_path doc doc_graph doc_output doc_variants - parent (chapter, name) doc_dump verbose = - if #name (! session) <> parent orelse not (! session_finished) then - error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name) - else - let - val _ = session := {chapter = chapter, name = name}; - val _ = session_finished := false; - in - Present.init build info info_path (if doc = "false" then "" else doc) - doc_graph doc_output doc_variants (chapter, name) - doc_dump verbose (map Thy_Info.get_theory (Thy_Info.get_names ())) - end; - - -(* finish *) - -fun finish () = - (Execution.shutdown (); - Thy_Info.finish (); - Present.finish (); - Outer_Syntax.check_syntax (); - Future.shutdown (); - Event_Timer.shutdown (); - Future.shutdown (); - session_finished := true); - - -(** protocol handlers **) - -val protocol_handlers = Synchronized.var "protocol_handlers" ([]: string list); - -fun protocol_handler name = - Synchronized.change protocol_handlers (fn handlers => - (Output.try_protocol_message (Markup.protocol_handler name) ""; - if not (member (op =) handlers name) then () - else warning ("Redefining protocol handler: " ^ quote name); - update (op =) name handlers)); - -fun init_protocol_handlers () = - Synchronized.value protocol_handlers - |> List.app (fn name => Output.try_protocol_message (Markup.protocol_handler name) ""); - -end; diff -r 3c89e21d9be2 -r c7c85cdb725d src/Pure/System/session.scala --- a/src/Pure/System/session.scala Tue Mar 18 17:53:40 2014 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,598 +0,0 @@ -/* Title: Pure/System/session.scala - Author: Makarius - Options: :folding=explicit:collapseFolds=1: - -Main Isabelle/Scala session, potentially with running prover process. -*/ - -package isabelle - - -import java.util.{Timer, TimerTask} - -import scala.collection.mutable -import scala.collection.immutable.Queue -import scala.actors.TIMEOUT -import scala.actors.Actor._ - - -object Session -{ - /* events */ - - //{{{ - case class Statistics(props: Properties.T) - case class Global_Options(options: Options) - case object Caret_Focus - case class Raw_Edits(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text]) - case class Dialog_Result(id: Document_ID.Generic, serial: Long, result: String) - case class Commands_Changed( - assignment: Boolean, nodes: Set[Document.Node.Name], commands: Set[Command]) - - sealed abstract class Phase - case object Inactive extends Phase - case object Startup extends Phase // transient - case object Failed extends Phase - case object Ready extends Phase - case object Shutdown extends Phase // transient - //}}} - - - /* protocol handlers */ - - type Prover = Isabelle_Process with Protocol - - abstract class Protocol_Handler - { - def stop(prover: Prover): Unit = {} - val functions: Map[String, (Prover, Isabelle_Process.Protocol_Output) => Boolean] - } - - class Protocol_Handlers( - handlers: Map[String, Session.Protocol_Handler] = Map.empty, - functions: Map[String, Isabelle_Process.Protocol_Output => Boolean] = Map.empty) - { - def get(name: String): Option[Protocol_Handler] = handlers.get(name) - - def add(prover: Prover, name: String): Protocol_Handlers = - { - val (handlers1, functions1) = - handlers.get(name) match { - case Some(old_handler) => - System.err.println("Redefining protocol handler: " + name) - old_handler.stop(prover) - (handlers - name, functions -- old_handler.functions.keys) - case None => (handlers, functions) - } - - val (handlers2, functions2) = - try { - val new_handler = Class.forName(name).newInstance.asInstanceOf[Protocol_Handler] - val new_functions = - for ((a, f) <- new_handler.functions.toList) yield - (a, (msg: Isabelle_Process.Protocol_Output) => f(prover, msg)) - - val dups = for ((a, _) <- new_functions if functions1.isDefinedAt(a)) yield a - if (!dups.isEmpty) error("Duplicate protocol functions: " + commas_quote(dups)) - - (handlers1 + (name -> new_handler), functions1 ++ new_functions) - } - catch { - case exn: Throwable => - System.err.println("Failed to initialize protocol handler: " + - name + "\n" + Exn.message(exn)) - (handlers1, functions1) - } - - new Protocol_Handlers(handlers2, functions2) - } - - def invoke(msg: Isabelle_Process.Protocol_Output): Boolean = - msg.properties match { - case Markup.Function(a) if functions.isDefinedAt(a) => - try { functions(a)(msg) } - catch { - case exn: Throwable => - System.err.println("Failed invocation of protocol function: " + - quote(a) + "\n" + Exn.message(exn)) - false - } - case _ => false - } - - def stop(prover: Prover): Protocol_Handlers = - { - for ((_, handler) <- handlers) handler.stop(prover) - new Protocol_Handlers() - } - } -} - - -class Session(val resources: Resources) -{ - /* global flags */ - - @volatile var timing: Boolean = false - @volatile var verbose: Boolean = false - - - /* tuning parameters */ - - def output_delay: Time = Time.seconds(0.1) // prover output (markup, common messages) - def message_delay: Time = Time.seconds(0.1) // prover input/output messages - def prune_delay: Time = Time.seconds(60.0) // prune history -- delete old versions - def prune_size: Int = 0 // size of retained history - def syslog_limit: Int = 100 - def reparse_limit: Int = 0 - - - /* pervasive event buses */ - - val statistics = new Event_Bus[Session.Statistics] - val global_options = new Event_Bus[Session.Global_Options] - val caret_focus = new Event_Bus[Session.Caret_Focus.type] - val raw_edits = new Event_Bus[Session.Raw_Edits] - val commands_changed = new Event_Bus[Session.Commands_Changed] - val phase_changed = new Event_Bus[Session.Phase] - val syslog_messages = new Event_Bus[Isabelle_Process.Output] - val raw_output_messages = new Event_Bus[Isabelle_Process.Output] - val all_messages = new Event_Bus[Isabelle_Process.Message] // potential bottle-neck - val trace_events = new Event_Bus[Simplifier_Trace.Event.type] - - - /** buffered command changes (delay_first discipline) **/ - - //{{{ - private case object Stop - - private val (_, commands_changed_buffer) = - Simple_Thread.actor("commands_changed_buffer", daemon = true) - { - var finished = false - while (!finished) { - receive { - case Stop => finished = true; reply(()) - case changed: Session.Commands_Changed => commands_changed.event(changed) - case bad => System.err.println("commands_changed_buffer: ignoring bad message " + bad) - } - } - } - //}}} - - - /** pipelined change parsing **/ - - //{{{ - private case class Text_Edits( - previous: Future[Document.Version], - doc_blobs: Document.Blobs, - text_edits: List[Document.Edit_Text], - version_result: Promise[Document.Version]) - - private val (_, change_parser) = Simple_Thread.actor("change_parser", daemon = true) - { - var finished = false - while (!finished) { - receive { - case Stop => finished = true; reply(()) - - case Text_Edits(previous, doc_blobs, text_edits, version_result) => - val prev = previous.get_finished - val (syntax_changed, doc_edits, version) = - Timing.timeit("text_edits", timing) { - resources.text_edits(reparse_limit, prev, doc_blobs, text_edits) - } - version_result.fulfill(version) - sender ! Change(doc_blobs, syntax_changed, doc_edits, prev, version) - - case bad => System.err.println("change_parser: ignoring bad message " + bad) - } - } - } - //}}} - - - - /** main protocol actor **/ - - /* global state */ - - private val syslog = Volatile(Queue.empty[XML.Elem]) - def current_syslog(): String = cat_lines(syslog().iterator.map(XML.content)) - - @volatile private var _phase: Session.Phase = Session.Inactive - private def phase_=(new_phase: Session.Phase) - { - _phase = new_phase - phase_changed.event(new_phase) - } - def phase = _phase - def is_ready: Boolean = phase == Session.Ready - - private val global_state = Volatile(Document.State.init) - def current_state(): Document.State = global_state() - - def recent_syntax(): Outer_Syntax = - { - val version = current_state().recent_finished.version.get_finished - if (version.is_init) resources.base_syntax - else version.syntax - } - - def snapshot(name: Document.Node.Name = Document.Node.Name.empty, - pending_edits: List[Text.Edit] = Nil): Document.Snapshot = - global_state().snapshot(name, pending_edits) - - - /* protocol handlers */ - - @volatile private var _protocol_handlers = new Session.Protocol_Handlers() - - def protocol_handler(name: String): Option[Session.Protocol_Handler] = - _protocol_handlers.get(name) - - - /* theory files */ - - def header_edit(name: Document.Node.Name, header: Document.Node.Header): Document.Edit_Text = - { - val header1 = - if (resources.loaded_theories(name.theory)) - header.error("Cannot update finished theory " + quote(name.theory)) - else header - (name, Document.Node.Deps(header1)) - } - - - /* actor messages */ - - private case class Start(args: List[String]) - private case class Cancel_Exec(exec_id: Document_ID.Exec) - private case class Change( - doc_blobs: Document.Blobs, - syntax_changed: Boolean, - doc_edits: List[Document.Edit_Command], - previous: Document.Version, - version: Document.Version) - private case class Protocol_Command(name: String, args: List[String]) - private case class Messages(msgs: List[Isabelle_Process.Message]) - private case class Update_Options(options: Options) - - private val (_, session_actor) = Simple_Thread.actor("session_actor", daemon = true) - { - val this_actor = self - - var prune_next = System.currentTimeMillis() + prune_delay.ms - - - /* buffered prover messages */ - - object receiver - { - private var buffer = new mutable.ListBuffer[Isabelle_Process.Message] - - private def flush(): Unit = synchronized { - if (!buffer.isEmpty) { - val msgs = buffer.toList - this_actor ! Messages(msgs) - buffer = new mutable.ListBuffer[Isabelle_Process.Message] - } - } - def invoke(msg: Isabelle_Process.Message): Unit = synchronized { - msg match { - case _: Isabelle_Process.Input => - buffer += msg - case output: Isabelle_Process.Protocol_Output if output.properties == Markup.Flush => - flush() - case output: Isabelle_Process.Output => - buffer += msg - if (output.is_syslog) - syslog >> (queue => - { - val queue1 = queue.enqueue(output.message) - if (queue1.length > syslog_limit) queue1.dequeue._2 else queue1 - }) - } - } - - private val timer = new Timer("session_actor.receiver", true) - timer.schedule(new TimerTask { def run = flush }, message_delay.ms, message_delay.ms) - - def cancel() { timer.cancel() } - } - - var prover: Option[Session.Prover] = None - - - /* delayed command changes */ - - object delay_commands_changed - { - private var changed_assignment: Boolean = false - private var changed_nodes: Set[Document.Node.Name] = Set.empty - private var changed_commands: Set[Command] = Set.empty - - private var flush_time: Option[Long] = None - - def flush_timeout: Long = - flush_time match { - case None => 5000L - case Some(time) => (time - System.currentTimeMillis()) max 0 - } - - def flush() - { - if (changed_assignment || !changed_nodes.isEmpty || !changed_commands.isEmpty) - commands_changed_buffer ! - Session.Commands_Changed(changed_assignment, changed_nodes, changed_commands) - changed_assignment = false - changed_nodes = Set.empty - changed_commands = Set.empty - flush_time = None - } - - def invoke(assign: Boolean, commands: List[Command]) - { - changed_assignment |= assign - for (command <- commands) { - changed_nodes += command.node_name - changed_commands += command - } - val now = System.currentTimeMillis() - flush_time match { - case None => flush_time = Some(now + output_delay.ms) - case Some(time) => if (now >= time) flush() - } - } - } - - - /* raw edits */ - - def handle_raw_edits(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text]) - //{{{ - { - prover.get.discontinue_execution() - - val previous = global_state().history.tip.version - val version = Future.promise[Document.Version] - val change = global_state >>> (_.continue_history(previous, edits, version)) - - raw_edits.event(Session.Raw_Edits(doc_blobs, edits)) - change_parser ! Text_Edits(previous, doc_blobs, edits, version) - } - //}}} - - - /* resulting changes */ - - def handle_change(change: Change) - //{{{ - { - val Change(doc_blobs, syntax_changed, doc_edits, previous, version) = change - - def id_command(command: Command) - { - for { - digest <- command.blobs_digests - if !global_state().defined_blob(digest) - } { - doc_blobs.get(digest) match { - case Some(blob) => - global_state >> (_.define_blob(digest)) - prover.get.define_blob(blob) - case None => - System.err.println("Missing blob for SHA1 digest " + digest) - } - } - - if (!global_state().defined_command(command.id)) { - global_state >> (_.define_command(command)) - prover.get.define_command(command) - } - } - doc_edits foreach { - case (_, edit) => - edit foreach { case (c1, c2) => c1 foreach id_command; c2 foreach id_command } - } - - val assignment = global_state().the_assignment(previous).check_finished - global_state >> (_.define_version(version, assignment)) - prover.get.update(previous.id, version.id, doc_edits) - - if (syntax_changed) resources.syntax_changed() - } - //}}} - - - /* prover output */ - - def handle_output(output: Isabelle_Process.Output) - //{{{ - { - def bad_output() - { - if (verbose) - System.err.println("Ignoring prover output: " + output.message.toString) - } - - def accumulate(state_id: Document_ID.Generic, message: XML.Elem) - { - try { - val st = global_state >>> (_.accumulate(state_id, message)) - delay_commands_changed.invoke(false, List(st.command)) - } - catch { - case _: Document.State.Fail => bad_output() - } - } - - output match { - case msg: Isabelle_Process.Protocol_Output => - val handled = _protocol_handlers.invoke(msg) - if (!handled) { - msg.properties match { - case Markup.Protocol_Handler(name) => - _protocol_handlers = _protocol_handlers.add(prover.get, name) - - case Protocol.Command_Timing(state_id, timing) => - val message = XML.elem(Markup.STATUS, List(XML.Elem(Markup.Timing(timing), Nil))) - accumulate(state_id, prover.get.xml_cache.elem(message)) - - case Markup.Assign_Update => - msg.text match { - case Protocol.Assign_Update(id, update) => - try { - val cmds = global_state >>> (_.assign(id, update)) - delay_commands_changed.invoke(true, cmds) - } - catch { case _: Document.State.Fail => bad_output() } - case _ => bad_output() - } - // FIXME separate timeout event/message!? - if (prover.isDefined && System.currentTimeMillis() > prune_next) { - val old_versions = global_state >>> (_.prune_history(prune_size)) - if (!old_versions.isEmpty) prover.get.remove_versions(old_versions) - prune_next = System.currentTimeMillis() + prune_delay.ms - } - - case Markup.Removed_Versions => - msg.text match { - case Protocol.Removed(removed) => - try { - global_state >> (_.removed_versions(removed)) - } - catch { case _: Document.State.Fail => bad_output() } - case _ => bad_output() - } - - case Markup.ML_Statistics(props) => - statistics.event(Session.Statistics(props)) - - case Markup.Task_Statistics(props) => - // FIXME - - case _ => bad_output() - } - } - case _ => - output.properties match { - case Position.Id(state_id) => - accumulate(state_id, output.message) - - case _ if output.is_init => - phase = Session.Ready - - case Markup.Return_Code(rc) if output.is_exit => - if (rc == 0) phase = Session.Inactive - else phase = Session.Failed - - case _ => raw_output_messages.event(output) - } - } - } - //}}} - - - /* main loop */ - - //{{{ - var finished = false - while (!finished) { - receiveWithin(delay_commands_changed.flush_timeout) { - case TIMEOUT => delay_commands_changed.flush() - - case Start(args) if prover.isEmpty => - if (phase == Session.Inactive || phase == Session.Failed) { - phase = Session.Startup - prover = Some(new Isabelle_Process(receiver.invoke _, args) with Protocol) - } - - case Stop => - if (phase == Session.Ready) { - _protocol_handlers = _protocol_handlers.stop(prover.get) - global_state >> (_ => Document.State.init) // FIXME event bus!? - phase = Session.Shutdown - prover.get.terminate - prover = None - phase = Session.Inactive - } - finished = true - receiver.cancel() - reply(()) - - case Update_Options(options) if prover.isDefined => - if (is_ready) { - prover.get.options(options) - handle_raw_edits(Document.Blobs.empty, Nil) - } - global_options.event(Session.Global_Options(options)) - reply(()) - - case Cancel_Exec(exec_id) if prover.isDefined => - prover.get.cancel_exec(exec_id) - - case Session.Raw_Edits(doc_blobs, edits) if prover.isDefined => - handle_raw_edits(doc_blobs, edits) - reply(()) - - case Session.Dialog_Result(id, serial, result) if prover.isDefined => - prover.get.dialog_result(serial, result) - handle_output(new Isabelle_Process.Output(Protocol.Dialog_Result(id, serial, result))) - - case Protocol_Command(name, args) if prover.isDefined => - prover.get.protocol_command(name, args:_*) - - case Messages(msgs) => - msgs foreach { - case input: Isabelle_Process.Input => - all_messages.event(input) - - case output: Isabelle_Process.Output => - if (output.is_stdout || output.is_stderr) raw_output_messages.event(output) - else handle_output(output) - if (output.is_syslog) syslog_messages.event(output) - all_messages.event(output) - } - - case change: Change - if prover.isDefined && global_state().is_assigned(change.previous) => - handle_change(change) - - case bad if !bad.isInstanceOf[Change] => - System.err.println("session_actor: ignoring bad message " + bad) - } - } - //}}} - } - - - /* actions */ - - def start(args: List[String]) - { - session_actor ! Start(args) - } - - def stop() - { - commands_changed_buffer !? Stop - change_parser !? Stop - session_actor !? Stop - } - - def protocol_command(name: String, args: String*) - { session_actor ! Protocol_Command(name, args.toList) } - - def cancel_exec(exec_id: Document_ID.Exec) { session_actor ! Cancel_Exec(exec_id) } - - def update(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text]) - { if (!edits.isEmpty) session_actor !? Session.Raw_Edits(doc_blobs, edits) } - - def update_options(options: Options) - { session_actor !? Update_Options(options) } - - def dialog_result(id: Document_ID.Generic, serial: Long, result: String) - { session_actor ! Session.Dialog_Result(id, serial, result) } -} diff -r 3c89e21d9be2 -r c7c85cdb725d src/Pure/build-jars --- a/src/Pure/build-jars Tue Mar 18 17:53:40 2014 +0100 +++ b/src/Pure/build-jars Tue Mar 18 18:09:31 2014 +0100 @@ -54,6 +54,7 @@ PIDE/protocol.scala PIDE/query_operation.scala PIDE/resources.scala + PIDE/session.scala PIDE/text.scala PIDE/xml.scala PIDE/yxml.scala @@ -67,7 +68,6 @@ System/isabelle_system.scala System/options.scala System/platform.scala - System/session.scala System/system_channel.scala System/utf8.scala Thy/html.scala