83 fun with_debugging e = |
83 fun with_debugging e = |
84 setmp_thread_data tag (get_debugging ()) (ML_Debugger.state (Thread.self ())) e (); |
84 setmp_thread_data tag (get_debugging ()) (ML_Debugger.state (Thread.self ())) e (); |
85 |
85 |
86 end; |
86 end; |
87 |
87 |
|
88 fun the_debug_state thread_name index = |
|
89 (case get_debugging () of |
|
90 [] => error ("Missing debugger information for thread " ^ quote thread_name) |
|
91 | states => |
|
92 if index < 0 orelse index >= length states then |
|
93 error ("Bad debugger stack index " ^ signed_string_of_int index ^ " for thread " ^ |
|
94 quote thread_name) |
|
95 else nth states index); |
|
96 |
|
97 |
88 |
98 |
89 (* eval ML *) |
99 (* eval ML *) |
90 |
100 |
91 fun eval thread_name index SML context expression = (* FIXME *) |
101 fun eval thread_name index SML txt1 txt2 = |
92 writeln_message ("SML = " ^ Markup.print_bool SML ^ |
102 let |
93 "\ncontext = " ^ context ^ "\nexpression = " ^ expression); |
103 fun evaluate verbose = |
|
104 ML_Context.eval |
|
105 {SML = SML, exchange = false, redirect = false, verbose = verbose, |
|
106 writeln = writeln_message, warning = warning_message} |
|
107 Position.none; |
|
108 |
|
109 val debug_state = the_debug_state thread_name index; |
|
110 val context1 = ML_Context.the_generic_context () |
|
111 |> Context_Position.set_visible_generic false |
|
112 |> ML_Env.add_name_space {SML = SML} (ML_Debugger.debug_name_space debug_state); |
|
113 val (toks1, toks2) = apply2 (ML_Lex.read_source SML o Input.string) (txt1, txt2); |
|
114 in |
|
115 if null (filter_out (fn Antiquote.Text tok => ML_Lex.is_improper tok | _ => false) toks1) |
|
116 then Context.setmp_thread_data (SOME context1) (fn () => evaluate true toks2) () |
|
117 else error "FIXME" |
|
118 end; |
94 |
119 |
95 |
120 |
96 (* debugger entry point *) |
121 (* debugger entry point *) |
97 |
122 |
98 local |
123 local |