1.1 --- a/src/Pure/PIDE/command.ML	Tue Aug 13 11:13:26 2013 +0200
     1.2 +++ b/src/Pure/PIDE/command.ML	Tue Aug 13 11:49:01 2013 +0200
     1.3 @@ -231,39 +231,42 @@
     1.4    let
     1.5      val print_functions = Synchronized.value print_functions;
     1.6  
     1.7 +    fun make_print name args {delay, pri, persistent, strict, print_fn} =
     1.8 +      let
     1.9 +        val exec_id = Document_ID.make ();
    1.10 +        fun process () =
    1.11 +          let
    1.12 +            val {failed, command, state = st', ...} = eval_result eval;
    1.13 +            val tr = Toplevel.exec_id exec_id command;
    1.14 +          in
    1.15 +            if failed andalso strict then ()
    1.16 +            else print_error tr (fn () => print_fn tr st')
    1.17 +          end;
    1.18 +      in
    1.19 +        Print {
    1.20 +          name = name, args = args, delay = delay, pri = pri, persistent = persistent,
    1.21 +          exec_id = exec_id, print_process = memo exec_id process}
    1.22 +      end;
    1.23 +
    1.24 +    fun bad_print name args exn =
    1.25 +      make_print name args {delay = NONE, pri = 0, persistent = false,
    1.26 +        strict = false, print_fn = fn _ => fn _ => reraise exn};
    1.27 +
    1.28      fun new_print name args get_pr =
    1.29        let
    1.30 -        fun make_print {delay, pri, persistent, strict, print_fn} =
    1.31 -          let
    1.32 -            val exec_id = Document_ID.make ();
    1.33 -            fun process () =
    1.34 -              let
    1.35 -                val {failed, command, state = st', ...} = eval_result eval;
    1.36 -                val tr = Toplevel.exec_id exec_id command;
    1.37 -              in
    1.38 -                if failed andalso strict then ()
    1.39 -                else print_error tr (fn () => print_fn tr st')
    1.40 -              end;
    1.41 -          in
    1.42 -            Print {
    1.43 -              name = name, args = args, delay = delay, pri = pri, persistent = persistent,
    1.44 -              exec_id = exec_id, print_process = memo exec_id process}
    1.45 -          end;
    1.46          val params = {command_name = command_name, args = args};
    1.47        in
    1.48          (case Exn.capture (Runtime.controlled_execution get_pr) params of
    1.49            Exn.Res NONE => NONE
    1.50 -        | Exn.Res (SOME pr) => SOME (make_print pr)
    1.51 -        | Exn.Exn exn =>
    1.52 -            SOME (make_print {delay = NONE, pri = 0, persistent = false,
    1.53 -              strict = false, print_fn = fn _ => fn _ => reraise exn}))
    1.54 +        | Exn.Res (SOME pr) => SOME (make_print name args pr)
    1.55 +        | Exn.Exn exn => SOME (bad_print name args exn))
    1.56        end;
    1.57  
    1.58      fun get_print (a, b) =
    1.59        (case find_first (fn Print {name, args, ...} => name = a andalso args = b) old_prints of
    1.60          NONE =>
    1.61            (case AList.lookup (op =) print_functions a of
    1.62 -            NONE => NONE
    1.63 +            NONE => SOME (bad_print a b (ERROR ("Missing print function " ^ quote a)))
    1.64            | SOME get_pr => new_print a b get_pr)
    1.65        | some => some);
    1.66