# HG changeset patch # User wenzelm # Date 1438257739 -7200 # Node ID 6512bb0b1ff40fd68dad8a9aee9e184c4d9252af # Parent 781f1168d31effd018a960826234319fda6ed518 clarified management of (single) session; proper Debugger.Update events; diff -r 781f1168d31e -r 6512bb0b1ff4 src/Pure/PIDE/resources.scala --- a/src/Pure/PIDE/resources.scala Thu Jul 30 11:39:30 2015 +0200 +++ b/src/Pure/PIDE/resources.scala Thu Jul 30 14:02:19 2015 +0200 @@ -16,9 +16,10 @@ object Resources { def thy_path(path: Path): Path = path.ext("thy") + + val empty: Resources = new Resources(Set.empty, Map.empty, Outer_Syntax.empty) } - class Resources( val loaded_theories: Set[String], val known_theories: Map[String, Document.Node.Name], diff -r 781f1168d31e -r 6512bb0b1ff4 src/Pure/PIDE/session.scala --- a/src/Pure/PIDE/session.scala Thu Jul 30 11:39:30 2015 +0200 +++ b/src/Pure/PIDE/session.scala Thu Jul 30 14:02:19 2015 +0200 @@ -203,7 +203,7 @@ val syslog_messages = new Session.Outlet[Prover.Output](dispatcher) val raw_output_messages = new Session.Outlet[Prover.Output](dispatcher) val trace_events = new Session.Outlet[Simplifier_Trace.Event.type](dispatcher) - val debugger_events = new Session.Outlet[Debugger.Event.type](dispatcher) + val debugger_updates = new Session.Outlet[Debugger.Update](dispatcher) val all_messages = new Session.Outlet[Prover.Message](dispatcher) // potential bottle-neck! diff -r 781f1168d31e -r 6512bb0b1ff4 src/Pure/Tools/debugger.scala --- a/src/Pure/Tools/debugger.scala Thu Jul 30 11:39:30 2015 +0200 +++ b/src/Pure/Tools/debugger.scala Thu Jul 30 14:02:19 2015 +0200 @@ -11,7 +11,8 @@ { /* global state */ - case class State( + sealed case class State( + session: Session = new Session(Resources.empty), output: Map[String, Command.Results] = Map.empty) // thread name ~> output messages { def add_output(name: String, entry: Command.Results.Entry): State = @@ -22,42 +23,36 @@ def current_state(): State = global_state.value - /* GUI interaction */ - - case object Event - - - /* manager thread */ + /* protocol handler */ - private lazy val manager: Consumer_Thread[Any] = - Consumer_Thread.fork[Any]("Debugger.manager", daemon = true)( - consume = (arg: Any) => - { - // FIXME - true - }, - finish = () => - { - // FIXME - } - ) - - - /* protocol handler */ + sealed case class Update(thread_names: Set[String]) class Handler extends Session.Protocol_Handler { + private var updated = Set.empty[String] + private val delay_update = + Simple_Thread.delay_first(current_state().session.output_delay) { + current_state().session.debugger_updates.post(Update(updated)) + updated = Set.empty + } + private def update(name: String) + { + updated += name + delay_update.invoke() + } + private def debugger_output(prover: Prover, msg: Prover.Protocol_Output): Boolean = { msg.properties match { - case Markup.Debugger_Output(name) => + case Markup.Debugger_Output(thread_name) => val msg_body = prover.xml_cache.body( YXML.parse_body_failsafe(UTF8.decode_permissive(msg.bytes))) msg_body match { case List(XML.Elem(Markup(name, props @ Markup.Serial(i)), body)) => val message = XML.Elem(Markup(Markup.message(name), props), body) - global_state.change(_.add_output(name, i -> message)) + global_state.change(_.add_output(thread_name, i -> message)) + update(thread_name) true case _ => false } @@ -65,11 +60,6 @@ } } - override def stop(prover: Prover) - { - manager.shutdown() - } - val functions = Map(Markup.DEBUGGER_OUTPUT -> debugger_output _) } @@ -77,12 +67,15 @@ /* protocol commands */ - def init(session: Session): Unit = - session.protocol_command("Debugger.init") + def init(new_session: Session) + { + global_state.change(_.copy(session = new_session)) + current_state().session.protocol_command("Debugger.init") + } - def cancel(session: Session, name: String): Unit = - session.protocol_command("Debugger.cancel", name) + def cancel(name: String): Unit = + current_state().session.protocol_command("Debugger.cancel", name) - def input(session: Session, name: String, msg: String*): Unit = - session.protocol_command("Debugger.input", (name :: msg.toList):_*) + def input(name: String, msg: String*): Unit = + current_state().session.protocol_command("Debugger.input", (name :: msg.toList):_*) } diff -r 781f1168d31e -r 6512bb0b1ff4 src/Tools/jEdit/src/debugger_dockable.scala --- a/src/Tools/jEdit/src/debugger_dockable.scala Thu Jul 30 11:39:30 2015 +0200 +++ b/src/Tools/jEdit/src/debugger_dockable.scala Thu Jul 30 14:02:19 2015 +0200 @@ -109,23 +109,25 @@ private val main = Session.Consumer[Any](getClass.getName) { case _: Session.Global_Options => + Debugger.init(PIDE.session) GUI_Thread.later { handle_resize() } - case Debugger.Event => + case _: Debugger.Update => GUI_Thread.later { handle_update() } } override def init() { PIDE.session.global_options += main - PIDE.session.debugger_events += main + PIDE.session.debugger_updates += main + Debugger.init(PIDE.session) handle_update() } override def exit() { PIDE.session.global_options -= main - PIDE.session.debugger_events -= main + PIDE.session.debugger_updates -= main delay_resize.revoke() } diff -r 781f1168d31e -r 6512bb0b1ff4 src/Tools/jEdit/src/jedit_resources.scala --- a/src/Tools/jEdit/src/jedit_resources.scala Thu Jul 30 11:39:30 2015 +0200 +++ b/src/Tools/jEdit/src/jedit_resources.scala Thu Jul 30 14:02:19 2015 +0200 @@ -21,6 +21,12 @@ import org.gjt.sp.jedit.bufferio.BufferIORequest +object JEdit_Resources +{ + val empty: JEdit_Resources = + new JEdit_Resources(Set.empty, Map.empty, Outer_Syntax.empty) +} + class JEdit_Resources( loaded_theories: Set[String], known_theories: Map[String, Document.Node.Name], @@ -119,4 +125,3 @@ if (change.deps_changed && PIDE.options.bool("jedit_auto_load")) PIDE.deps_changed() } } - diff -r 781f1168d31e -r 6512bb0b1ff4 src/Tools/jEdit/src/plugin.scala --- a/src/Tools/jEdit/src/plugin.scala Thu Jul 30 11:39:30 2015 +0200 +++ b/src/Tools/jEdit/src/plugin.scala Thu Jul 30 14:02:19 2015 +0200 @@ -36,8 +36,7 @@ @volatile var startup_notified = false @volatile var plugin: Plugin = null - @volatile var session: Session = - new Session(new JEdit_Resources(Set.empty, Map.empty, Outer_Syntax.empty)) + @volatile var session: Session = new Session(JEdit_Resources.empty) def options_changed() { plugin.options_changed() } def deps_changed() { plugin.deps_changed() }