1.1 --- a/src/Pure/PIDE/command.ML Fri Aug 02 14:26:09 2013 +0200
1.2 +++ b/src/Pure/PIDE/command.ML Fri Aug 02 16:00:14 2013 +0200
1.3 @@ -14,10 +14,11 @@
1.4 val eval_result_state: eval -> Toplevel.state
1.5 val eval: (unit -> theory) -> Token.T list -> eval -> eval
1.6 type print
1.7 - val print: bool -> string -> eval -> print list -> print list option
1.8 + val print: bool -> (string * string list) list -> string ->
1.9 + eval -> print list -> print list option
1.10 type print_fn = Toplevel.transition -> Toplevel.state -> unit
1.11 val print_function: string ->
1.12 - ({command_name: string} ->
1.13 + ({command_name: string, args: string list} ->
1.14 {delay: Time.time option, pri: int, persistent: bool, print_fn: print_fn} option) -> unit
1.15 val no_print_function: string -> unit
1.16 type exec = eval * print list
1.17 @@ -195,13 +196,13 @@
1.18 (* print *)
1.19
1.20 datatype print = Print of
1.21 - {name: string, delay: Time.time option, pri: int, persistent: bool,
1.22 + {name: string, args: string list, delay: Time.time option, pri: int, persistent: bool,
1.23 exec_id: Document_ID.exec, print_process: unit memo};
1.24
1.25 type print_fn = Toplevel.transition -> Toplevel.state -> unit;
1.26
1.27 type print_function =
1.28 - {command_name: string} ->
1.29 + {command_name: string, args: string list} ->
1.30 {delay: Time.time option, pri: int, persistent: bool, print_fn: print_fn} option;
1.31
1.32 local
1.33 @@ -223,9 +224,11 @@
1.34
1.35 in
1.36
1.37 -fun print command_visible command_name eval old_prints =
1.38 +fun print command_visible command_overlays command_name eval old_prints =
1.39 let
1.40 - fun new_print (name, get_pr) =
1.41 + val print_functions = Synchronized.value print_functions;
1.42 +
1.43 + fun new_print name args get_pr =
1.44 let
1.45 fun make_print strict {delay, pri, persistent, print_fn} =
1.46 let
1.47 @@ -240,11 +243,12 @@
1.48 end;
1.49 in
1.50 Print {
1.51 - name = name, delay = delay, pri = pri, persistent = persistent,
1.52 + name = name, args = args, delay = delay, pri = pri, persistent = persistent,
1.53 exec_id = exec_id, print_process = memo exec_id process}
1.54 end;
1.55 + val params = {command_name = command_name, args = args};
1.56 in
1.57 - (case Exn.capture (Runtime.controlled_execution get_pr) {command_name = command_name} of
1.58 + (case Exn.capture (Runtime.controlled_execution get_pr) params of
1.59 Exn.Res NONE => NONE
1.60 | Exn.Res (SOME pr) => SOME (make_print false pr)
1.61 | Exn.Exn exn =>
1.62 @@ -252,12 +256,18 @@
1.63 {delay = NONE, pri = 0, persistent = false, print_fn = fn _ => fn _ => reraise exn}))
1.64 end;
1.65
1.66 + fun get_print (a, b) =
1.67 + (case find_first (fn Print {name, args, ...} => name = a andalso args = b) old_prints of
1.68 + NONE =>
1.69 + (case AList.lookup (op =) print_functions a of
1.70 + NONE => NONE
1.71 + | SOME get_pr => new_print a b get_pr)
1.72 + | some => some);
1.73 +
1.74 val new_prints =
1.75 if command_visible then
1.76 - rev (Synchronized.value print_functions) |> map_filter (fn pr =>
1.77 - (case find_first (fn Print {name, ...} => name = fst pr) old_prints of
1.78 - NONE => new_print pr
1.79 - | some => some))
1.80 + distinct (op =) (fold (fn (a, _) => cons (a, [])) print_functions command_overlays)
1.81 + |> map_filter get_print
1.82 else filter (fn print => print_finished print andalso print_persistent print) old_prints;
1.83 in
1.84 if eq_list print_eq (old_prints, new_prints) then NONE else SOME new_prints
1.85 @@ -276,7 +286,7 @@
1.86
1.87 val _ =
1.88 print_function "print_state"
1.89 - (fn {command_name} =>
1.90 + (fn {command_name, ...} =>
1.91 SOME {delay = NONE, pri = 1, persistent = true,
1.92 print_fn = fn tr => fn st' =>
1.93 let
2.1 --- a/src/Pure/PIDE/document.ML Fri Aug 02 14:26:09 2013 +0200
2.2 +++ b/src/Pure/PIDE/document.ML Fri Aug 02 16:00:14 2013 +0200
2.3 @@ -100,7 +100,7 @@
2.4 val visible_command = Inttab.defined o #visible o get_perspective;
2.5 val visible_last = #visible_last o get_perspective;
2.6 val visible_node = is_some o visible_last
2.7 -val overlays = #overlays o get_perspective;
2.8 +val overlays = Inttab.lookup_list o #overlays o get_perspective;
2.9
2.10 fun map_entries f =
2.11 map_node (fn (header, perspective, entries, result) => (header, perspective, f entries, result));
2.12 @@ -442,9 +442,10 @@
2.13 SOME (eval, prints) =>
2.14 let
2.15 val command_visible = visible_command node command_id;
2.16 + val command_overlays = overlays node command_id;
2.17 val command_name = the_command_name state command_id;
2.18 in
2.19 - (case Command.print command_visible command_name eval prints of
2.20 + (case Command.print command_visible command_overlays command_name eval prints of
2.21 SOME prints' => assign_update_new (command_id, SOME (eval, prints'))
2.22 | NONE => I)
2.23 end
2.24 @@ -462,15 +463,18 @@
2.25
2.26 fun illegal_init _ = error "Illegal theory header after end of theory";
2.27
2.28 -fun new_exec state proper_init command_visible command_id' (assign_update, command_exec, init) =
2.29 +fun new_exec state node proper_init command_id' (assign_update, command_exec, init) =
2.30 if not proper_init andalso is_none init then NONE
2.31 else
2.32 let
2.33 val (_, (eval, _)) = command_exec;
2.34 +
2.35 + val command_visible = visible_command node command_id';
2.36 + val command_overlays = overlays node command_id';
2.37 val (command_name, span) = the_command state command_id' ||> Lazy.force;
2.38
2.39 val eval' = Command.eval (fn () => the_default illegal_init init span) span eval;
2.40 - val prints' = perhaps (Command.print command_visible command_name eval') [];
2.41 + val prints' = perhaps (Command.print command_visible command_overlays command_name eval') [];
2.42 val exec' = (eval', prints');
2.43
2.44 val assign_update' = assign_update_new (command_id', SOME exec') assign_update;
2.45 @@ -525,7 +529,7 @@
2.46 iterate_entries_after common
2.47 (fn ((prev, id), _) => fn res =>
2.48 if not node_required andalso prev = visible_last node then NONE
2.49 - else new_exec state proper_init (visible_command node id) id res) node;
2.50 + else new_exec state node proper_init id res) node;
2.51
2.52 val assigned_execs =
2.53 (node0, updated_execs) |-> iterate_entries_after common
3.1 --- a/src/Tools/try.ML Fri Aug 02 14:26:09 2013 +0200
3.2 +++ b/src/Tools/try.ML Fri Aug 02 16:00:14 2013 +0200
3.3 @@ -117,7 +117,7 @@
3.4
3.5 fun print_function ((name, (weight, auto, tool)): tool) =
3.6 Command.print_function name
3.7 - (fn {command_name} =>
3.8 + (fn {command_name, ...} =>
3.9 if Keyword.is_theory_goal command_name andalso Options.default_bool auto then
3.10 SOME
3.11 {delay = SOME (seconds (Options.default_real @{option auto_time_start})),