# HG changeset patch
# User wenzelm
# Date 1375452014 -7200
# Node ID 9fff9f78240ad8838739f9de7ed2dd20e54f205a
# Parent  199e9fa5a5c2212c090853c47ec3f907e61740cc
support print functions with explicit arguments, as provided by overlays;

diff -r 199e9fa5a5c2 -r 9fff9f78240a src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Fri Aug 02 14:26:09 2013 +0200
+++ b/src/Pure/PIDE/command.ML	Fri Aug 02 16:00:14 2013 +0200
@@ -14,10 +14,11 @@
   val eval_result_state: eval -> Toplevel.state
   val eval: (unit -> theory) -> Token.T list -> eval -> eval
   type print
-  val print: bool -> string -> eval -> print list -> print list option
+  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} ->
+    ({command_name: string, args: string list} ->
       {delay: Time.time option, pri: int, persistent: bool, print_fn: print_fn} option) -> unit
   val no_print_function: string -> unit
   type exec = eval * print list
@@ -195,13 +196,13 @@
 (* print *)
 
 datatype print = Print of
- {name: string, delay: Time.time option, pri: int, persistent: bool,
+ {name: string, args: string list, delay: Time.time option, pri: int, persistent: bool,
   exec_id: Document_ID.exec, print_process: unit memo};
 
 type print_fn = Toplevel.transition -> Toplevel.state -> unit;
 
 type print_function =
-  {command_name: string} ->
+  {command_name: string, args: string list} ->
     {delay: Time.time option, pri: int, persistent: bool, print_fn: print_fn} option;
 
 local
@@ -223,9 +224,11 @@
 
 in
 
-fun print command_visible command_name eval old_prints =
+fun print command_visible command_overlays command_name eval old_prints =
   let
-    fun new_print (name, get_pr) =
+    val print_functions = Synchronized.value print_functions;
+
+    fun new_print name args get_pr =
       let
         fun make_print strict {delay, pri, persistent, print_fn} =
           let
@@ -240,11 +243,12 @@
               end;
           in
            Print {
-             name = name, delay = delay, pri = pri, persistent = persistent,
+             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) {command_name = command_name} of
+        (case Exn.capture (Runtime.controlled_execution get_pr) params of
           Exn.Res NONE => NONE
         | Exn.Res (SOME pr) => SOME (make_print false pr)
         | Exn.Exn exn =>
@@ -252,12 +256,18 @@
               {delay = NONE, pri = 0, persistent = false, print_fn = fn _ => fn _ => reraise exn}))
       end;
 
+    fun get_print (a, b) =
+      (case find_first (fn Print {name, args, ...} => name = a andalso args = b) old_prints of
+        NONE =>
+          (case AList.lookup (op =) print_functions a of
+            NONE => NONE
+          | SOME get_pr => new_print a b get_pr)
+      | some => some);
+
     val new_prints =
       if command_visible then
-        rev (Synchronized.value print_functions) |> map_filter (fn pr =>
-          (case find_first (fn Print {name, ...} => name = fst pr) old_prints of
-            NONE => new_print pr
-          | some => some))
+        distinct (op =) (fold (fn (a, _) => cons (a, [])) print_functions command_overlays)
+        |> map_filter get_print
       else filter (fn print => print_finished print andalso print_persistent print) old_prints;
   in
     if eq_list print_eq (old_prints, new_prints) then NONE else SOME new_prints
@@ -276,7 +286,7 @@
 
 val _ =
   print_function "print_state"
-    (fn {command_name} =>
+    (fn {command_name, ...} =>
       SOME {delay = NONE, pri = 1, persistent = true,
         print_fn = fn tr => fn st' =>
           let
diff -r 199e9fa5a5c2 -r 9fff9f78240a src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Fri Aug 02 14:26:09 2013 +0200
+++ b/src/Pure/PIDE/document.ML	Fri Aug 02 16:00:14 2013 +0200
@@ -100,7 +100,7 @@
 val visible_command = Inttab.defined o #visible o get_perspective;
 val visible_last = #visible_last o get_perspective;
 val visible_node = is_some o visible_last
-val overlays = #overlays o get_perspective;
+val overlays = Inttab.lookup_list o #overlays o get_perspective;
 
 fun map_entries f =
   map_node (fn (header, perspective, entries, result) => (header, perspective, f entries, result));
@@ -442,9 +442,10 @@
               SOME (eval, prints) =>
                 let
                   val command_visible = visible_command node command_id;
+                  val command_overlays = overlays node command_id;
                   val command_name = the_command_name state command_id;
                 in
-                  (case Command.print command_visible command_name eval prints of
+                  (case Command.print command_visible command_overlays command_name eval prints of
                     SOME prints' => assign_update_new (command_id, SOME (eval, prints'))
                   | NONE => I)
                 end
@@ -462,15 +463,18 @@
 
 fun illegal_init _ = error "Illegal theory header after end of theory";
 
-fun new_exec state proper_init command_visible command_id' (assign_update, command_exec, init) =
+fun new_exec state node proper_init command_id' (assign_update, command_exec, init) =
   if not proper_init andalso is_none init then NONE
   else
     let
       val (_, (eval, _)) = command_exec;
+
+      val command_visible = visible_command node command_id';
+      val command_overlays = overlays node command_id';
       val (command_name, span) = the_command state command_id' ||> Lazy.force;
 
       val eval' = Command.eval (fn () => the_default illegal_init init span) span eval;
-      val prints' = perhaps (Command.print command_visible command_name eval') [];
+      val prints' = perhaps (Command.print command_visible command_overlays command_name eval') [];
       val exec' = (eval', prints');
 
       val assign_update' = assign_update_new (command_id', SOME exec') assign_update;
@@ -525,7 +529,7 @@
                         iterate_entries_after common
                           (fn ((prev, id), _) => fn res =>
                             if not node_required andalso prev = visible_last node then NONE
-                            else new_exec state proper_init (visible_command node id) id res) node;
+                            else new_exec state node proper_init id res) node;
 
                     val assigned_execs =
                       (node0, updated_execs) |-> iterate_entries_after common
diff -r 199e9fa5a5c2 -r 9fff9f78240a src/Tools/try.ML
--- a/src/Tools/try.ML	Fri Aug 02 14:26:09 2013 +0200
+++ b/src/Tools/try.ML	Fri Aug 02 16:00:14 2013 +0200
@@ -117,7 +117,7 @@
 
 fun print_function ((name, (weight, auto, tool)): tool) =
   Command.print_function name
-    (fn {command_name} =>
+    (fn {command_name, ...} =>
       if Keyword.is_theory_goal command_name andalso Options.default_bool auto then
         SOME
          {delay = SOME (seconds (Options.default_real @{option auto_time_start})),