print values for stack entry;

--- a/src/Pure/ML-Systems/ml_name_space.ML	Tue Aug 11 18:42:29 2015 +0200
+++ b/src/Pure/ML-Systems/ml_name_space.ML	Tue Aug 11 20:05:27 2015 +0200
@@ -63,4 +63,6 @@
 
 fun forget_global_structure (_: string) = ();
 
+fun display_val (_, _: int, _: T) = ML_Pretty.String ("?", 1);
+
 end;

--- a/src/Pure/ML-Systems/polyml.ML	Tue Aug 11 18:42:29 2015 +0200
+++ b/src/Pure/ML-Systems/polyml.ML	Tue Aug 11 20:05:27 2015 +0200
@@ -4,23 +4,9 @@
 Compatibility wrapper for Poly/ML.
 *)
 
-(* ML name space *)
-
-structure ML_Name_Space =
-struct
-  open PolyML.NameSpace;
-  type T = PolyML.NameSpace.nameSpace;
-  val global = PolyML.globalNameSpace;
-  val initial_val =
-    List.filter (fn (a, _) => a <> "use" andalso a <> "exit" andalso a <> "commit")
-      (#allVal global ());
-  val initial_type = #allType global ();
-  val initial_fixity = #allFix global ();
-  val initial_structure = #allStruct global ();
-  val initial_signature = #allSig global ();
-  val initial_functor = #allFunct global ();
-  val forget_global_structure = PolyML.Compiler.forgetStructure;
-end;
+val ml_initial_val =
+  List.filter (fn (a, _) => a <> "use" andalso a <> "exit" andalso a <> "commit")
+    (#allVal PolyML.globalNameSpace ());
 
 
 (* ML system operations *)
@@ -120,33 +106,6 @@
 val pointer_eq = PolyML.pointerEq;
 
 
-(* ML compiler *)
-
-use "ML-Systems/use_context.ML";
-use "ML-Systems/ml_positions.ML";
-use "ML-Systems/compiler_polyml.ML";
-
-PolyML.Compiler.reportUnreferencedIds := true;
-PolyML.Compiler.printInAlphabeticalOrder := false;
-PolyML.Compiler.maxInlineSize := 80;
-
-fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2);
-
-use "ML-Systems/ml_parse_tree.ML";
-if ML_System.name = "polyml-5.5.3"
-then use "ML-Systems/ml_parse_tree_polyml-5.5.3.ML" else ();
-
-use "ML-Systems/ml_compiler_parameters.ML";
-if ML_System.name = "polyml-5.5.3"
-then use "ML-Systems/ml_compiler_parameters_polyml-5.5.3.ML" else ();
-
-
-(* ML debugger *)
-
-use "ML-Systems/ml_debugger.ML";
-if ML_System.name = "polyml-5.5.3" then use "ML-Systems/ml_debugger_polyml-5.5.3.ML" else ();
-
-
 (* ML toplevel pretty printing *)
 
 use "ML-Systems/ml_pretty.ML";
@@ -195,6 +154,42 @@
       else PolyML.PrettyBlock
         (0, false, [PolyML.ContextProperty ("length", Int.toString len)], [PolyML.PrettyString s]);
 
+
+(* ML compiler *)
+
+structure ML_Name_Space =
+struct
+  open PolyML.NameSpace;
+  type T = PolyML.NameSpace.nameSpace;
+  val global = PolyML.globalNameSpace;
+  val initial_val = ml_initial_val;
+  val initial_type = #allType global ();
+  val initial_fixity = #allFix global ();
+  val initial_structure = #allStruct global ();
+  val initial_signature = #allSig global ();
+  val initial_functor = #allFunct global ();
+  val forget_global_structure = PolyML.Compiler.forgetStructure;
+  val display_val = pretty_ml o PolyML.NameSpace.displayVal;
+end;
+
+use "ML-Systems/use_context.ML";
+use "ML-Systems/ml_positions.ML";
+use "ML-Systems/compiler_polyml.ML";
+
+PolyML.Compiler.reportUnreferencedIds := true;
+PolyML.Compiler.printInAlphabeticalOrder := false;
+PolyML.Compiler.maxInlineSize := 80;
+
+fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2);
+
+use "ML-Systems/ml_parse_tree.ML";
+if ML_System.name = "polyml-5.5.3"
+then use "ML-Systems/ml_parse_tree_polyml-5.5.3.ML" else ();
+
+use "ML-Systems/ml_compiler_parameters.ML";
+if ML_System.name = "polyml-5.5.3"
+then use "ML-Systems/ml_compiler_parameters_polyml-5.5.3.ML" else ();
+
 fun toplevel_pp context (_: string list) pp =
   use_text context (1, "pp") false
     ("PolyML.addPrettyPrinter (fn _ => fn _ => ml_pretty o Pretty.to_ML o (" ^ pp ^ "))");
@@ -202,3 +197,9 @@
 fun ml_make_string struct_name =
   "(fn x => Pretty.string_of (Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (x, " ^
     struct_name ^ ".ML_print_depth ())))))";
+
+
+(* ML debugger *)
+
+use "ML-Systems/ml_debugger.ML";
+if ML_System.name = "polyml-5.5.3" then use "ML-Systems/ml_debugger_polyml-5.5.3.ML" else ();

--- a/src/Pure/ML-Systems/smlnj.ML	Tue Aug 11 18:42:29 2015 +0200
+++ b/src/Pure/ML-Systems/smlnj.ML	Tue Aug 11 20:05:27 2015 +0200
@@ -19,8 +19,8 @@
 use "ML-Systems/thread_dummy.ML";
 use "ML-Systems/multithreading.ML";
 use "ML-Systems/maximum_ml_stack_dummy.ML";
+use "ML-Systems/ml_pretty.ML";
 use "ML-Systems/ml_name_space.ML";
-use "ML-Systems/ml_pretty.ML";
 structure PolyML = struct end;
 use "ML-Systems/pp_dummy.ML";
 use "ML-Systems/use_context.ML";

--- a/src/Pure/Tools/debugger.ML	Tue Aug 11 18:42:29 2015 +0200
+++ b/src/Pure/Tools/debugger.ML	Tue Aug 11 20:05:27 2015 +0200
@@ -134,25 +134,22 @@
       writeln = writeln_message, warning = warning_message}
     Position.none;
 
-in
-
-fun eval thread_name index SML txt1 txt2 =
+fun eval_context thread_name index SML toks =
   let
-    val (toks1, toks2) = apply2 (ML_Lex.read_source SML o Input.string) (txt1, txt2);
-
-    val evaluate_verbose = evaluate {SML = SML, verbose = true};
-    val context1 = ML_Context.the_generic_context ()
+    val context1 =
+      ML_Context.the_generic_context ()
       |> Context_Position.set_visible_generic false
       |> Config.put_generic ML_Options.debugger false
       |> ML_Env.add_name_space {SML = SML}
           (ML_Debugger.debug_name_space (the_debug_state thread_name index));
     val context2 =
-      if SML orelse forall (fn Antiquote.Text tok => ML_Lex.is_improper tok | _ => false) toks1
+      if SML orelse forall (fn Antiquote.Text tok => ML_Lex.is_improper tok | _ => false) toks
       then context1
       else
         let
           val context' = context1
-            |> ML_Context.exec (fn () => evaluate_verbose (ML_Lex.read "val ML_context = " @ toks1));
+            |> ML_Context.exec (fn () =>
+                evaluate {SML = SML, verbose = true} (ML_Lex.read "val ML_context = " @ toks));
           fun try_exec toks =
             try (ML_Context.exec (fn () => evaluate {SML = false, verbose = false} toks)) context';
         in
@@ -160,7 +157,28 @@
             SOME context2 => context2
           | NONE => error "Malformed context: expected type theory, Proof.context, Context.generic")
         end;
-  in Context.setmp_thread_data (SOME context2) evaluate_verbose toks2 end;
+  in context2 end;
+
+in
+
+fun eval thread_name index SML txt1 txt2 =
+  let
+    val (toks1, toks2) = apply2 (ML_Lex.read_source SML o Input.string) (txt1, txt2);
+    val context = eval_context thread_name index SML toks1;
+  in Context.setmp_thread_data (SOME context) evaluate {SML = SML, verbose = true} toks2 end;
+
+fun print_vals thread_name index SML txt =
+  let
+    val context = eval_context thread_name index SML (ML_Lex.read_source SML (Input.string txt));
+    val space = ML_Debugger.debug_name_space (the_debug_state thread_name index);
+
+    fun print x =
+      Pretty.from_ML (ML_Name_Space.display_val (x, ML_Options.get_print_depth (), space));
+    fun print_all () =
+      #allVal (ML_Debugger.debug_name_space (the_debug_state thread_name index)) ()
+      |> sort_wrt #1 |> map (Pretty.item o single o print o #2)
+      |> Pretty.chunks |> Pretty.string_of |> writeln_message;
+  in Context.setmp_thread_data (SOME context) print_all () end;
 
 end;
 
@@ -189,6 +207,9 @@
   | ["eval", index, SML, txt1, txt2] =>
      (error_wrapper (fn () =>
         eval thread_name (Markup.parse_int index) (Markup.parse_bool SML) txt1 txt2); true)
+  | ["print_vals", index, SML, txt] =>
+     (error_wrapper (fn () =>
+        print_vals thread_name (Markup.parse_int index) (Markup.parse_bool SML) txt); true)
   | bad =>
      (Output.system_message
         ("Debugger: bad input " ^ ML_Syntax.print_list ML_Syntax.print_string bad); true));

--- a/src/Pure/Tools/debugger.scala	Tue Aug 11 18:42:29 2015 +0200
+++ b/src/Pure/Tools/debugger.scala	Tue Aug 11 20:05:27 2015 +0200
@@ -195,4 +195,12 @@
       state.clear_output(thread_name)
     })
   }
+
+  def print_vals(thread_name: String, index: Int, SML: Boolean, context: String)
+  {
+    global_state.change(state => {
+      input(thread_name, "print_vals", index.toString, SML.toString, Symbol.encode(context))
+      state.clear_output(thread_name)
+    })
+  }
 }

--- a/src/Tools/jEdit/src/debugger_dockable.scala	Tue Aug 11 18:42:29 2015 +0200
+++ b/src/Tools/jEdit/src/debugger_dockable.scala	Tue Aug 11 20:05:27 2015 +0200
@@ -158,14 +158,20 @@
 
   def thread_selection(): Option[String] = tree_selection().map(sel => sel._1.thread_name)
 
-  def focus_selection(): Option[Position.T] =
+  def index_selection(): Option[(Debugger_Dockable.Thread_Entry, Int)] =
     tree_selection() match {
       case Some((t, opt_index)) =>
         val i = opt_index getOrElse 0
-        if (i < t.debug_states.length) Some(t.debug_states(i).pos) else None
+        if (i < t.debug_states.length) Some((t, i)) else None
       case _ => None
     }
 
+  def focus_selection(): Option[Position.T] =
+    index_selection() match {
+      case Some((t, i)) => Some(t.debug_states(i).pos)
+      case None => None
+    }
+
   private def update_tree(thread_entries: List[Debugger_Dockable.Thread_Entry])
   {
     val old_thread_selection =
@@ -212,7 +218,11 @@
       if (click != null && e.getClickCount == 1) {
         (click.getLastPathComponent, tree.getLastSelectedPathComponent) match {
           case (node: DefaultMutableTreeNode, node1: DefaultMutableTreeNode) if node == node1 =>
-            handle_update()
+            index_selection() match {
+              case Some((t, i)) =>
+                Debugger.print_vals(t.thread_name, i, sml_button.selected, context_field.getText)
+              case None =>
+            }
           case _ =>
         }
       }