--- 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;
--- 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
--- 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";
--- 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 =
--- 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"
--- 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()
}
--- 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()
--- 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 */
--- 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
}