src/Pure/PIDE/command.ML
changeset 52516 b5b3c888df9f
parent 52515 0dcadc90550b
child 52526 d234cb6b60e3
equal deleted inserted replaced
52515:0dcadc90550b 52516:b5b3c888df9f
   163 local
   163 local
   164 
   164 
   165 val print_functions =
   165 val print_functions =
   166   Synchronized.var "Command.print_functions" ([]: (string * (int * print_function)) list);
   166   Synchronized.var "Command.print_functions" ([]: (string * (int * print_function)) list);
   167 
   167 
       
   168 fun output_error tr exn =
       
   169   List.app (Future.error_msg (Toplevel.pos_of tr)) (ML_Compiler.exn_messages_ids exn);
       
   170 
       
   171 fun print_error tr f x =
       
   172   (Toplevel.setmp_thread_position tr o Runtime.controlled_execution) f x
       
   173     handle exn => output_error tr exn;
       
   174 
   168 in
   175 in
   169 
   176 
   170 fun print st tr st' =
   177 fun print st tr st' =
   171   rev (Synchronized.value print_functions) |> map_filter (fn (name, (pri, f)) =>
   178   rev (Synchronized.value print_functions) |> map_filter (fn (name, (pri, f)) =>
   172     (case f {old_state = st, tr = tr, state = st'} of
   179     (case Exn.capture (Runtime.controlled_execution f) {old_state = st, tr = tr, state = st'} of
   173       SOME pr =>
   180       Exn.Res NONE => NONE
   174         SOME {name = name, pri = pri, pr = (Lazy.lazy o Toplevel.setmp_thread_position tr) pr}
   181     | Exn.Res (SOME pr) => SOME {name = name, pri = pri, pr = (Lazy.lazy o print_error tr) pr}
   175     | NONE => NONE));
   182     | Exn.Exn exn => SOME {name = name, pri = pri, pr = Lazy.lazy (fn () => output_error tr exn)}));
   176 
   183 
   177 fun print_function name pri f =
   184 fun print_function name pri f =
   178   Synchronized.change print_functions (fn funs =>
   185   Synchronized.change print_functions (fn funs =>
   179    (if not (AList.defined (op =) funs name) then ()
   186    (if not (AList.defined (op =) funs name) then ()
   180     else warning ("Redefining command print function: " ^ quote name);
   187     else warning ("Redefining command print function: " ^ quote name);