# 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("<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)