# HG changeset patch
# User wenzelm
# Date 1438889514 -7200
# Node ID 7bf2188a0998fa8b9e7301764eca77b272052a3f
# Parent  4c18d8e4fe149ece4f25b4973445b5ccb2e48c4e
evaluate ML expressions within debugger context;
redirected writeln/warning for ML compiler;

diff -r 4c18d8e4fe14 -r 7bf2188a0998 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Thu Aug 06 20:33:12 2015 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Thu Aug 06 21:31:54 2015 +0200
@@ -209,7 +209,9 @@
         let
           val ([{lines, pos, ...}], thy') = files thy;
           val source = Input.source true (cat_lines lines) (pos, pos);
-          val flags = {SML = true, exchange = false, redirect = true, verbose = true};
+          val flags =
+            {SML = true, exchange = false, redirect = true, verbose = true,
+              writeln = writeln, warning = warning};
         in
           thy' |> Context.theory_map
             (ML_Context.exec (fn () => ML_Context.eval_source flags source))
@@ -218,7 +220,11 @@
 val _ =
   Outer_Syntax.command @{command_keyword SML_export} "evaluate SML within Isabelle/ML environment"
     (Parse.ML_source >> (fn source =>
-      let val flags = {SML = true, exchange = true, redirect = false, verbose = true} in
+      let
+        val flags =
+          {SML = true, exchange = true, redirect = false, verbose = true,
+            writeln = writeln, warning = warning};
+      in
         Toplevel.theory
           (Context.theory_map (ML_Context.exec (fn () => ML_Context.eval_source flags source)))
       end));
@@ -226,7 +232,11 @@
 val _ =
   Outer_Syntax.command @{command_keyword SML_import} "evaluate Isabelle/ML within SML environment"
     (Parse.ML_source >> (fn source =>
-      let val flags = {SML = false, exchange = true, redirect = false, verbose = true} in
+      let
+        val flags =
+          {SML = false, exchange = true, redirect = false, verbose = true,
+            writeln = writeln, warning = warning};
+      in
         Toplevel.generic_theory
           (ML_Context.exec (fn () => ML_Context.eval_source flags source) #>
             Local_Theory.propagate_ml_env)
diff -r 4c18d8e4fe14 -r 7bf2188a0998 src/Pure/ML/ml_compiler.ML
--- a/src/Pure/ML/ml_compiler.ML	Thu Aug 06 20:33:12 2015 +0200
+++ b/src/Pure/ML/ml_compiler.ML	Thu Aug 06 21:31:54 2015 +0200
@@ -6,7 +6,9 @@
 
 signature ML_COMPILER =
 sig
-  type flags = {SML: bool, exchange: bool, redirect: bool, verbose: bool}
+  type flags =
+    {SML: bool, exchange: bool, redirect: bool, verbose: bool,
+      writeln: string -> unit, warning: string -> unit}
   val flags: flags
   val verbose: bool -> flags -> flags
   val eval: flags -> Position.T -> ML_Lex.token list -> unit
@@ -15,11 +17,17 @@
 structure ML_Compiler: ML_COMPILER =
 struct
 
-type flags = {SML: bool, exchange: bool, redirect: bool, verbose: bool};
-val flags = {SML = false, exchange = false, redirect = false, verbose = false};
+type flags =
+  {SML: bool, exchange: bool, redirect: bool, verbose: bool,
+    writeln: string -> unit, warning: string -> unit};
+
+val flags: flags =
+  {SML = false, exchange = false, redirect = false, verbose = false,
+    writeln = writeln, warning = warning};
 
 fun verbose b (flags: flags) =
-  {SML = #SML flags, exchange = #exchange flags, redirect = #redirect flags, verbose = b};
+  {SML = #SML flags, exchange = #exchange flags, redirect = #redirect flags, verbose = b,
+    writeln = #writeln flags, warning = #warning flags};
 
 fun eval (flags: flags) pos toks =
   let
diff -r 4c18d8e4fe14 -r 7bf2188a0998 src/Pure/ML/ml_compiler_polyml.ML
--- a/src/Pure/ML/ml_compiler_polyml.ML	Thu Aug 06 20:33:12 2015 +0200
+++ b/src/Pure/ML/ml_compiler_polyml.ML	Thu Aug 06 21:31:54 2015 +0200
@@ -145,15 +145,15 @@
 
     val writeln_buffer = Unsynchronized.ref Buffer.empty;
     fun write s = Unsynchronized.change writeln_buffer (Buffer.add s);
-    fun output_writeln () = writeln (trim_line (Buffer.content (! writeln_buffer)));
+    fun output_writeln () = #writeln flags (trim_line (Buffer.content (! writeln_buffer)));
 
     val warnings = Unsynchronized.ref ([]: string list);
     fun warn msg = Unsynchronized.change warnings (cons msg);
-    fun output_warnings () = List.app warning (rev (! warnings));
+    fun output_warnings () = List.app (#warning flags) (rev (! warnings));
 
     val error_buffer = Unsynchronized.ref Buffer.empty;
     fun err msg = Unsynchronized.change error_buffer (Buffer.add msg #> Buffer.add "\n");
-    fun flush_error () = writeln (Buffer.content (! error_buffer));
+    fun flush_error () = #writeln flags (Buffer.content (! error_buffer));
     fun raise_error msg = error (Buffer.content (Buffer.add msg (! error_buffer)));
 
     fun message {message = msg, hard, location = loc, context = _} =
diff -r 4c18d8e4fe14 -r 7bf2188a0998 src/Pure/ML/ml_env.ML
--- a/src/Pure/ML/ml_env.ML	Thu Aug 06 20:33:12 2015 +0200
+++ b/src/Pure/ML/ml_env.ML	Thu Aug 06 21:31:54 2015 +0200
@@ -12,6 +12,7 @@
   val add_breakpoint: serial * (bool Unsynchronized.ref * Position.T) ->
     Context.generic -> Context.generic
   val get_breakpoint: Context.generic -> serial -> (bool Unsynchronized.ref * Position.T) option
+  val add_name_space: {SML: bool} -> ML_Name_Space.T -> Context.generic -> Context.generic
   val name_space: {SML: bool, exchange: bool} -> ML_Name_Space.T
   val local_context: use_context
   val local_name_space: ML_Name_Space.T
@@ -91,6 +92,22 @@
 
 (* name space *)
 
+fun add_name_space {SML} (space: ML_Name_Space.T) =
+  Env.map (fn {bootstrap, tables, sml_tables, breakpoints} =>
+    let
+      val (tables', sml_tables') =
+        (tables, sml_tables) |> (if SML then apsnd else apfst)
+          (fn (val1, type1, fixity1, structure1, signature1, functor1) =>
+            let
+              val val2 = fold Symtab.update (#allVal space ()) val1;
+              val type2 = fold Symtab.update (#allType space ()) type1;
+              val fixity2 = fold Symtab.update (#allFix space ()) fixity1;
+              val structure2 = fold Symtab.update (#allStruct space ()) structure1;
+              val signature2 = fold Symtab.update (#allSig space ()) signature1;
+              val functor2 = fold Symtab.update (#allFunct space ()) functor1;
+            in (val2, type2, fixity2, structure2, signature2, functor2) end);
+    in make_data (bootstrap, tables', sml_tables', breakpoints) end);
+
 fun name_space {SML, exchange} : ML_Name_Space.T =
   let
     fun lookup sel1 sel2 name =
diff -r 4c18d8e4fe14 -r 7bf2188a0998 src/Pure/ML/ml_file.ML
--- a/src/Pure/ML/ml_file.ML	Thu Aug 06 20:33:12 2015 +0200
+++ b/src/Pure/ML/ml_file.ML	Thu Aug 06 21:31:54 2015 +0200
@@ -14,7 +14,9 @@
           val [{src_path, lines, digest, pos}] = files (Context.theory_of gthy);
           val provide = Resources.provide (src_path, digest);
           val source = Input.source true (cat_lines lines) (pos, pos);
-          val flags = {SML = false, exchange = false, redirect = true, verbose = true};
+          val flags =
+            {SML = false, exchange = false, redirect = true, verbose = true,
+              writeln = writeln, warning = warning};
         in
           gthy
           |> ML_Context.exec (fn () => ML_Context.eval_source flags source)
diff -r 4c18d8e4fe14 -r 7bf2188a0998 src/Pure/Tools/debugger.ML
--- a/src/Pure/Tools/debugger.ML	Thu Aug 06 20:33:12 2015 +0200
+++ b/src/Pure/Tools/debugger.ML	Thu Aug 06 21:31:54 2015 +0200
@@ -85,12 +85,37 @@
 
 end;
 
+fun the_debug_state thread_name index =
+  (case get_debugging () of
+    [] => error ("Missing debugger information for thread " ^ quote thread_name)
+  | states =>
+      if index < 0 orelse index >= length states then
+        error ("Bad debugger stack index " ^ signed_string_of_int index ^ " for thread " ^
+          quote thread_name)
+      else nth states index);
+
+
 
 (* eval ML *)
 
-fun eval thread_name index SML context expression =  (* FIXME *)
-  writeln_message ("SML = " ^ Markup.print_bool SML ^
-    "\ncontext = " ^ context ^ "\nexpression = " ^ expression);
+fun eval thread_name index SML txt1 txt2 =
+  let
+    fun evaluate verbose =
+      ML_Context.eval
+        {SML = SML, exchange = false, redirect = false, verbose = verbose,
+          writeln = writeln_message, warning = warning_message}
+        Position.none;
+
+    val debug_state = the_debug_state thread_name index;
+    val context1 = ML_Context.the_generic_context ()
+      |> Context_Position.set_visible_generic false
+      |> ML_Env.add_name_space {SML = SML} (ML_Debugger.debug_name_space debug_state);
+    val (toks1, toks2) = apply2 (ML_Lex.read_source SML o Input.string) (txt1, txt2);
+  in
+    if null (filter_out (fn Antiquote.Text tok => ML_Lex.is_improper tok | _ => false) toks1)
+    then Context.setmp_thread_data (SOME context1) (fn () => evaluate true toks2) ()
+    else error "FIXME"
+  end;
 
 
 (* debugger entry point *)
diff -r 4c18d8e4fe14 -r 7bf2188a0998 src/Pure/context_position.ML
--- a/src/Pure/context_position.ML	Thu Aug 06 20:33:12 2015 +0200
+++ b/src/Pure/context_position.ML	Thu Aug 06 21:31:54 2015 +0200
@@ -9,6 +9,7 @@
   val is_visible_generic: Context.generic -> bool
   val is_visible: Proof.context -> bool
   val is_visible_global: theory -> bool
+  val set_visible_generic: bool -> Context.generic -> Context.generic
   val set_visible: bool -> Proof.context -> Proof.context
   val set_visible_global: bool -> theory -> theory
   val is_really_visible: Proof.context -> bool
@@ -40,6 +41,7 @@
 val is_visible = is_visible_generic o Context.Proof;
 val is_visible_global = is_visible_generic o Context.Theory;
 
+val set_visible_generic = Data.map o apsnd o K o SOME;
 val set_visible = Context.proof_map o Data.map o apsnd o K o SOME;
 val set_visible_global = Context.theory_map o Data.map o apsnd o K o SOME;