more print function parameters;
check command_visible statically in assignment, instead of dynamically in execution;

--- a/src/Pure/PIDE/command.ML	Wed Jul 03 21:55:15 2013 +0200
+++ b/src/Pure/PIDE/command.ML	Wed Jul 03 22:30:33 2013 +0200
@@ -17,9 +17,12 @@
   val read: span -> Toplevel.transition
   val eval: span -> Toplevel.transition ->
     Toplevel.state * {malformed: bool} -> {failed: bool} * (Toplevel.state * {malformed: bool})
-  val print: Toplevel.transition -> Toplevel.state -> (string * unit lazy) list
-  val print_function: string ->
-    ({tr: Toplevel.transition, state: Toplevel.state} -> (unit -> unit) option) -> unit
+  type print = {name: string, pri: int, pr: unit lazy}
+  val print: Toplevel.state -> Toplevel.transition -> Toplevel.state -> print list
+  type print_function =
+    {old_state: Toplevel.state, tr: Toplevel.transition, state: Toplevel.state} ->
+      (unit -> unit) option
+  val print_function: string -> int -> print_function -> unit
 end;
 
 structure Command: COMMAND =
@@ -151,31 +154,35 @@
 
 (* print *)
 
+type print_function =
+  {old_state: Toplevel.state, tr: Toplevel.transition, state: Toplevel.state} ->
+    (unit -> unit) option;
+
+type print = {name: string, pri: int, pr: unit lazy};
+
 local
 
-type print_function =
-  {tr: Toplevel.transition, state: Toplevel.state} -> (unit -> unit) option;
-
 val print_functions =
-  Synchronized.var "Command.print_functions" ([]: (string * print_function) list);
+  Synchronized.var "Command.print_functions" ([]: (string * (int * print_function)) list);
 
 in
 
-fun print tr st' =
-  rev (Synchronized.value print_functions) |> map_filter (fn (name, f) =>
-    (case f {tr = tr, state = st'} of
-      SOME pr => SOME (name, (Lazy.lazy o Toplevel.setmp_thread_position tr) pr)
+fun print st tr st' =
+  rev (Synchronized.value print_functions) |> map_filter (fn (name, (pri, f)) =>
+    (case f {old_state = st, tr = tr, state = st'} of
+      SOME pr =>
+        SOME {name = name, pri = pri, pr = (Lazy.lazy o Toplevel.setmp_thread_position tr) pr}
     | NONE => NONE));
 
-fun print_function name f =
+fun print_function name pri f =
   Synchronized.change print_functions (fn funs =>
    (if not (AList.defined (op =) funs name) then ()
     else warning ("Redefining command print function: " ^ quote name);
-    AList.update (op =) (name, f) funs));
+    AList.update (op =) (name, (pri, f)) funs));
 
 end;
 
-val _ = print_function "print_state" (fn {tr, state} =>
+val _ = print_function "print_state" 0 (fn {tr, state, ...} =>
   let
     val is_init = Toplevel.is_init tr;
     val is_proof = Keyword.is_proof (Toplevel.name_of tr);

--- a/src/Pure/PIDE/document.ML	Wed Jul 03 21:55:15 2013 +0200
+++ b/src/Pure/PIDE/document.ML	Wed Jul 03 22:30:33 2013 +0200
@@ -63,8 +63,8 @@
 type perspective = (command_id -> bool) * command_id option;
 structure Entries = Linear_Set(type key = command_id val ord = int_ord);
 
-type print = string * unit lazy;
-type exec = ((Toplevel.state * {malformed: bool}) * print list) Command.memo; (*eval/print process*)
+type exec = ((Toplevel.state * {malformed: bool}) * Command.print list) Command.memo;
+  (*eval/print process*)
 val no_exec = Command.memo_value ((Toplevel.toplevel, {malformed = false}), []);
 
 abstype node = Node of
@@ -324,16 +324,12 @@
 
 fun start_execution state =
   let
-    fun run node command_id exec =
-      let
-        val (_, print) = Command.memo_eval exec;
-        val _ =
-          if visible_command node command_id then
-            print |> List.app (fn (a, pr) =>
-              ignore
-                (Lazy.future {name = a, group = NONE, deps = [], pri = 0, interrupts = true} pr))
-          else ();
-      in () end;
+    fun execute exec =
+      Command.memo_eval exec
+      |> (fn (_, print) =>
+        print |> List.app (fn {name, pri, pr} =>
+          Lazy.future {name = name, group = NONE, deps = [], pri = pri, interrupts = true} pr
+          |> ignore));
 
     val (version_id, group, running) = execution_of state;
 
@@ -351,9 +347,9 @@
                   {name = "theory:" ^ name, group = SOME (Future.new_group (SOME group)),
                     deps = map (Future.task_of o #2) deps, pri = ~2, interrupts = false}
                   (fn () =>
-                    iterate_entries (fn ((_, id), opt_exec) => fn () =>
+                    iterate_entries (fn (_, opt_exec) => fn () =>
                       (case opt_exec of
-                        SOME (_, exec) => if ! running then SOME (run node id exec) else NONE
+                        SOME (_, exec) => if ! running then SOME (execute exec) else NONE
                       | NONE => NONE)) node ()))));
   in () end;
 
@@ -437,7 +433,7 @@
     else (common, flags)
   end;
 
-fun new_exec state proper_init command_id' (execs, command_exec, init) =
+fun new_exec state proper_init command_visible command_id' (execs, command_exec, init) =
   if not proper_init andalso is_none init then NONE
   else
     let
@@ -458,10 +454,10 @@
       val exec' =
         Command.memo (fn () =>
           let
-            val (st_malformed, _) = Command.memo_result (snd (snd command_exec));
+            val ((st, malformed), _) = Command.memo_result (snd (snd command_exec));
             val tr = read ();
-            val ({failed}, (st', malformed')) = Command.eval span tr st_malformed;
-            val print = if failed then [] else Command.print tr st';
+            val ({failed}, (st', malformed')) = Command.eval span tr (st, malformed);
+            val print = if failed orelse not command_visible then [] else Command.print st tr st';
           in ((st', malformed'), print) end);
       val command_exec' = (command_id', (exec_id', exec'));
     in SOME (command_exec' :: execs, command_exec', init') end;
@@ -511,7 +507,7 @@
                         iterate_entries_after common
                           (fn ((prev, id), _) => fn res =>
                             if not node_required andalso prev = last_visible then NONE
-                            else new_exec state proper_init id res) node;
+                            else new_exec state proper_init (visible_command node id) id res) node;
 
                     val no_execs =
                       iterate_entries_after common