# HG changeset patch
# User wenzelm
# Date 1489484947 -3600
# Node ID fb82535644834e1da0dbc63f87e872cb054777c5
# Parent  6af51a47545bbdc21a4708dad01eb6f5a63c1c94
more robust debugger initialization, e.g. required for GUI components before actual session startup;

diff -r 6af51a47545b -r fb8253564483 src/Pure/PIDE/rendering.scala
--- 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)))
diff -r 6af51a47545b -r fb8253564483 src/Pure/PIDE/session.scala
--- 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 =
diff -r 6af51a47545b -r fb8253564483 src/Pure/Tools/debugger.ML
--- 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
diff -r 6af51a47545b -r fb8253564483 src/Pure/Tools/debugger.scala
--- 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 */
 
diff -r 6af51a47545b -r fb8253564483 src/Tools/jEdit/src/plugin.scala
--- 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