--- a/src/Pure/Tools/debugger.ML Thu Aug 06 23:56:48 2015 +0200
+++ b/src/Pure/Tools/debugger.ML Sat Aug 08 21:33:11 2015 +0200
@@ -14,7 +14,9 @@
structure Debugger: DEBUGGER =
struct
-(* messages *)
+(** global state **)
+
+(* output messages *)
val _ = Session.protocol_handler "isabelle.Debugger$Handler";
@@ -35,7 +37,7 @@
else error_message (Runtime.exn_message exn);
-(* global state *)
+(* thread names and input *)
datatype state =
State of {
@@ -73,7 +75,10 @@
in SOME (msg, make_state (threads, input')) end));
-(* thread state *)
+
+(** thread state **)
+
+(* stack frame during debugging *)
local
val tag = Universal.tag () : ML_Debugger.state list Universal.tag;
@@ -97,8 +102,32 @@
else nth states index);
+(* flags for single-stepping *)
-(* eval ML *)
+datatype stepping = Stepping of bool * int; (*stepping enabled, stack depth limit*)
+
+local
+ val tag = Universal.tag () : stepping Universal.tag;
+in
+
+fun get_stepping () = the_default (Stepping (false, ~1)) (Thread.getLocal tag);
+fun put_stepping stepping = Thread.setLocal (tag, Stepping stepping);
+
+end;
+
+fun is_stepping () =
+ let
+ val stack = ML_Debugger.state (Thread.self ());
+ val Stepping (stepping, depth) = get_stepping ();
+ in stepping andalso (depth < 0 orelse length stack <= depth) end;
+
+fun step_stepping () = put_stepping (true, ~1);
+fun step_over_stepping () = put_stepping (true, length (get_debugging ()));
+fun step_out_stepping () = put_stepping (true, length (get_debugging ()) - 1);
+fun continue_stepping () = put_stepping (false, ~1);
+
+
+(** eval ML **)
local
@@ -144,7 +173,8 @@
end;
-(* debugger entry point *)
+
+(** debugger entry point **)
local
@@ -159,7 +189,10 @@
fun debugger_command thread_name =
(case get_input thread_name of
- ["continue"] => false
+ ["step"] => (step_stepping (); false)
+ | ["step_over"] => (step_over_stepping (); false)
+ | ["step_out"] => (step_out_stepping (); false)
+ | ["continue"] => (continue_stepping (); false)
| ["eval", index, SML, txt1, txt2] =>
(error_wrapper (fn () =>
eval thread_name (Markup.parse_int index) (Markup.parse_bool SML) txt1 txt2); true)
@@ -173,26 +206,26 @@
(debugger_state thread_name; if debugger_command thread_name then loop () else ());
in with_debugging loop; debugger_state thread_name end;
-fun debugger cond =
- if is_debugging () orelse not (cond ()) orelse
- not (Options.default_bool @{system_option ML_debugger_active})
- then ()
- else
- (case Simple_Thread.get_name () of
- NONE => ()
- | SOME thread_name => debugger_loop thread_name);
-
in
fun init () =
ML_Debugger.on_breakpoint
- (SOME (fn (_, b) =>
- debugger (fn () => ! b orelse Options.default_bool @{system_option ML_debugger_stepping})));
+ (SOME (fn (_, break) =>
+ if not (is_debugging ()) andalso
+ (! break orelse Options.default_bool @{system_option ML_debugger_stepping} orelse
+ is_stepping ()) andalso
+ Options.default_bool @{system_option ML_debugger_active}
+ then
+ (case Simple_Thread.get_name () of
+ SOME thread_name => debugger_loop thread_name
+ | NONE => ())
+ else ()));
end;
-(* protocol commands *)
+
+(** protocol commands **)
val _ =
Isabelle_Process.protocol_command "Debugger.init"
--- a/src/Pure/Tools/debugger.scala Thu Aug 06 23:56:48 2015 +0200
+++ b/src/Pure/Tools/debugger.scala Sat Aug 08 21:33:11 2015 +0200
@@ -126,6 +126,9 @@
def input(thread_name: String, msg: String*): Unit =
current_state().session.protocol_command("Debugger.input", (thread_name :: msg.toList):_*)
+ def step(thread_name: String): Unit = input(thread_name, "step")
+ def step_over(thread_name: String): Unit = input(thread_name, "step_over")
+ def step_out(thread_name: String): Unit = input(thread_name, "step_out")
def continue(thread_name: String): Unit = input(thread_name, "continue")
def eval(thread_name: String, index: Int, SML: Boolean, context: String, expression: String): Unit =
--- a/src/Tools/jEdit/src/debugger_dockable.scala Thu Aug 06 23:56:48 2015 +0200
+++ b/src/Tools/jEdit/src/debugger_dockable.scala Sat Aug 08 21:33:11 2015 +0200
@@ -226,27 +226,30 @@
}
}
+ private val step_button = new Button("Step") {
+ tooltip = "Single-step in depth-first order"
+ reactions += { case ButtonClicked(_) => thread_selection().map(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(_)) }
+ }
+
+ private val step_out_button = new Button("Step out") {
+ tooltip = "Single-step outside this function"
+ reactions += { case ButtonClicked(_) => thread_selection().map(Debugger.step_out(_)) }
+ }
+
private val continue_button = new Button("Continue") {
- tooltip = "Continue program on current thread, until next breakpoint"
- reactions += {
- case ButtonClicked(_) =>
- tree_selection() match {
- case Some((t, _)) => Debugger.continue(t.thread_name)
- case _ =>
- }
- }
- }
+ tooltip = "Continue program on current thread, until next breakpoint"
+ reactions += { case ButtonClicked(_) => thread_selection().map(Debugger.continue(_)) }
+ }
private val cancel_button = new Button("Cancel") {
- tooltip = "Interrupt program on current thread"
- reactions += {
- case ButtonClicked(_) =>
- tree_selection() match {
- case Some((t, _)) => Debugger.cancel(t.thread_name)
- case _ =>
- }
- }
- }
+ tooltip = "Interrupt program on current thread"
+ reactions += { case ButtonClicked(_) => thread_selection().map(Debugger.cancel(_)) }
+ }
private val debugger_active =
new JEdit_Options.Check_Box("ML_debugger_active", "Active", "Enable debugger at run-time")
@@ -258,9 +261,10 @@
private val controls =
new Wrap_Panel(Wrap_Panel.Alignment.Right)(
+ step_button, step_over_button, step_out_button, continue_button, cancel_button,
context_label, Component.wrap(context_field),
expression_label, Component.wrap(expression_field),
- sml_button, eval_button, continue_button, cancel_button,
+ sml_button, eval_button,
pretty_text_area.search_label, pretty_text_area.search_field,
debugger_stepping, debugger_active, zoom)
add(controls.peer, BorderLayout.NORTH)