# HG changeset patch
# User wenzelm
# Date 1438875605 -7200
# Node ID eb21ae05ec439acea96042ac91977bf2a1712e7c
# Parent  6449ae4b85f9d844c5c75cfb85877a14da38fd30
clarified thread state;
support for eval operation;

diff -r 6449ae4b85f9 -r eb21ae05ec43 src/Pure/Tools/debugger.ML
--- a/src/Pure/Tools/debugger.ML	Thu Aug 06 14:29:05 2015 +0200
+++ b/src/Pure/Tools/debugger.ML	Thu Aug 06 17:40:05 2015 +0200
@@ -16,6 +16,8 @@
 
 (* messages *)
 
+val _ = Session.protocol_handler "isabelle.Debugger$Handler";
+
 fun output_message kind msg =
   Output.protocol_message
     (Markup.debugger_output (Simple_Thread.the_name ()))
@@ -25,6 +27,11 @@
 val warning_message = output_message Markup.warningN;
 val error_message = output_message Markup.errorN;
 
+fun error_wrapper e = e ()
+  handle exn =>
+    if Exn.is_interrupt exn then reraise exn
+    else error_message (Runtime.exn_message exn);
+
 
 (* global state *)
 
@@ -64,29 +71,32 @@
         in SOME (msg, make_state (threads, input')) end));
 
 
-(* thread data *)
+(* thread state *)
+
+local
+  val tag = Universal.tag () : ML_Debugger.state list Universal.tag;
+in
 
-local val tag = Universal.tag () : ML_Debugger.state list Universal.tag in
+fun get_debugging () = the_default [] (Thread.getLocal tag);
+val is_debugging = not o null o get_debugging;
 
-fun get_data () = the_default [] (Thread.getLocal tag);
-fun setmp_data data f x = setmp_thread_data tag (get_data ()) data f x;
+fun with_debugging e =
+  setmp_thread_data tag (get_debugging ()) (ML_Debugger.state (Thread.self ())) e ();
 
 end;
 
-val debugging = not o null o get_data;
-fun with_debugging e = setmp_data (ML_Debugger.state (Thread.self ())) e ();
 
+(* eval ML *)
 
-(* protocol messages *)
-
-val _ = Session.protocol_handler "isabelle.Debugger$Handler";
+fun eval opt_index SML context expression =  (* FIXME *)
+  writeln_message ("context = " ^ context ^ "\nexpression = " ^ expression);
 
 
 (* main entry point *)
 
 fun debugger_state thread_name =
   Output.protocol_message (Markup.debugger_state thread_name)
-   [get_data ()
+   [get_debugging ()
     |> map (fn st =>
       (Position.properties_of (Exn_Properties.position_of (ML_Debugger.debug_location st)),
        ML_Debugger.debug_function st))
@@ -94,23 +104,28 @@
     |> YXML.string_of_body];
 
 fun debugger_loop thread_name =
-  (debugger_state thread_name;
-   case get_input thread_name of
-    ["continue"] => ()
-  | bad =>
-     (Output.system_message
-        ("Debugger: bad input " ^ ML_Syntax.print_list ML_Syntax.print_string bad);
-      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 ()));
+  in with_debugging loop; debugger_state thread_name end;
 
 fun debugger cond =
-  if debugging () orelse not (cond ()) orelse
+  if is_debugging () orelse not (cond ()) orelse
     not (Options.default_bool @{system_option ML_debugger_active})
   then ()
   else
-    with_debugging (fn () =>
-      (case Simple_Thread.get_name () of
-        NONE => ()
-      | SOME thread_name => debugger_loop thread_name));
+    (case Simple_Thread.get_name () of
+      NONE => ()
+    | SOME thread_name => debugger_loop thread_name);
 
 fun init () =
   ML_Debugger.on_breakpoint
diff -r 6449ae4b85f9 -r eb21ae05ec43 src/Pure/Tools/debugger.scala
--- a/src/Pure/Tools/debugger.scala	Thu Aug 06 14:29:05 2015 +0200
+++ b/src/Pure/Tools/debugger.scala	Thu Aug 06 17:40:05 2015 +0200
@@ -126,4 +126,11 @@
     current_state().session.protocol_command("Debugger.input", (thread_name :: msg.toList):_*)
 
   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 =
+  {
+    val index = opt_index.map(_.toString).getOrElse("")
+    input(thread_name, "eval", index, language, context, expression)
+  }
 }
diff -r 6449ae4b85f9 -r eb21ae05ec43 src/Tools/jEdit/src/debugger_dockable.scala
--- a/src/Tools/jEdit/src/debugger_dockable.scala	Thu Aug 06 14:29:05 2015 +0200
+++ b/src/Tools/jEdit/src/debugger_dockable.scala	Thu Aug 06 17:40:05 2015 +0200
@@ -196,9 +196,13 @@
 
   private def eval_expression()
   {
-    // FIXME
-    Output.writeln("eval context = " + quote(context_field.getText) + " expression = " +
-      quote(expression_field.getText))
+    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 _ =>
+    }
   }
 
   private val continue_button = new Button("Continue") {