src/Pure/PIDE/command.ML
changeset 53709 84522727f9d3
parent 53404 d598b6231ff7
child 53976 da610b507799
equal deleted inserted replaced
53708:92aa282841f8 53709:84522727f9d3
   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