# HG changeset patch
# User wenzelm
# Date 1376125196 -7200
# Node ID 2c927b7501c58ec445d26c856a485b0713c95c7f
# Parent  07423b37bc225ab60faf32c51e9eb786b0130a01
explicit "strict" flag for print functions (flipped internal meaning);
non-strict query operations may operate on failed states;

diff -r 07423b37bc22 -r 2c927b7501c5 src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Sat Aug 10 10:15:30 2013 +0200
+++ b/src/Pure/PIDE/command.ML	Sat Aug 10 10:59:56 2013 +0200
@@ -17,9 +17,10 @@
   val print: bool -> (string * string list) list -> string ->
     eval -> print list -> print list option
   type print_fn = Toplevel.transition -> Toplevel.state -> unit
-  val print_function: string ->
-    ({command_name: string, args: string list} ->
-      {delay: Time.time option, pri: int, persistent: bool, print_fn: print_fn} option) -> unit
+  type print_function =
+    {command_name: string, args: string list} ->
+      {delay: Time.time option, pri: int, persistent: bool, strict: bool, print_fn: print_fn} option
+  val print_function: string -> print_function -> unit
   val no_print_function: string -> unit
   type exec = eval * print list
   val no_exec: exec
@@ -203,7 +204,7 @@
 
 type print_function =
   {command_name: string, args: string list} ->
-    {delay: Time.time option, pri: int, persistent: bool, print_fn: print_fn} option;
+    {delay: Time.time option, pri: int, persistent: bool, strict: bool, print_fn: print_fn} option;
 
 local
 
@@ -232,7 +233,7 @@
 
     fun new_print name args get_pr =
       let
-        fun make_print strict {delay, pri, persistent, print_fn} =
+        fun make_print {delay, pri, persistent, strict, print_fn} =
           let
             val exec_id = Document_ID.make ();
             fun process () =
@@ -240,22 +241,22 @@
                 val {failed, command, state = st', ...} = eval_result eval;
                 val tr = Toplevel.exec_id exec_id command;
               in
-                if failed andalso not strict then ()
+                if failed andalso strict then ()
                 else print_error tr (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}
+            Print {
+              name = name, args = args, delay = delay, pri = pri, persistent = persistent,
+              exec_id = exec_id, print_process = memo exec_id process}
           end;
         val params = {command_name = command_name, args = args};
       in
         (case Exn.capture (Runtime.controlled_execution get_pr) params of
           Exn.Res NONE => NONE
-        | Exn.Res (SOME pr) => SOME (make_print false pr)
+        | Exn.Res (SOME pr) => SOME (make_print pr)
         | Exn.Exn exn =>
-            SOME (make_print true
-              {delay = NONE, pri = 0, persistent = false, print_fn = fn _ => fn _ => reraise exn}))
+            SOME (make_print {delay = NONE, pri = 0, persistent = false,
+              strict = false, print_fn = fn _ => fn _ => reraise exn}))
       end;
 
     fun get_print (a, b) =
@@ -290,7 +291,7 @@
 val _ =
   print_function "print_state"
     (fn {command_name, ...} =>
-      SOME {delay = NONE, pri = 1, persistent = true,
+      SOME {delay = NONE, pri = 1, persistent = true, strict = true,
         print_fn = fn tr => fn st' =>
           let
             val is_init = Keyword.is_theory_begin command_name;
diff -r 07423b37bc22 -r 2c927b7501c5 src/Pure/PIDE/query_operation.ML
--- a/src/Pure/PIDE/query_operation.ML	Sat Aug 10 10:15:30 2013 +0200
+++ b/src/Pure/PIDE/query_operation.ML	Sat Aug 10 10:59:56 2013 +0200
@@ -17,7 +17,7 @@
 fun register_parallel name f =
   Command.print_function name
     (fn {args = instance :: args, ...} =>
-        SOME {delay = NONE, pri = 0, persistent = false,
+        SOME {delay = NONE, pri = 0, persistent = false, strict = false,
           print_fn = fn _ => uninterruptible (fn restore_attributes => fn state =>
             let
               fun result s = Output.result [(Markup.instanceN, instance)] s;
diff -r 07423b37bc22 -r 2c927b7501c5 src/Tools/try.ML
--- a/src/Tools/try.ML	Sat Aug 10 10:15:30 2013 +0200
+++ b/src/Tools/try.ML	Sat Aug 10 10:59:56 2013 +0200
@@ -123,6 +123,7 @@
          {delay = SOME (seconds (Options.default_real @{option auto_time_start})),
           pri = ~ weight,
           persistent = true,
+          strict = true,
           print_fn = fn _ => fn st =>
             let
               val state = Toplevel.proof_of st