# HG changeset patch # User wenzelm # Date 1439064523 -7200 # Node ID 6b7d10331b6b487efd78b4a49c66d2fcf4a27106 # Parent dd18c33c001e18201f056edf5a1d6e274c5f28f9# Parent 878e32cf3131f4c5344d36f9c53e24dd91149f39 merged diff -r dd18c33c001e -r 6b7d10331b6b src/Pure/Tools/debugger.ML --- a/src/Pure/Tools/debugger.ML Sat Aug 08 10:51:33 2015 +0200 +++ b/src/Pure/Tools/debugger.ML Sat Aug 08 22:08:43 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" diff -r dd18c33c001e -r 6b7d10331b6b src/Pure/Tools/debugger.scala --- a/src/Pure/Tools/debugger.scala Sat Aug 08 10:51:33 2015 +0200 +++ b/src/Pure/Tools/debugger.scala Sat Aug 08 22:08:43 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 = diff -r dd18c33c001e -r 6b7d10331b6b src/Tools/jEdit/src/debugger_dockable.scala --- a/src/Tools/jEdit/src/debugger_dockable.scala Sat Aug 08 10:51:33 2015 +0200 +++ b/src/Tools/jEdit/src/debugger_dockable.scala Sat Aug 08 22:08:43 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)