support print functions with explicit arguments, as provided by overlays;
authorwenzelm
Fri Aug 02 16:00:14 2013 +0200 (2013-08-02)
changeset 528509fff9f78240a
parent 52849 199e9fa5a5c2
child 52851 e71b5160f242
support print functions with explicit arguments, as provided by overlays;
src/Pure/PIDE/command.ML
src/Pure/PIDE/document.ML
src/Tools/try.ML
     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})),