equal
deleted
inserted
replaced
210 |
210 |
211 val print_functions = |
211 val print_functions = |
212 Synchronized.var "Command.print_functions" ([]: (string * print_function) list); |
212 Synchronized.var "Command.print_functions" ([]: (string * print_function) list); |
213 |
213 |
214 fun print_error tr e = |
214 fun print_error tr e = |
215 (Toplevel.setmp_thread_position tr o Runtime.controlled_execution) e () |
215 (Toplevel.setmp_thread_position tr o Toplevel.controlled_execution) e () |
216 handle exn => |
216 handle exn => |
217 if Exn.is_interrupt exn then reraise exn |
217 if Exn.is_interrupt exn then reraise exn |
218 else List.app (Future.error_msg (Toplevel.pos_of tr)) (ML_Compiler.exn_messages_ids exn); |
218 else List.app (Future.error_msg (Toplevel.pos_of tr)) (ML_Compiler.exn_messages_ids exn); |
219 |
219 |
220 fun print_eq (Print {exec_id, ...}, Print {exec_id = exec_id', ...}) = exec_id = exec_id'; |
220 fun print_eq (Print {exec_id, ...}, Print {exec_id = exec_id', ...}) = exec_id = exec_id'; |
254 |
254 |
255 fun new_print name args get_pr = |
255 fun new_print name args get_pr = |
256 let |
256 let |
257 val params = {command_name = command_name, args = args}; |
257 val params = {command_name = command_name, args = args}; |
258 in |
258 in |
259 (case Exn.capture (Runtime.controlled_execution get_pr) params of |
259 (case Exn.capture (Toplevel.controlled_execution get_pr) params of |
260 Exn.Res NONE => NONE |
260 Exn.Res NONE => NONE |
261 | Exn.Res (SOME pr) => SOME (make_print name args pr) |
261 | Exn.Res (SOME pr) => SOME (make_print name args pr) |
262 | Exn.Exn exn => SOME (bad_print name args exn)) |
262 | Exn.Exn exn => SOME (bad_print name args exn)) |
263 end; |
263 end; |
264 |
264 |