more robust debugger initialization, e.g. required for GUI components before actual session startup;
--- a/src/Pure/PIDE/rendering.scala Tue Mar 14 09:41:02 2017 +0100
+++ b/src/Pure/PIDE/rendering.scala Tue Mar 14 10:49:07 2017 +0100
@@ -472,14 +472,10 @@
Some(info + (r0, false, Pretty.block(XML.Text("ML:") :: Pretty.brk(1) :: body)))
case (info, Text.Info(r0, Protocol.ML_Breakpoint(breakpoint))) =>
- Debugger.get(session) match {
- case None => None
- case Some(debugger) =>
- val text =
- if (debugger.breakpoint_state(breakpoint)) "breakpoint (enabled)"
- else "breakpoint (disabled)"
- Some(info + (r0, true, XML.Text(text)))
- }
+ val text =
+ if (session.debugger.breakpoint_state(breakpoint)) "breakpoint (enabled)"
+ else "breakpoint (disabled)"
+ Some(info + (r0, true, XML.Text(text)))
case (info, Text.Info(r0, XML.Elem(Markup.Language(language, _, _, _), _))) =>
val lang = Word.implode(Word.explode('_', language))
Some(info + (r0, true, XML.Text("language: " + lang)))
--- a/src/Pure/PIDE/session.scala Tue Mar 14 09:41:02 2017 +0100
+++ b/src/Pure/PIDE/session.scala Tue Mar 14 10:49:07 2017 +0100
@@ -295,6 +295,14 @@
protocol_handlers.add(name)
+ /* debugger */
+
+ private val debugger_handler = new Debugger.Handler(this)
+ add_protocol_handler(debugger_handler)
+
+ def debugger: Debugger = debugger_handler.debugger
+
+
/* manager thread */
private val delay_prune =
--- a/src/Pure/Tools/debugger.ML Tue Mar 14 09:41:02 2017 +0100
+++ b/src/Pure/Tools/debugger.ML Tue Mar 14 10:49:07 2017 +0100
@@ -18,8 +18,6 @@
(* output messages *)
-val _ = Session.protocol_handler "isabelle.Debugger$Handler";
-
fun output_message kind msg =
if msg = "" then ()
else
--- a/src/Pure/Tools/debugger.scala Tue Mar 14 09:41:02 2017 +0100
+++ b/src/Pure/Tools/debugger.scala Tue Mar 14 10:49:07 2017 +0100
@@ -105,29 +105,9 @@
/* protocol handler */
- def get(session: Session): Option[Debugger] =
- session.get_protocol_handler("isabelle.Debugger$Handler") match {
- case Some(handler: Handler) => handler.get_debugger
- case _ => None
- }
-
- def apply(session: Session): Debugger =
- get(session) getOrElse error("Debugger not initialized")
-
- class Handler extends Session.Protocol_Handler
+ class Handler(session: Session) extends Session.Protocol_Handler
{
- private val _debugger_ = Synchronized[Option[Debugger]](None)
- def get_debugger: Option[Debugger] = _debugger_.value
- def the_debugger: Debugger = get_debugger getOrElse error("Debugger not initialized")
-
- override def init(session: Session)
- {
- _debugger_.change(
- {
- case None => Some(new Debugger(session))
- case Some(_) => error("Debugger already initialized")
- })
- }
+ val debugger: Debugger = new Debugger(session)
private def debugger_state(msg: Prover.Protocol_Output): Boolean =
{
@@ -142,7 +122,7 @@
case (pos, function) => Debug_State(pos, function)
})
}
- the_debugger.update_thread(thread_name, debug_states)
+ debugger.update_thread(thread_name, debug_states)
true
case _ => false
}
@@ -154,9 +134,8 @@
case Markup.Debugger_Output(thread_name) =>
YXML.parse_body_failsafe(Symbol.decode(UTF8.decode_permissive(msg.bytes))) match {
case List(XML.Elem(Markup(name, props @ Markup.Serial(i)), body)) =>
- val debugger = the_debugger
val message = XML.Elem(Markup(Markup.message(name), props), body)
- debugger.add_output(thread_name, i -> debugger.session.xml_cache.elem(message))
+ debugger.add_output(thread_name, i -> session.xml_cache.elem(message))
true
case _ => false
}
@@ -171,7 +150,7 @@
}
}
-class Debugger private(val session: Session)
+class Debugger private(session: Session)
{
/* debugger state */
--- a/src/Tools/jEdit/src/plugin.scala Tue Mar 14 09:41:02 2017 +0100
+++ b/src/Tools/jEdit/src/plugin.scala Tue Mar 14 10:49:07 2017 +0100
@@ -45,7 +45,7 @@
def resources(): JEdit_Resources =
session.resources.asInstanceOf[JEdit_Resources]
- def debugger: Debugger = Debugger(session)
+ def debugger: Debugger = session.debugger
def file_watcher(): File_Watcher =
if (plugin == null) File_Watcher.none else plugin.file_watcher