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;

     2.1 --- a/src/Pure/PIDE/query_operation.ML	Sat Aug 10 10:15:30 2013 +0200
     2.2 +++ b/src/Pure/PIDE/query_operation.ML	Sat Aug 10 10:59:56 2013 +0200
     2.3 @@ -17,7 +17,7 @@
     2.4  fun register_parallel name f =
     2.5    Command.print_function name
     2.6      (fn {args = instance :: args, ...} =>
     2.7 -        SOME {delay = NONE, pri = 0, persistent = false,
     2.8 +        SOME {delay = NONE, pri = 0, persistent = false, strict = false,
     2.9            print_fn = fn _ => uninterruptible (fn restore_attributes => fn state =>
    2.10              let
    2.11                fun result s = Output.result [(Markup.instanceN, instance)] s;

     3.1 --- a/src/Tools/try.ML	Sat Aug 10 10:15:30 2013 +0200
     3.2 +++ b/src/Tools/try.ML	Sat Aug 10 10:59:56 2013 +0200
     3.3 @@ -123,6 +123,7 @@
     3.4           {delay = SOME (seconds (Options.default_real @{option auto_time_start})),
     3.5            pri = ~ weight,
     3.6            persistent = true,
     3.7 +          strict = true,
     3.8            print_fn = fn _ => fn st =>
     3.9              let
    3.10                val state = Toplevel.proof_of st