--- 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
--- 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
--- 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})),