--- 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],
--- 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!
--- 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):_*)
}
--- 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()
}
--- 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()
}
}
-
--- 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() }