1.1 --- a/src/Pure/PIDE/command.ML Sat Aug 10 10:15:30 2013 +0200
1.2 +++ b/src/Pure/PIDE/command.ML Sat Aug 10 10:59:56 2013 +0200
1.3 @@ -17,9 +17,10 @@
1.4 val print: bool -> (string * string list) list -> string ->
1.5 eval -> print list -> print list option
1.6 type print_fn = Toplevel.transition -> Toplevel.state -> unit
1.7 - val print_function: string ->
1.8 - ({command_name: string, args: string list} ->
1.9 - {delay: Time.time option, pri: int, persistent: bool, print_fn: print_fn} option) -> unit
1.10 + type print_function =
1.11 + {command_name: string, args: string list} ->
1.12 + {delay: Time.time option, pri: int, persistent: bool, strict: bool, print_fn: print_fn} option
1.13 + val print_function: string -> print_function -> unit
1.14 val no_print_function: string -> unit
1.15 type exec = eval * print list
1.16 val no_exec: exec
1.17 @@ -203,7 +204,7 @@
1.18
1.19 type print_function =
1.20 {command_name: string, args: string list} ->
1.21 - {delay: Time.time option, pri: int, persistent: bool, print_fn: print_fn} option;
1.22 + {delay: Time.time option, pri: int, persistent: bool, strict: bool, print_fn: print_fn} option;
1.23
1.24 local
1.25
1.26 @@ -232,7 +233,7 @@
1.27
1.28 fun new_print name args get_pr =
1.29 let
1.30 - fun make_print strict {delay, pri, persistent, print_fn} =
1.31 + fun make_print {delay, pri, persistent, strict, print_fn} =
1.32 let
1.33 val exec_id = Document_ID.make ();
1.34 fun process () =
1.35 @@ -240,22 +241,22 @@
1.36 val {failed, command, state = st', ...} = eval_result eval;
1.37 val tr = Toplevel.exec_id exec_id command;
1.38 in
1.39 - if failed andalso not strict then ()
1.40 + if failed andalso strict then ()
1.41 else print_error tr (fn () => print_fn tr st')
1.42 end;
1.43 in
1.44 - Print {
1.45 - name = name, args = args, delay = delay, pri = pri, persistent = persistent,
1.46 - exec_id = exec_id, print_process = memo exec_id process}
1.47 + Print {
1.48 + name = name, args = args, delay = delay, pri = pri, persistent = persistent,
1.49 + exec_id = exec_id, print_process = memo exec_id process}
1.50 end;
1.51 val params = {command_name = command_name, args = args};
1.52 in
1.53 (case Exn.capture (Runtime.controlled_execution get_pr) params of
1.54 Exn.Res NONE => NONE
1.55 - | Exn.Res (SOME pr) => SOME (make_print false pr)
1.56 + | Exn.Res (SOME pr) => SOME (make_print pr)
1.57 | Exn.Exn exn =>
1.58 - SOME (make_print true
1.59 - {delay = NONE, pri = 0, persistent = false, print_fn = fn _ => fn _ => reraise exn}))
1.60 + SOME (make_print {delay = NONE, pri = 0, persistent = false,
1.61 + strict = false, print_fn = fn _ => fn _ => reraise exn}))
1.62 end;
1.63
1.64 fun get_print (a, b) =
1.65 @@ -290,7 +291,7 @@
1.66 val _ =
1.67 print_function "print_state"
1.68 (fn {command_name, ...} =>
1.69 - SOME {delay = NONE, pri = 1, persistent = true,
1.70 + SOME {delay = NONE, pri = 1, persistent = true, strict = true,
1.71 print_fn = fn tr => fn st' =>
1.72 let
1.73 val is_init = Keyword.is_theory_begin command_name;