print "persistent" flag allows to adjust tradeoff of ML run-time vs. JVM heap-space;
1.1 --- a/src/Pure/PIDE/command.ML Wed Jul 10 11:32:49 2013 +0200
1.2 +++ b/src/Pure/PIDE/command.ML Wed Jul 10 12:10:32 2013 +0200
1.3 @@ -10,7 +10,9 @@
1.4 type eval = {exec_id: Document_ID.exec, eval_process: eval_process}
1.5 val eval_result_state: eval -> Toplevel.state
1.6 type print_process
1.7 - type print = {name: string, pri: int, exec_id: Document_ID.exec, print_process: print_process}
1.8 + type print =
1.9 + {name: string, pri: int, persistent: bool,
1.10 + exec_id: Document_ID.exec, print_process: print_process}
1.11 type exec = eval * print list
1.12 val no_exec: exec
1.13 val exec_ids: exec option -> Document_ID.exec list
1.14 @@ -20,7 +22,8 @@
1.15 val eval: (unit -> theory) -> Token.T list -> eval -> eval
1.16 val print: bool -> string -> eval -> print list -> print list option
1.17 type print_fn = Toplevel.transition -> Toplevel.state -> unit
1.18 - val print_function: {name: string, pri: int} -> (string -> print_fn option) -> unit
1.19 + val print_function: {name: string, pri: int, persistent: bool} ->
1.20 + ({command_name: string} -> print_fn option) -> unit
1.21 val no_print_function: string -> unit
1.22 val execute: exec -> unit
1.23 end;
1.24 @@ -86,7 +89,9 @@
1.25 val eval_result_state = #state o eval_result;
1.26
1.27 type print_process = unit memo;
1.28 -type print = {name: string, pri: int, exec_id: Document_ID.exec, print_process: print_process};
1.29 +type print =
1.30 + {name: string, pri: int, persistent: bool,
1.31 + exec_id: Document_ID.exec, print_process: print_process};
1.32
1.33 type exec = eval * print list;
1.34 val no_exec: exec = ({exec_id = Document_ID.none, eval_process = memo_value init_eval_state}, []);
1.35 @@ -210,7 +215,7 @@
1.36
1.37 local
1.38
1.39 -type print_function = string * (int * (string -> print_fn option));
1.40 +type print_function = string * (int * bool * ({command_name: string} -> print_fn option));
1.41 val print_functions = Synchronized.var "Command.print_functions" ([]: print_function list);
1.42
1.43 fun print_error tr e =
1.44 @@ -221,7 +226,7 @@
1.45
1.46 fun print command_visible command_name eval old_prints =
1.47 let
1.48 - fun new_print (name, (pri, get_print_fn)) =
1.49 + fun new_print (name, (pri, persistent, get_fn)) =
1.50 let
1.51 fun make_print strict print_fn =
1.52 let
1.53 @@ -234,9 +239,12 @@
1.54 if failed andalso not strict then ()
1.55 else print_error tr (fn () => print_fn tr st')
1.56 end;
1.57 - in {name = name, pri = pri, exec_id = exec_id, print_process = memo process} end;
1.58 + in
1.59 + {name = name, pri = pri, persistent = persistent,
1.60 + exec_id = exec_id, print_process = memo process}
1.61 + end;
1.62 in
1.63 - (case Exn.capture (Runtime.controlled_execution get_print_fn) command_name of
1.64 + (case Exn.capture (Runtime.controlled_execution get_fn) {command_name = command_name} of
1.65 Exn.Res NONE => NONE
1.66 | Exn.Res (SOME print_fn) => SOME (make_print false print_fn)
1.67 | Exn.Exn exn => SOME (make_print true (fn _ => fn _ => reraise exn)))
1.68 @@ -248,17 +256,17 @@
1.69 (case find_first (equal (fst pr) o #name) old_prints of
1.70 SOME print => if stable_print print then SOME print else new_print pr
1.71 | NONE => new_print pr))
1.72 - else filter stable_print old_prints;
1.73 + else filter (fn print => #persistent print andalso stable_print print) old_prints;
1.74 in
1.75 if eq_list (op = o pairself #exec_id) (old_prints, new_prints) then NONE
1.76 else SOME new_prints
1.77 end;
1.78
1.79 -fun print_function {name, pri} f =
1.80 +fun print_function {name, pri, persistent} f =
1.81 Synchronized.change print_functions (fn funs =>
1.82 (if not (AList.defined (op =) funs name) then ()
1.83 else warning ("Redefining command print function: " ^ quote name);
1.84 - AList.update (op =) (name, (pri, f)) funs));
1.85 + AList.update (op =) (name, (pri, persistent, f)) funs));
1.86
1.87 fun no_print_function name =
1.88 Synchronized.change print_functions (filter_out (equal name o #1));
1.89 @@ -266,14 +274,15 @@
1.90 end;
1.91
1.92 val _ =
1.93 - print_function {name = "print_state", pri = 0} (fn command_name => SOME (fn tr => fn st' =>
1.94 - let
1.95 - val is_init = Keyword.is_theory_begin command_name;
1.96 - val is_proof = Keyword.is_proof command_name;
1.97 - val do_print =
1.98 - not is_init andalso
1.99 - (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st'));
1.100 - in if do_print then Toplevel.print_state false st' else () end));
1.101 + print_function {name = "print_state", pri = 0, persistent = true}
1.102 + (fn {command_name} => SOME (fn tr => fn st' =>
1.103 + let
1.104 + val is_init = Keyword.is_theory_begin command_name;
1.105 + val is_proof = Keyword.is_proof command_name;
1.106 + val do_print =
1.107 + not is_init andalso
1.108 + (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st'));
1.109 + in if do_print then Toplevel.print_state false st' else () end));
1.110
1.111
1.112 (* overall execution process *)