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