--- 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)))
--- 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 */
--- 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()
}
--- 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 _)
--- 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())
}
--- 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)(_ :+ _))
--- 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()
}
--- 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)
--- 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)
})
--- 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()
--- 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, _)))