# HG changeset patch # User wenzelm # Date 1438885992 -7200 # Node ID 4c18d8e4fe149ece4f25b4973445b5ccb2e48c4e # Parent eb21ae05ec439acea96042ac91977bf2a1712e7c clarified debugger loop; more controls; diff -r eb21ae05ec43 -r 4c18d8e4fe14 src/Pure/Tools/debugger.ML --- a/src/Pure/Tools/debugger.ML Thu Aug 06 17:40:05 2015 +0200 +++ b/src/Pure/Tools/debugger.ML Thu Aug 06 20:33:12 2015 +0200 @@ -88,11 +88,14 @@ (* eval ML *) -fun eval opt_index SML context expression = (* FIXME *) - writeln_message ("context = " ^ context ^ "\nexpression = " ^ expression); +fun eval thread_name index SML context expression = (* FIXME *) + writeln_message ("SML = " ^ Markup.print_bool SML ^ + "\ncontext = " ^ context ^ "\nexpression = " ^ expression); -(* main entry point *) +(* debugger entry point *) + +local fun debugger_state thread_name = Output.protocol_message (Markup.debugger_state thread_name) @@ -103,19 +106,20 @@ |> let open XML.Encode in list (pair properties string) end |> YXML.string_of_body]; +fun debugger_command thread_name = + (case get_input thread_name of + ["continue"] => false + | ["eval", index, SML, txt1, txt2] => + (error_wrapper (fn () => + eval thread_name (Markup.parse_int index) (Markup.parse_bool SML) txt1 txt2); true) + | bad => + (Output.system_message + ("Debugger: bad input " ^ ML_Syntax.print_list ML_Syntax.print_string bad); true)); + fun debugger_loop thread_name = let fun loop () = - (debugger_state thread_name; - case get_input thread_name of - ["continue"] => () - | ["eval", index, language, context, expression] => - (error_wrapper (fn () => - eval (try Markup.parse_int index) (language = "SML") context expression); loop ()) - | bad => - (Output.system_message - ("Debugger: bad input " ^ ML_Syntax.print_list ML_Syntax.print_string bad); - loop ())); + (debugger_state thread_name; if debugger_command thread_name then loop () else ()); in with_debugging loop; debugger_state thread_name end; fun debugger cond = @@ -127,11 +131,15 @@ 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}))); +end; + (* protocol commands *) diff -r eb21ae05ec43 -r 4c18d8e4fe14 src/Pure/Tools/debugger.scala --- a/src/Pure/Tools/debugger.scala Thu Aug 06 17:40:05 2015 +0200 +++ b/src/Pure/Tools/debugger.scala Thu Aug 06 20:33:12 2015 +0200 @@ -127,10 +127,9 @@ def continue(thread_name: String): Unit = input(thread_name, "continue") - def eval(thread_name: String, opt_index: Option[Int], - language: String, context: String, expression: String): Unit = + def eval(thread_name: String, index: Int, SML: Boolean, context: String, expression: String): Unit = { - val index = opt_index.map(_.toString).getOrElse("") - input(thread_name, "eval", index, language, context, expression) + input(thread_name, "eval", + index.toString, SML.toString, Symbol.decode(context), Symbol.decode(expression)) } } diff -r eb21ae05ec43 -r 4c18d8e4fe14 src/Tools/jEdit/src/debugger_dockable.scala --- a/src/Tools/jEdit/src/debugger_dockable.scala Thu Aug 06 17:40:05 2015 +0200 +++ b/src/Tools/jEdit/src/debugger_dockable.scala Thu Aug 06 20:33:12 2015 +0200 @@ -15,7 +15,7 @@ import javax.swing.tree.{DefaultMutableTreeNode, DefaultTreeModel, TreeSelectionModel} import javax.swing.event.{TreeSelectionEvent, TreeSelectionListener} -import scala.swing.{Button, Label, Component, SplitPane, Orientation} +import scala.swing.{Button, Label, Component, SplitPane, Orientation, CheckBox} import scala.swing.event.ButtonClicked import org.gjt.sp.jedit.View @@ -188,6 +188,11 @@ setFont(GUI.imitate_font(getFont, Font_Info.main_family(), 1.2)) } + private val sml_button = new CheckBox("SML") { + tooltip = "Official Standard ML instead of Isabelle/ML" + selected = false + } + private val eval_button = new Button("Eval") { tooltip = "Evaluate Isabelle/ML expression within optional context" reactions += { case ButtonClicked(_) => eval_expression() } @@ -197,10 +202,9 @@ private def eval_expression() { tree_selection() match { - case Some((t, opt_index)) => - Debugger.eval(t.thread_name, opt_index, "ML", - Symbol.decode(context_field.getText), - Symbol.decode(expression_field.getText)) + case Some((t, opt_index)) if t.debug_states.nonEmpty => + Debugger.eval(t.thread_name, opt_index getOrElse 0, + sml_button.selected, context_field.getText, expression_field.getText) case _ => } } @@ -238,8 +242,8 @@ private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)( context_label, Component.wrap(context_field), - expression_label, Component.wrap(expression_field), eval_button, - continue_button, cancel_button, + expression_label, Component.wrap(expression_field), + sml_button, eval_button, continue_button, cancel_button, pretty_text_area.search_label, pretty_text_area.search_field, debugger_stepping, debugger_active, zoom) add(controls.peer, BorderLayout.NORTH)