# HG changeset patch # User wenzelm # Date 1439341621 -7200 # Node ID 2986137093c6571af30635374ea1a69b880bb8e5 # Parent 3db3f4154e186f54648243295222ed9e45e4c094# Parent f39d004f2ff407c7f40a6c652f599de8c8679cfd merged diff -r 3db3f4154e18 -r 2986137093c6 src/Pure/Concurrent/future.ML --- a/src/Pure/Concurrent/future.ML Wed Aug 12 10:15:18 2015 +1000 +++ b/src/Pure/Concurrent/future.ML Wed Aug 12 03:07:01 2015 +0200 @@ -429,12 +429,14 @@ let val result = Single_Assignment.var "future" : 'a result; val pos = Position.thread_data (); + val context = Context.thread_data (); fun job ok = let val res = if ok then Exn.capture (fn () => - Multithreading.with_attributes atts (fn _ => Position.setmp_thread_data pos e ())) () + Multithreading.with_attributes atts (fn _ => + (Position.setmp_thread_data pos o Context.setmp_thread_data context) e ())) () else Exn.interrupt_exn; in assign_result group result (identify_result pos res) end; in (result, job) end; diff -r 3db3f4154e18 -r 2986137093c6 src/Pure/ML/ml_compiler_polyml.ML --- a/src/Pure/ML/ml_compiler_polyml.ML Wed Aug 12 10:15:18 2015 +1000 +++ b/src/Pure/ML/ml_compiler_polyml.ML Wed Aug 12 03:07:01 2015 +0200 @@ -12,6 +12,17 @@ (* parse trees *) +fun breakpoint_position loc = + let val pos = Position.reset_range (Exn_Properties.position_of loc) in + (case Position.offset_of pos of + NONE => pos + | SOME 1 => pos + | SOME j => + Position.properties_of pos + |> Properties.put (Markup.offsetN, Markup.print_int (j - 1)) + |> Position.of_properties) + end; + fun report_parse_tree redirect depth space parse_tree = let val is_visible = @@ -90,7 +101,7 @@ | breakpoints loc pt = (case ML_Parse_Tree.breakpoint pt of SOME b => - let val pos = Position.reset_range (Exn_Properties.position_of loc) in + let val pos = breakpoint_position loc in if is_reported pos then let val id = serial (); in cons ((pos, Markup.ML_breakpoint id), (id, (b, pos))) end diff -r 3db3f4154e18 -r 2986137093c6 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Wed Aug 12 10:15:18 2015 +1000 +++ b/src/Pure/ROOT.ML Wed Aug 12 03:07:01 2015 +0200 @@ -85,7 +85,15 @@ use "General/change_table.ML"; use "General/graph.ML"; + +(* fundamental structures *) + +use "name.ML"; +use "term.ML"; +use "context.ML"; +use "context_position.ML"; use "System/options.ML"; +use "config.ML"; (* concurrency within the ML runtime *) @@ -132,15 +140,6 @@ use "PIDE/active.ML"; -(* fundamental structures *) - -use "name.ML"; -use "term.ML"; -use "context.ML"; -use "context_position.ML"; -use "config.ML"; - - (* inner syntax *) use "Syntax/type_annotation.ML"; diff -r 3db3f4154e18 -r 2986137093c6 src/Pure/Tools/debugger.scala --- a/src/Pure/Tools/debugger.scala Wed Aug 12 10:15:18 2015 +1000 +++ b/src/Pure/Tools/debugger.scala Wed Aug 12 03:07:01 2015 +0200 @@ -26,7 +26,7 @@ def set_session(new_session: Session): State = copy(session = new_session) - def is_active: Boolean = active > 0 + def is_active: Boolean = active > 0 && session.is_ready def inc_active: State = copy(active = active + 1) def dec_active: State = copy(active = active - 1) @@ -123,12 +123,20 @@ /* protocol commands */ - def set_session(session: Session): Unit = - global_state.change(_.set_session(session)) - def is_active(): Boolean = global_state.value.is_active - def inc_active(): Unit = + def init_session(session: Session) + { + 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 + }) + } + + def init(): Unit = global_state.change(state => { val state1 = state.inc_active @@ -137,7 +145,7 @@ state1 }) - def dec_active(): Unit = + def exit(): Unit = global_state.change(state => { val state1 = state.dec_active @@ -149,7 +157,7 @@ def active_breakpoint_state(breakpoint: Long): Option[Boolean] = { val state = global_state.value - if (state.active > 0) Some(state.active_breakpoints(breakpoint)) else None + if (state.is_active) Some(state.active_breakpoints(breakpoint)) else None } def breakpoint_state(breakpoint: Long): Boolean = diff -r 3db3f4154e18 -r 2986137093c6 src/Tools/jEdit/etc/options --- a/src/Tools/jEdit/etc/options Wed Aug 12 10:15:18 2015 +1000 +++ b/src/Tools/jEdit/etc/options Wed Aug 12 03:07:01 2015 +0200 @@ -100,8 +100,8 @@ option spell_checker_color : string = "0000FFFF" option bad_color : string = "FF6A6A64" option intensify_color : string = "FFCC6664" -option breakpoint_color : string = "00CC0014" -option breakpoint_active_color : string = "00CC0032" +option breakpoint_disabled_color : string = "CCCC0080" +option breakpoint_enabled_color : string = "FF9966FF" option quoted_color : string = "8B8B8B19" option antiquoted_color : string = "FFC83219" option antiquote_color : string = "6600CCFF" diff -r 3db3f4154e18 -r 2986137093c6 src/Tools/jEdit/src/debugger_dockable.scala --- a/src/Tools/jEdit/src/debugger_dockable.scala Wed Aug 12 10:15:18 2015 +1000 +++ b/src/Tools/jEdit/src/debugger_dockable.scala Wed Aug 12 03:07:01 2015 +0200 @@ -343,7 +343,6 @@ private val main = Session.Consumer[Any](getClass.getName) { case _: Session.Global_Options => - Debugger.set_session(PIDE.session) GUI_Thread.later { handle_resize() } case Debugger.Update => @@ -354,8 +353,7 @@ { PIDE.session.global_options += main PIDE.session.debugger_updates += main - Debugger.set_session(PIDE.session) - Debugger.inc_active() + Debugger.init() handle_update() jEdit.propertiesChanged() } @@ -366,7 +364,7 @@ PIDE.session.debugger_updates -= main delay_resize.revoke() update_focus(None) - Debugger.dec_active() + Debugger.exit() jEdit.propertiesChanged() } diff -r 3db3f4154e18 -r 2986137093c6 src/Tools/jEdit/src/plugin.scala --- a/src/Tools/jEdit/src/plugin.scala Wed Aug 12 10:15:18 2015 +1000 +++ b/src/Tools/jEdit/src/plugin.scala Wed Aug 12 03:07:01 2015 +0200 @@ -262,6 +262,7 @@ } case Session.Ready => + Debugger.init_session(PIDE.session) PIDE.session.update_options(PIDE.options.value) PIDE.init_models() diff -r 3db3f4154e18 -r 2986137093c6 src/Tools/jEdit/src/rendering.scala --- a/src/Tools/jEdit/src/rendering.scala Wed Aug 12 10:15:18 2015 +1000 +++ b/src/Tools/jEdit/src/rendering.scala Wed Aug 12 03:07:01 2015 +0200 @@ -204,14 +204,14 @@ Markup.STATE_MESSAGE + Markup.INFORMATION_MESSAGE + Markup.TRACING_MESSAGE + Markup.WARNING_MESSAGE + Markup.LEGACY_MESSAGE + Markup.ERROR_MESSAGE + - Markup.BAD + Markup.INTENSIFY + Markup.ML_BREAKPOINT ++ active_elements + Markup.BAD + Markup.INTENSIFY ++ active_elements private val foreground_elements = Markup.Elements(Markup.STRING, Markup.ALT_STRING, Markup.VERBATIM, Markup.CARTOUCHE, Markup.ANTIQUOTED) private val bullet_elements = - Markup.Elements(Markup.BULLET) + Markup.Elements(Markup.BULLET, Markup.ML_BREAKPOINT) private val fold_depth_elements = Markup.Elements(Markup.TEXT_FOLD, Markup.GOAL, Markup.SUBGOAL) @@ -249,8 +249,8 @@ val spell_checker_color = color_value("spell_checker_color") val bad_color = color_value("bad_color") val intensify_color = color_value("intensify_color") - val breakpoint_color = color_value("breakpoint_color") - val breakpoint_active_color = color_value("breakpoint_active_color") + val breakpoint_disabled_color = color_value("breakpoint_disabled_color") + val breakpoint_enabled_color = color_value("breakpoint_enabled_color") val quoted_color = color_value("quoted_color") val antiquoted_color = color_value("antiquoted_color") val antiquote_color = color_value("antiquote_color") @@ -680,9 +680,6 @@ Some((Nil, Some(bad_color))) case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) => Some((Nil, Some(intensify_color))) - case (_, Text.Info(_, Protocol.ML_Breakpoint(breakpoint))) => - Debugger.active_breakpoint_state(breakpoint).map(active => - (Nil, Some(if (active) breakpoint_active_color else breakpoint_color))) case (acc, Text.Info(_, Protocol.Dialog(_, serial, result))) => command_states.collectFirst( { case st if st.results.defined(serial) => st.results.get(serial).get }) match @@ -774,7 +771,13 @@ /* virtual bullets */ def bullet(range: Text.Range): List[Text.Info[Color]] = - snapshot.select(range, Rendering.bullet_elements, _ => _ => Some(bullet_color)) + snapshot.select(range, Rendering.bullet_elements, _ => + { + case Text.Info(_, Protocol.ML_Breakpoint(breakpoint)) => + Debugger.active_breakpoint_state(breakpoint).map(b => + if (b) breakpoint_enabled_color else breakpoint_disabled_color) + case _ => Some(bullet_color) + }) /* text folds */ diff -r 3db3f4154e18 -r 2986137093c6 src/Tools/jEdit/src/rich_text_area.scala --- a/src/Tools/jEdit/src/rich_text_area.scala Wed Aug 12 10:15:18 2015 +1000 +++ b/src/Tools/jEdit/src/rich_text_area.scala Wed Aug 12 03:07:01 2015 +0200 @@ -463,16 +463,6 @@ if (line != -1) { val line_range = Text.Range(start(i), end(i) min buffer.getLength) - // bullet bar - for { - Text.Info(range, color) <- rendering.bullet(line_range) - r <- JEdit_Lib.gfx_range(text_area, range) - } { - gfx.setColor(color) - gfx.fillRect(r.x + bullet_x, y + i * line_height + bullet_y, - r.length - bullet_w, line_height - bullet_h) - } - // text chunks val screen_line = first_line + i val chunks = text_area.getChunksOfScreenLine(screen_line) @@ -486,6 +476,16 @@ screen_line, line, start(i), end(i), y + line_height * i) } finally { gfx.setClip(clip) } } + + // bullet bar + for { + Text.Info(range, color) <- rendering.bullet(line_range) + r <- JEdit_Lib.gfx_range(text_area, range) + } { + gfx.setColor(color) + gfx.fillRect(r.x + bullet_x, y + i * line_height + bullet_y, + r.length - bullet_w, line_height - bullet_h) + } } y0 += line_height }