1.1 --- a/src/Pure/PIDE/command.ML Thu Jul 04 12:02:11 2013 +0200
1.2 +++ b/src/Pure/PIDE/command.ML Thu Jul 04 16:04:53 2013 +0200
1.3 @@ -13,16 +13,19 @@
1.4 val memo: (unit -> 'a) -> 'a memo
1.5 val memo_value: 'a -> 'a memo
1.6 val memo_eval: 'a memo -> 'a
1.7 + val memo_fork: Future.params -> 'a memo -> unit
1.8 val memo_result: 'a memo -> 'a
1.9 + val memo_stable: 'a memo -> bool
1.10 val read: span -> Toplevel.transition
1.11 - val eval: span -> Toplevel.transition ->
1.12 - Toplevel.state * {malformed: bool} -> {failed: bool} * (Toplevel.state * {malformed: bool})
1.13 - type print = {name: string, pri: int, pr: unit lazy}
1.14 - val print: Toplevel.state -> Toplevel.transition -> Toplevel.state -> print list
1.15 - type print_function =
1.16 - {old_state: Toplevel.state, tr: Toplevel.transition, state: Toplevel.state} ->
1.17 - (unit -> unit) option
1.18 - val print_function: string -> int -> print_function -> unit
1.19 + type eval_state =
1.20 + {failed: bool, malformed: bool, command: Toplevel.transition, state: Toplevel.state}
1.21 + type eval = eval_state memo
1.22 + val no_eval: eval
1.23 + val eval: span -> Toplevel.transition -> eval_state -> eval_state
1.24 + type print_fn = Toplevel.transition -> Toplevel.state -> unit
1.25 + type print = {name: string, pri: int, print: unit memo}
1.26 + val print: string -> eval -> print list
1.27 + val print_function: {name: string, pri: int} -> (string -> print_fn option) -> unit
1.28 end;
1.29
1.30 structure Command: COMMAND =
1.31 @@ -59,11 +62,21 @@
1.32 in SOME (res, Result res) end))
1.33 |> Exn.release;
1.34
1.35 +fun memo_fork params (Memo v) =
1.36 + (case Synchronized.value v of
1.37 + Result _ => ()
1.38 + | _ => ignore ((singleton o Future.forks) params (fn () => memo_eval (Memo v))));
1.39 +
1.40 fun memo_result (Memo v) =
1.41 (case Synchronized.value v of
1.42 Result res => Exn.release res
1.43 | _ => raise Fail "Unfinished memo result");
1.44
1.45 +fun memo_stable (Memo v) =
1.46 + (case Synchronized.value v of
1.47 + Expr _ => true
1.48 + | Result res => not (Exn.is_interrupt_exn res));
1.49 +
1.50 end;
1.51
1.52
1.53 @@ -98,6 +111,14 @@
1.54
1.55 (* eval *)
1.56
1.57 +type eval_state =
1.58 + {failed: bool, malformed: bool, command: Toplevel.transition, state: Toplevel.state};
1.59 +val no_eval_state: eval_state =
1.60 + {failed = false, malformed = false, command = Toplevel.empty, state = Toplevel.toplevel};
1.61 +
1.62 +type eval = eval_state memo;
1.63 +val no_eval = memo_value no_eval_state;
1.64 +
1.65 local
1.66
1.67 fun run int tr st =
1.68 @@ -120,9 +141,9 @@
1.69
1.70 in
1.71
1.72 -fun eval span tr (st, {malformed}) =
1.73 +fun eval span tr ({malformed, state = st, ...}: eval_state) =
1.74 if malformed then
1.75 - ({failed = true}, (Toplevel.toplevel, {malformed = malformed}))
1.76 + {failed = true, malformed = malformed, command = tr, state = Toplevel.toplevel}
1.77 else
1.78 let
1.79 val malformed' = Toplevel.is_malformed tr;
1.80 @@ -142,11 +163,11 @@
1.81 let
1.82 val _ = if null errs then Exn.interrupt () else ();
1.83 val _ = Toplevel.status tr Markup.failed;
1.84 - in ({failed = true}, (st, {malformed = malformed'})) end
1.85 + in {failed = true, malformed = malformed', command = tr, state = st} end
1.86 | SOME st' =>
1.87 let
1.88 val _ = proof_status tr st';
1.89 - in ({failed = false}, (st', {malformed = malformed'})) end)
1.90 + in {failed = false, malformed = malformed', command = tr, state = st'} end)
1.91 end;
1.92
1.93 end;
1.94 @@ -154,16 +175,13 @@
1.95
1.96 (* print *)
1.97
1.98 -type print_function =
1.99 - {old_state: Toplevel.state, tr: Toplevel.transition, state: Toplevel.state} ->
1.100 - (unit -> unit) option;
1.101 -
1.102 -type print = {name: string, pri: int, pr: unit lazy};
1.103 +type print = {name: string, pri: int, print: unit memo};
1.104 +type print_fn = Toplevel.transition -> Toplevel.state -> unit;
1.105
1.106 local
1.107
1.108 -val print_functions =
1.109 - Synchronized.var "Command.print_functions" ([]: (string * (int * print_function)) list);
1.110 +type print_function = string * (int * (string -> print_fn option));
1.111 +val print_functions = Synchronized.var "Command.print_functions" ([]: print_function list);
1.112
1.113 fun output_error tr exn =
1.114 List.app (Future.error_msg (Toplevel.pos_of tr)) (ML_Compiler.exn_messages_ids exn);
1.115 @@ -174,14 +192,20 @@
1.116
1.117 in
1.118
1.119 -fun print st tr st' =
1.120 - rev (Synchronized.value print_functions) |> map_filter (fn (name, (pri, f)) =>
1.121 - (case Exn.capture (Runtime.controlled_execution f) {old_state = st, tr = tr, state = st'} of
1.122 +fun print command_name eval =
1.123 + rev (Synchronized.value print_functions) |> map_filter (fn (name, (pri, get_print_fn)) =>
1.124 + (case Exn.capture (Runtime.controlled_execution get_print_fn) command_name of
1.125 Exn.Res NONE => NONE
1.126 - | Exn.Res (SOME pr) => SOME {name = name, pri = pri, pr = (Lazy.lazy o print_error tr) pr}
1.127 - | Exn.Exn exn => SOME {name = name, pri = pri, pr = Lazy.lazy (fn () => output_error tr exn)}));
1.128 + | Exn.Res (SOME print_fn) =>
1.129 + SOME {name = name, pri = pri,
1.130 + print = memo (fn () =>
1.131 + let val {failed, command = tr, state = st', ...} = memo_result eval
1.132 + in if failed then () else print_error tr (fn () => print_fn tr st') () end)}
1.133 + | Exn.Exn exn =>
1.134 + SOME {name = name, pri = pri,
1.135 + print = memo (fn () => output_error (#command (memo_result eval)) exn)}));
1.136
1.137 -fun print_function name pri f =
1.138 +fun print_function {name, pri} f =
1.139 Synchronized.change print_functions (fn funs =>
1.140 (if not (AList.defined (op =) funs name) then ()
1.141 else warning ("Redefining command print function: " ^ quote name);
1.142 @@ -189,14 +213,15 @@
1.143
1.144 end;
1.145
1.146 -val _ = print_function "print_state" 0 (fn {tr, state, ...} =>
1.147 - let
1.148 - val is_init = Toplevel.is_init tr;
1.149 - val is_proof = Keyword.is_proof (Toplevel.name_of tr);
1.150 - val do_print =
1.151 - not is_init andalso
1.152 - (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof state));
1.153 - in if do_print then SOME (fn () => Toplevel.print_state false state) else NONE end);
1.154 +val _ =
1.155 + print_function {name = "print_state", pri = 0} (fn command_name => SOME (fn tr => fn st' =>
1.156 + let
1.157 + val is_init = Keyword.is_theory_begin command_name;
1.158 + val is_proof = Keyword.is_proof command_name;
1.159 + val do_print =
1.160 + not is_init andalso
1.161 + (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st'));
1.162 + in if do_print then Toplevel.print_state false st' else () end));
1.163
1.164 end;
1.165