src/Pure/PIDE/command.ML

 local
 
 val print_functions =
   Synchronized.var "Command.print_functions" ([]: (string * print_function) list);
 
-fun print_error tr e =
-  (Toplevel.setmp_thread_position tr o Toplevel.controlled_execution) e ()
+fun print_error tr opt_context e =
+  (Toplevel.setmp_thread_position tr o Toplevel.controlled_execution opt_context) e ()
     handle exn =>
       if Exn.is_interrupt exn then reraise exn
       else List.app (Future.error_msg (Toplevel.pos_of tr)) (ML_Compiler.exn_messages_ids exn);
 
 fun print_eq (Print {exec_id, ...}, Print {exec_id = exec_id', ...}) = exec_id = exec_id';

         val exec_id = Document_ID.make ();
         fun process () =
           let
             val {failed, command, state = st', ...} = eval_result eval;
             val tr = Toplevel.exec_id exec_id command;
+            val opt_context = try Toplevel.generic_theory_of st';
           in
             if failed andalso strict then ()
-            else print_error tr (fn () => print_fn tr st')
+            else print_error tr opt_context (fn () => print_fn tr st')
           end;
       in
         Print {
           name = name, args = args, delay = delay, pri = pri, persistent = persistent,
           exec_id = exec_id, print_process = memo exec_id process}

 
     fun new_print name args get_pr =
       let
         val params = {command_name = command_name, args = args};
       in
-        (case Exn.capture (Toplevel.controlled_execution get_pr) params of
+        (case Exn.capture (Toplevel.controlled_execution NONE get_pr) params of
           Exn.Res NONE => NONE
         | Exn.Res (SOME pr) => SOME (make_print name args pr)
         | Exn.Exn exn => SOME (bad_print name args exn))
       end;