src/Pure/PIDE/command.ML

   Toplevel.setmp_thread_position tr
     (fn () =>
       Outer_Syntax.side_comments span |> maps (fn cmt =>
         (Thy_Output.output_text st' {markdown = false} (Token.input_of cmt); [])
           handle exn =>
-            if Exn.is_interrupt exn then reraise exn
+            if Exn.is_interrupt exn then Exn.reraise exn
             else Runtime.exn_messages_ids exn)) ();
 
 fun report tr m =
   Toplevel.setmp_thread_position tr (fn () => Output.report [Markup.markup_only m]) ();
 

   Synchronized.var "Command.print_functions" ([]: (string * print_function) list);
 
 fun print_error tr opt_context e =
   (Toplevel.setmp_thread_position tr o Runtime.controlled_execution opt_context) e ()
     handle exn =>
-      if Exn.is_interrupt exn then reraise exn
+      if Exn.is_interrupt exn then Exn.reraise exn
       else List.app (Future.error_message (Toplevel.pos_of tr)) (Runtime.exn_messages_ids exn);
 
 fun print_finished (Print {print_process, ...}) = Lazy.is_finished print_process;
 
 fun print_persistent (Print {persistent, ...}) = persistent;

           exec_id = exec_id, print_process = Lazy.lazy process}
       end;
 
     fun bad_print name args exn =
       make_print name args {delay = NONE, pri = 0, persistent = false,
-        strict = false, print_fn = fn _ => fn _ => reraise exn};
+        strict = false, print_fn = fn _ => fn _ => Exn.reraise exn};
 
     fun new_print name args get_pr =
       let
         val params =
          {keywords = keywords,