# 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, _)))