# HG changeset patch
# User wenzelm
# Date 1489433622 -3600
# Node ID 51c0f094dc0290a742f1034815ad2077d3c523fc
# Parent  fd6bc719c98b84c25b408939dde9bd6776b3a64f
proper local debugger state, depending on session;
tuned signature;

diff -r fd6bc719c98b -r 51c0f094dc02 src/Pure/PIDE/rendering.scala
--- a/src/Pure/PIDE/rendering.scala	Mon Mar 13 17:21:46 2017 +0100
+++ b/src/Pure/PIDE/rendering.scala	Mon Mar 13 20:33:42 2017 +0100
@@ -221,7 +221,7 @@
 abstract class Rendering(
   val snapshot: Document.Snapshot,
   val options: Options,
-  val resources: Resources)
+  val session: Session)
 {
   override def toString: String = "Rendering(" + snapshot.toString + ")"
 
@@ -448,7 +448,7 @@
             Some(info + (r0, true, XML.Text(txt1 + txt2)))
 
           case (info, Text.Info(r0, XML.Elem(Markup.Path(name), _))) =>
-            val file = resources.append_file(snapshot.node_name.master_dir, name)
+            val file = session.resources.append_file(snapshot.node_name.master_dir, name)
             val text =
               if (name == file) "file " + quote(file)
               else "path " + quote(name) + "\nfile " + quote(file)
@@ -472,11 +472,14 @@
             Some(info + (r0, false, Pretty.block(XML.Text("ML:") :: Pretty.brk(1) :: body)))
 
           case (info, Text.Info(r0, Protocol.ML_Breakpoint(breakpoint))) =>
-            val text =
-              if (Debugger.breakpoint_state(breakpoint)) "breakpoint (enabled)"
-              else "breakpoint (disabled)"
-            Some(info + (r0, true, XML.Text(text)))
-
+            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)))
+            }
           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 fd6bc719c98b -r 51c0f094dc02 src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Mon Mar 13 17:21:46 2017 +0100
+++ b/src/Pure/PIDE/session.scala	Mon Mar 13 20:33:42 2017 +0100
@@ -107,7 +107,7 @@
 
   abstract class Protocol_Handler
   {
-    def start(prover: Prover): Unit = {}
+    def start(session: Session, prover: Prover): Unit = {}
     def stop(prover: Prover): Unit = {}
     val functions: Map[String, (Prover, Prover.Protocol_Output) => Boolean]
   }
@@ -122,7 +122,7 @@
   {
     def get(name: String): Option[Protocol_Handler] = handlers.get(name)
 
-    def add(prover: Prover, handler: Protocol_Handler): Protocol_Handlers =
+    def add(session: Session, prover: Prover, handler: Protocol_Handler): Protocol_Handlers =
     {
       val name = handler.getClass.getName
 
@@ -137,7 +137,7 @@
 
       val (handlers2, functions2) =
         try {
-          handler.start(prover)
+          handler.start(session, prover)
 
           val new_functions =
             for ((a, f) <- handler.functions.toList) yield
@@ -349,7 +349,7 @@
     _protocol_handlers.value.get(name)
 
   def add_protocol_handler(handler: Session.Protocol_Handler): Unit =
-    _protocol_handlers.change(_.add(prover.get, handler))
+    _protocol_handlers.change(_.add(this, prover.get, handler))
 
 
   /* manager thread */
diff -r fd6bc719c98b -r 51c0f094dc02 src/Pure/Tools/debugger.scala
--- a/src/Pure/Tools/debugger.scala	Mon Mar 13 17:21:46 2017 +0100
+++ b/src/Pure/Tools/debugger.scala	Mon Mar 13 20:33:42 2017 +0100
@@ -12,11 +12,12 @@
 
 object Debugger
 {
-  /* context */
+  /* thread context */
 
-  sealed case class Debug_State(
-    pos: Position.T,
-    function: String)
+  case object Update
+
+  sealed case class Debug_State(pos: Position.T, function: String)
+  type Threads = SortedMap[String, List[Debug_State]]
 
   sealed case class Context(thread_name: String, debug_states: List[Debug_State], index: Int = 0)
   {
@@ -47,12 +48,10 @@
   }
 
 
-  /* global state */
-
-  type Threads = SortedMap[String, List[Debug_State]]
+  /* debugger state */
 
   sealed case class State(
-    session: Session = new Session(Resources.empty),  // implicit session
+    session: Session,
     active: Int = 0,  // active views
     break: Boolean = false,  // break at next possible breakpoint
     active_breakpoints: Set[Long] = Set.empty,  // explicit breakpoint state
@@ -60,12 +59,6 @@
     focus: Map[String, Context] = Map.empty,  // thread name ~> focus
     output: Map[String, Command.Results] = Map.empty)  // thread name ~> output messages
   {
-    def set_session(new_session: Session): State =
-    {
-      session.stop()
-      copy(session = new_session)
-    }
-
     def set_break(b: Boolean): State = copy(break = b)
 
     def is_active: Boolean = active > 0 && session.is_ready
@@ -109,23 +102,33 @@
       copy(output = output - thread_name)
   }
 
-  private val global_state = Synchronized(State())
-
-
-  /* update events */
-
-  case object Update
-
-  private val delay_update =
-    Standard_Thread.delay_first(global_state.value.session.output_delay) {
-      global_state.value.session.debugger_updates.post(Update)
-    }
-
 
   /* 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
   {
+    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 start(session: Session, prover: Prover)
+    {
+      _debugger_.change(
+        {
+          case None => Some(new Debugger(session))
+          case Some(_) => error("Debugger already initialized")
+        })
+    }
+
     private def debugger_state(prover: Prover, msg: Prover.Protocol_Output): Boolean =
     {
       msg.properties match {
@@ -139,8 +142,7 @@
               case (pos, function) => Debug_State(pos, function)
             })
           }
-          global_state.change(_.update_thread(thread_name, debug_states))
-          delay_update.invoke()
+          the_debugger.update_thread(thread_name, debug_states)
           true
         case _ => false
       }
@@ -156,8 +158,7 @@
           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(thread_name, i -> message))
-              delay_update.invoke()
+              the_debugger.add_output(thread_name, i -> message)
               true
             case _ => false
           }
@@ -170,101 +171,114 @@
         Markup.DEBUGGER_STATE -> debugger_state _,
         Markup.DEBUGGER_OUTPUT -> debugger_output _)
   }
+}
+
+class Debugger private(session: Session)
+{
+  /* debugger state */
+
+  private val state = Synchronized(Debugger.State(session))
+
+  private val delay_update =
+    Standard_Thread.delay_first(session.output_delay) {
+      session.debugger_updates.post(Debugger.Update)
+    }
 
 
   /* protocol commands */
 
-  def is_active(): Boolean = global_state.value.is_active
-
-  def init_session(session: Session)
+  def update_thread(thread_name: String, debug_states: List[Debugger.Debug_State])
   {
-    global_state.change(state =>
-    {
-      val state1 = state.set_session(session)
-      if (!state.session.is_ready && state1.session.is_ready && state1.is_active)
-        state1.session.protocol_command("Debugger.init")
-      state1
-    })
+    state.change(_.update_thread(thread_name, debug_states))
+    delay_update.invoke()
   }
 
+  def add_output(thread_name: String, entry: Command.Results.Entry)
+  {
+    state.change(_.add_output(thread_name, entry))
+    delay_update.invoke()
+  }
+
+  def is_active(): Boolean = state.value.is_active
+
   def init(): Unit =
-    global_state.change(state =>
+    state.change(st =>
     {
-      val state1 = state.inc_active
-      if (!state.is_active && state1.is_active)
-        state1.session.protocol_command("Debugger.init")
-      state1
+      val st1 = st.inc_active
+      if (!st.is_active && st1.is_active)
+        session.protocol_command("Debugger.init")
+      st1
     })
 
   def exit(): Unit =
-    global_state.change(state =>
+    state.change(st =>
     {
-      val state1 = state.dec_active
-      if (state.is_active && !state1.is_active)
-        state1.session.protocol_command("Debugger.exit")
-      state1
+      val st1 = st.dec_active
+      if (st.is_active && !st1.is_active)
+        session.protocol_command("Debugger.exit")
+      st1
     })
 
-  def is_break(): Boolean = global_state.value.break
+  def is_break(): Boolean = state.value.break
   def set_break(b: Boolean)
   {
-    global_state.change(state => {
-      val state1 = state.set_break(b)
-      state1.session.protocol_command("Debugger.break", b.toString)
-      state1
+    state.change(st => {
+      val st1 = st.set_break(b)
+      session.protocol_command("Debugger.break", b.toString)
+      st1
     })
     delay_update.invoke()
   }
 
   def active_breakpoint_state(breakpoint: Long): Option[Boolean] =
   {
-    val state = global_state.value
-    if (state.is_active) Some(state.active_breakpoints(breakpoint)) else None
+    val st = state.value
+    if (st.is_active) Some(st.active_breakpoints(breakpoint)) else None
   }
 
   def breakpoint_state(breakpoint: Long): Boolean =
-    global_state.value.active_breakpoints(breakpoint)
+    state.value.active_breakpoints(breakpoint)
 
   def toggle_breakpoint(command: Command, breakpoint: Long)
   {
-    global_state.change(state =>
-    {
-      val (breakpoint_state, state1) = state.toggle_breakpoint(breakpoint)
-      state1.session.protocol_command(
-        "Debugger.breakpoint",
-        Symbol.encode(command.node_name.node),
-        Document_ID(command.id),
-        Value.Long(breakpoint),
-        Value.Boolean(breakpoint_state))
-      state1
-    })
+    state.change(st =>
+      {
+        val (breakpoint_state, st1) = st.toggle_breakpoint(breakpoint)
+        session.protocol_command(
+          "Debugger.breakpoint",
+          Symbol.encode(command.node_name.node),
+          Document_ID(command.id),
+          Value.Long(breakpoint),
+          Value.Boolean(breakpoint_state))
+        st1
+      })
   }
 
-  def status(focus: Option[Context]): (Threads, List[XML.Tree]) =
+  def status(focus: Option[Debugger.Context]): (Debugger.Threads, List[XML.Tree]) =
   {
-    val state = global_state.value
+    val st = state.value
     val output =
       focus match {
         case None => Nil
         case Some(c) =>
           (for {
-            (thread_name, results) <- state.output
+            (thread_name, results) <- st.output
             if thread_name == c.thread_name
             (_, tree) <- results.iterator
           } yield tree).toList
       }
-    (state.threads, output)
+    (st.threads, output)
   }
 
-  def focus(): List[Context] = global_state.value.focus.toList.map(_._2)
-  def set_focus(c: Context)
+  def focus(): List[Debugger.Context] = state.value.focus.toList.map(_._2)
+  def set_focus(c: Debugger.Context)
   {
-    global_state.change(_.set_focus(c))
+    state.change(_.set_focus(c))
     delay_update.invoke()
   }
 
   def input(thread_name: String, msg: String*): Unit =
-    global_state.value.session.protocol_command("Debugger.input", (thread_name :: msg.toList):_*)
+    session.protocol_command("Debugger.input", (thread_name :: msg.toList):_*)
 
   def continue(thread_name: String): Unit = input(thread_name, "continue")
   def step(thread_name: String): Unit = input(thread_name, "step")
@@ -273,28 +287,28 @@
 
   def clear_output(thread_name: String)
   {
-    global_state.change(_.clear_output(thread_name))
+    state.change(_.clear_output(thread_name))
     delay_update.invoke()
   }
 
-  def eval(c: Context, SML: Boolean, context: String, expression: String)
+  def eval(c: Debugger.Context, SML: Boolean, context: String, expression: String)
   {
-    global_state.change(state => {
+    state.change(st => {
       input(c.thread_name, "eval", c.debug_index.getOrElse(0).toString,
         SML.toString, Symbol.encode(context), Symbol.encode(expression))
-      state.clear_output(c.thread_name)
+      st.clear_output(c.thread_name)
     })
     delay_update.invoke()
   }
 
-  def print_vals(c: Context, SML: Boolean, context: String)
+  def print_vals(c: Debugger.Context, SML: Boolean, context: String)
   {
     require(c.debug_index.isDefined)
 
-    global_state.change(state => {
+    state.change(st => {
       input(c.thread_name, "print_vals", c.debug_index.getOrElse(0).toString,
         SML.toString, Symbol.encode(context))
-      state.clear_output(c.thread_name)
+      st.clear_output(c.thread_name)
     })
     delay_update.invoke()
   }
diff -r fd6bc719c98b -r 51c0f094dc02 src/Pure/Tools/print_operation.scala
--- a/src/Pure/Tools/print_operation.scala	Mon Mar 13 17:21:46 2017 +0100
+++ b/src/Pure/Tools/print_operation.scala	Mon Mar 13 20:33:42 2017 +0100
@@ -35,7 +35,7 @@
       true
     }
 
-    override def start(prover: Prover): Unit =
+    override def start(session: Session, prover: Prover): Unit =
       prover.protocol_command(Markup.PRINT_OPERATIONS)
 
     val functions = Map(Markup.PRINT_OPERATIONS -> put _)
diff -r fd6bc719c98b -r 51c0f094dc02 src/Tools/VSCode/src/document_model.scala
--- a/src/Tools/VSCode/src/document_model.scala	Mon Mar 13 17:21:46 2017 +0100
+++ b/src/Tools/VSCode/src/document_model.scala	Mon Mar 13 20:33:42 2017 +0100
@@ -167,6 +167,6 @@
   def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits)
 
   def rendering(snapshot: Document.Snapshot): VSCode_Rendering =
-    new VSCode_Rendering(this, snapshot, resources)
+    new VSCode_Rendering(this, snapshot)
   def rendering(): VSCode_Rendering = rendering(snapshot())
 }
diff -r fd6bc719c98b -r 51c0f094dc02 src/Tools/VSCode/src/vscode_rendering.scala
--- a/src/Tools/VSCode/src/vscode_rendering.scala	Mon Mar 13 17:21:46 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Mon Mar 13 20:33:42 2017 +0100
@@ -63,11 +63,8 @@
     Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.CITATION)
 }
 
-class VSCode_Rendering(
-    val model: Document_Model,
-    snapshot: Document.Snapshot,
-    resources: VSCode_Resources)
-  extends Rendering(snapshot, resources.options, resources)
+class VSCode_Rendering(val model: Document_Model, snapshot: Document.Snapshot)
+  extends Rendering(snapshot, model.resources.options, model.session)
 {
   /* completion */
 
@@ -77,7 +74,7 @@
         model.content.try_get_text(complete_range) match {
           case Some(original) =>
             names.complete(complete_range, Completion.History.empty,
-                resources.unicode_symbols, original) match {
+                model.resources.unicode_symbols, original) match {
               case Some(result) =>
                 result.items.map(item =>
                   Protocol.CompletionItem(
@@ -111,7 +108,7 @@
       range = model.content.doc.range(text_range)
       (_, XML.Elem(Markup(name, _), body)) <- res.iterator
     } yield {
-      val message = resources.output_pretty_message(body)
+      val message = model.resources.output_pretty_message(body)
       val severity = VSCode_Rendering.message_severity.get(name)
       Protocol.Diagnostic(range, message, severity = severity)
     }).toList
@@ -143,7 +140,7 @@
   {
     val ranges =
       (for {
-        spell_checker <- resources.spell_checker.get.iterator
+        spell_checker <- model.resources.spell_checker.get.iterator
         spell_range <- spell_checker_ranges(model.content.text_range).iterator
         text <- model.content.try_get_text(spell_range).iterator
         info <- spell_checker.marked_words(spell_range.start, text).iterator
@@ -172,7 +169,7 @@
       yield {
         val range = model.content.doc.range(text_range)
         Protocol.DecorationOpts(range,
-          msgs.map(msg => Protocol.MarkedString(resources.output_pretty_tooltip(msg))))
+          msgs.map(msg => Protocol.MarkedString(model.resources.output_pretty_tooltip(msg))))
       }
     Protocol.Decoration(decoration.typ, content)
   }
@@ -189,7 +186,7 @@
     : Option[Line.Node_Range] =
   {
     for {
-      platform_path <- resources.source_file(source_name)
+      platform_path <- model.resources.source_file(source_name)
       file <-
         (try { Some(new JFile(platform_path).getCanonicalFile) }
          catch { case ERROR(_) => None })
@@ -197,7 +194,7 @@
     yield {
       Line.Node_Range(file.getPath,
         if (range.start > 0) {
-          resources.get_file_content(file) match {
+          model.resources.get_file_content(file) match {
             case Some(text) =>
               val chunk = Symbol.Text_Chunk(text)
               val doc = Line.Document(text)
@@ -240,7 +237,7 @@
       range, Nil, VSCode_Rendering.hyperlink_elements, _ =>
         {
           case (links, Text.Info(_, XML.Elem(Markup.Path(name), _))) =>
-            val file = resources.append_file(snapshot.node_name.master_dir, name)
+            val file = model.resources.append_file(snapshot.node_name.master_dir, name)
             Some(Line.Node_Range(file) :: links)
 
           case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
@@ -252,7 +249,7 @@
           case (links, Text.Info(info_range, XML.Elem(Markup.Citation(name), _))) =>
             val iterator =
               for {
-                Text.Info(entry_range, (entry, model)) <- resources.bibtex_entries_iterator
+                Text.Info(entry_range, (entry, model)) <- model.resources.bibtex_entries_iterator
                 if entry == name
               } yield Line.Node_Range(model.node_name.node, model.content.doc.range(entry_range))
             if (iterator.isEmpty) None else Some((links /: iterator)(_ :+ _))
diff -r fd6bc719c98b -r 51c0f094dc02 src/Tools/jEdit/src/debugger_dockable.scala
--- a/src/Tools/jEdit/src/debugger_dockable.scala	Mon Mar 13 17:21:46 2017 +0100
+++ b/src/Tools/jEdit/src/debugger_dockable.scala	Mon Mar 13 20:33:42 2017 +0100
@@ -34,7 +34,7 @@
   {
     GUI_Thread.require {}
 
-    Debugger.toggle_breakpoint(command, breakpoint)
+    PIDE.debugger.toggle_breakpoint(command, breakpoint)
     jEdit.propertiesChanged()
   }
 
@@ -55,7 +55,7 @@
   /* context menu */
 
   def context_menu(text_area: JEditTextArea, offset: Text.Offset): List[JMenuItem] =
-    if (Debugger.is_active() && get_breakpoint(text_area, offset).isDefined) {
+    if (PIDE.debugger.is_active() && get_breakpoint(text_area, offset).isDefined) {
       val context = jEdit.getActionContext()
       val name = "isabelle.toggle-breakpoint"
       List(new EnhancedMenuItem(context.getAction(name).getLabel, name, context))
@@ -94,7 +94,7 @@
     GUI_Thread.require {}
 
     val new_snapshot = PIDE.editor.current_node_snapshot(view).getOrElse(current_snapshot)
-    val (new_threads, new_output) = Debugger.status(tree_selection())
+    val (new_threads, new_output) = PIDE.debugger.status(tree_selection())
 
     if (new_threads != current_threads)
       update_tree(new_threads)
@@ -173,9 +173,9 @@
   {
     tree_selection() match {
       case Some(c) if c.stack_state.isDefined =>
-        Debugger.print_vals(c, sml_button.selected, context_field.getText)
+        PIDE.debugger.print_vals(c, sml_button.selected, context_field.getText)
       case Some(c) =>
-        Debugger.clear_output(c.thread_name)
+        PIDE.debugger.clear_output(c.thread_name)
       case None =>
     }
   }
@@ -207,28 +207,28 @@
 
   private val break_button = new CheckBox("Break") {
     tooltip = "Break running threads at next possible breakpoint"
-    selected = Debugger.is_break()
-    reactions += { case ButtonClicked(_) => Debugger.set_break(selected) }
+    selected = PIDE.debugger.is_break()
+    reactions += { case ButtonClicked(_) => PIDE.debugger.set_break(selected) }
   }
 
   private val continue_button = new Button("Continue") {
     tooltip = "Continue program on current thread, until next breakpoint"
-    reactions += { case ButtonClicked(_) => thread_selection().map(Debugger.continue(_)) }
+    reactions += { case ButtonClicked(_) => thread_selection().map(PIDE.debugger.continue(_)) }
   }
 
   private val step_button = new Button("Step") {
     tooltip = "Single-step in depth-first order"
-    reactions += { case ButtonClicked(_) => thread_selection().map(Debugger.step(_)) }
+    reactions += { case ButtonClicked(_) => thread_selection().map(PIDE.debugger.step(_)) }
   }
 
   private val step_over_button = new Button("Step over") {
     tooltip = "Single-step within this function"
-    reactions += { case ButtonClicked(_) => thread_selection().map(Debugger.step_over(_)) }
+    reactions += { case ButtonClicked(_) => thread_selection().map(PIDE.debugger.step_over(_)) }
   }
 
   private val step_out_button = new Button("Step out") {
     tooltip = "Single-step outside this function"
-    reactions += { case ButtonClicked(_) => thread_selection().map(Debugger.step_out(_)) }
+    reactions += { case ButtonClicked(_) => thread_selection().map(PIDE.debugger.step_out(_)) }
   }
 
   private val context_label = new Label("Context:") {
@@ -277,7 +277,7 @@
     expression_field.addCurrentToHistory()
     tree_selection() match {
       case Some(c) if c.debug_index.isDefined =>
-        Debugger.eval(c, sml_button.selected, context_field.getText, expression_field.getText)
+        PIDE.debugger.eval(c, sml_button.selected, context_field.getText, expression_field.getText)
       case _ =>
     }
   }
@@ -309,7 +309,7 @@
   private def update_focus()
   {
     for (c <- tree_selection()) {
-      Debugger.set_focus(c)
+      PIDE.debugger.set_focus(c)
       for {
         pos <- c.debug_position
         link <- PIDE.editor.hyperlink_position(false, current_snapshot, pos)
@@ -338,7 +338,7 @@
 
       case Debugger.Update =>
         GUI_Thread.later {
-          break_button.selected = Debugger.is_break()
+          break_button.selected = PIDE.debugger.is_break()
           handle_update()
         }
     }
@@ -347,7 +347,7 @@
   {
     PIDE.session.global_options += main
     PIDE.session.debugger_updates += main
-    Debugger.init()
+    PIDE.debugger.init()
     handle_update()
     jEdit.propertiesChanged()
   }
@@ -357,7 +357,7 @@
     PIDE.session.global_options -= main
     PIDE.session.debugger_updates -= main
     delay_resize.revoke()
-    Debugger.exit()
+    PIDE.debugger.exit()
     jEdit.propertiesChanged()
   }
 
diff -r fd6bc719c98b -r 51c0f094dc02 src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Mon Mar 13 17:21:46 2017 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala	Mon Mar 13 20:33:42 2017 +0100
@@ -439,7 +439,7 @@
   /* debugger */
 
   def toggle_breakpoint(text_area: JEditTextArea): Unit =
-    if (Debugger.is_active()) {
+    if (PIDE.debugger.is_active()) {
       for {
         (command, serial) <- Debugger_Dockable.get_breakpoint(text_area, text_area.getCaretPosition)
       } Debugger_Dockable.toggle_breakpoint(command, serial)
diff -r fd6bc719c98b -r 51c0f094dc02 src/Tools/jEdit/src/jedit_rendering.scala
--- a/src/Tools/jEdit/src/jedit_rendering.scala	Mon Mar 13 17:21:46 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_rendering.scala	Mon Mar 13 20:33:42 2017 +0100
@@ -158,7 +158,7 @@
 
 
 class JEdit_Rendering(snapshot: Document.Snapshot, options: Options)
-  extends Rendering(snapshot, options, PIDE.resources)
+  extends Rendering(snapshot, options, PIDE.session)
 {
   /* colors */
 
@@ -304,7 +304,7 @@
       range, Vector.empty, JEdit_Rendering.hyperlink_elements, _ =>
         {
           case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _))) =>
-            val file = resources.append_file(snapshot.node_name.master_dir, name)
+            val file = PIDE.resources.append_file(snapshot.node_name.master_dir, name)
             val link = PIDE.editor.hyperlink_file(true, file)
             Some(links :+ Text.Info(snapshot.convert(info_range), link))
 
@@ -456,7 +456,7 @@
     snapshot.select(range, JEdit_Rendering.bullet_elements, _ =>
       {
         case Text.Info(_, Protocol.ML_Breakpoint(breakpoint)) =>
-          Debugger.active_breakpoint_state(breakpoint).map(b =>
+          PIDE.debugger.active_breakpoint_state(breakpoint).map(b =>
             if (b) breakpoint_enabled_color else breakpoint_disabled_color)
         case _ => Some(bullet_color)
       })
diff -r fd6bc719c98b -r 51c0f094dc02 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Mon Mar 13 17:21:46 2017 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Mon Mar 13 20:33:42 2017 +0100
@@ -45,6 +45,8 @@
   def resources(): JEdit_Resources =
     session.resources.asInstanceOf[JEdit_Resources]
 
+  def debugger: Debugger = Debugger(session)
+
   def file_watcher(): File_Watcher =
     if (plugin == null) File_Watcher.none else plugin.file_watcher
 
@@ -248,7 +250,6 @@
         }
 
       case Session.Ready =>
-        Debugger.init_session(PIDE.session)
         PIDE.session.update_options(PIDE.options.value)
         PIDE.init_models()
 
diff -r fd6bc719c98b -r 51c0f094dc02 src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Mon Mar 13 17:21:46 2017 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Mon Mar 13 20:33:42 2017 +0100
@@ -371,7 +371,7 @@
     else {
       val debug_positions =
         (for {
-          c <- Debugger.focus().iterator
+          c <- PIDE.debugger.focus().iterator
           pos <- c.debug_position.iterator
         } yield pos).toList
       if (debug_positions.exists(PIDE.editor.is_hyperlink_position(rendering.snapshot, offset, _)))