--- 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 *)
--- 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))
}
}
--- 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("<html><b>Eval</b></html>") {
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)