more abstract types;
authorwenzelm
Thu Jul 11 16:26:14 2013 +0200 (2013-07-11 ago)
changeset 5260075afb82daf5c
parent 52599 d7871f38ffb4
child 52601 55e62a25a7ce
more abstract types;
tuned signature;
src/Pure/PIDE/command.ML
src/Pure/PIDE/document.ML
     1.1 --- a/src/Pure/PIDE/command.ML	Thu Jul 11 16:01:48 2013 +0200
     1.2 +++ b/src/Pure/PIDE/command.ML	Thu Jul 11 16:26:14 2013 +0200
     1.3 @@ -6,25 +6,21 @@
     1.4  
     1.5  signature COMMAND =
     1.6  sig
     1.7 -  type eval_process
     1.8 -  type eval = {exec_id: Document_ID.exec, eval_process: eval_process}
     1.9 +  val read: (unit -> theory) -> Token.T list -> Toplevel.transition
    1.10 +  type eval
    1.11    val eval_result_state: eval -> Toplevel.state
    1.12    val eval_same: eval * eval -> bool
    1.13 -  type print_process
    1.14 -  type print =
    1.15 -   {name: string, pri: int, persistent: bool,
    1.16 -    exec_id: Document_ID.exec, print_process: print_process}
    1.17 -  type exec = eval * print list
    1.18 -  val no_exec: exec
    1.19 -  val exec_ids: exec option -> Document_ID.exec list
    1.20 -  val read: (unit -> theory) -> Token.T list -> Toplevel.transition
    1.21    val eval: (unit -> theory) -> Token.T list -> eval -> eval
    1.22 +  type print
    1.23    val print: bool -> string -> eval -> print list -> print list option
    1.24    type print_fn = Toplevel.transition -> Toplevel.state -> unit
    1.25    val print_function: {name: string, pri: int, persistent: bool} ->
    1.26      ({command_name: string} -> print_fn option) -> unit
    1.27    val no_print_function: string -> unit
    1.28 -  val execute: exec -> unit
    1.29 +  type exec = eval * print list
    1.30 +  val no_exec: exec
    1.31 +  val exec_ids: exec option -> Document_ID.exec list
    1.32 +  val exec: exec -> unit
    1.33  end;
    1.34  
    1.35  structure Command: COMMAND =
    1.36 @@ -78,34 +74,6 @@
    1.37  
    1.38  (** main phases of execution **)
    1.39  
    1.40 -(* type definitions *)
    1.41 -
    1.42 -type eval_state =
    1.43 -  {failed: bool, malformed: bool, command: Toplevel.transition, state: Toplevel.state};
    1.44 -val init_eval_state =
    1.45 -  {failed = false, malformed = false, command = Toplevel.empty, state = Toplevel.toplevel};
    1.46 -
    1.47 -type eval_process = eval_state memo;
    1.48 -type eval = {exec_id: Document_ID.exec, eval_process: eval_process};
    1.49 -
    1.50 -fun eval_result ({eval_process, ...}: eval) = memo_result eval_process;
    1.51 -val eval_result_state = #state o eval_result;
    1.52 -
    1.53 -fun eval_same ({exec_id, ...}: eval, {exec_id = exec_id', ...}: eval) =
    1.54 -  exec_id = exec_id' andalso Exec.is_stable exec_id;
    1.55 -
    1.56 -type print_process = unit memo;
    1.57 -type print =
    1.58 - {name: string, pri: int, persistent: bool,
    1.59 -  exec_id: Document_ID.exec, print_process: print_process};
    1.60 -
    1.61 -type exec = eval * print list;
    1.62 -val no_exec: exec = ({exec_id = Document_ID.none, eval_process = memo_value init_eval_state}, []);
    1.63 -
    1.64 -fun exec_ids (NONE: exec option) = []
    1.65 -  | exec_ids (SOME ({exec_id, ...}, prints)) = exec_id :: map #exec_id prints;
    1.66 -
    1.67 -
    1.68  (* read *)
    1.69  
    1.70  fun read init span =
    1.71 @@ -138,6 +106,19 @@
    1.72  
    1.73  (* eval *)
    1.74  
    1.75 +type eval_state =
    1.76 +  {failed: bool, malformed: bool, command: Toplevel.transition, state: Toplevel.state};
    1.77 +val init_eval_state =
    1.78 +  {failed = false, malformed = false, command = Toplevel.empty, state = Toplevel.toplevel};
    1.79 +
    1.80 +datatype eval = Eval of {exec_id: Document_ID.exec, eval_process: eval_state memo};
    1.81 +
    1.82 +fun eval_result (Eval {eval_process, ...}) = memo_result eval_process;
    1.83 +val eval_result_state = #state o eval_result;
    1.84 +
    1.85 +fun eval_same (Eval {exec_id, ...}, Eval {exec_id = exec_id', ...}) =
    1.86 +  exec_id = exec_id' andalso Exec.is_stable exec_id;
    1.87 +
    1.88  local
    1.89  
    1.90  fun run int tr st =
    1.91 @@ -198,13 +179,17 @@
    1.92            Position.setmp_thread_data (Position.id_only (Document_ID.print exec_id))
    1.93              (fn () => read init span |> Toplevel.exec_id exec_id) ();
    1.94        in eval_state span tr (eval_result eval0) end;
    1.95 -  in {exec_id = exec_id, eval_process = memo exec_id process} end;
    1.96 +  in Eval {exec_id = exec_id, eval_process = memo exec_id process} end;
    1.97  
    1.98  end;
    1.99  
   1.100  
   1.101  (* print *)
   1.102  
   1.103 +datatype print = Print of
   1.104 + {name: string, pri: int, persistent: bool,
   1.105 +  exec_id: Document_ID.exec, print_process: unit memo};
   1.106 +
   1.107  type print_fn = Toplevel.transition -> Toplevel.state -> unit;
   1.108  
   1.109  local
   1.110 @@ -216,7 +201,9 @@
   1.111    (Toplevel.setmp_thread_position tr o Runtime.controlled_execution) e () handle exn =>
   1.112      List.app (Future.error_msg (Toplevel.pos_of tr)) (ML_Compiler.exn_messages_ids exn);
   1.113  
   1.114 -fun print_stable (print: print) = Exec.is_stable (#exec_id print);
   1.115 +fun print_persistent (Print {persistent, ...}) = persistent;
   1.116 +fun print_stable (Print {exec_id, ...}) = Exec.is_stable exec_id;
   1.117 +fun print_eq (Print {exec_id, ...}, Print {exec_id = exec_id', ...}) = exec_id = exec_id';
   1.118  
   1.119  in
   1.120  
   1.121 @@ -236,8 +223,9 @@
   1.122                  else print_error tr (fn () => print_fn tr st')
   1.123                end;
   1.124            in
   1.125 -           {name = name, pri = pri, persistent = persistent,
   1.126 -            exec_id = exec_id, print_process = memo exec_id process}
   1.127 +           Print {
   1.128 +             name = name, pri = pri, persistent = persistent,
   1.129 +             exec_id = exec_id, print_process = memo exec_id process}
   1.130            end;
   1.131        in
   1.132          (case Exn.capture (Runtime.controlled_execution get_fn) {command_name = command_name} of
   1.133 @@ -249,13 +237,12 @@
   1.134      val new_prints =
   1.135        if command_visible then
   1.136          rev (Synchronized.value print_functions) |> map_filter (fn pr =>
   1.137 -          (case find_first (equal (fst pr) o #name) old_prints of
   1.138 +          (case find_first (fn Print {name, ...} => name = fst pr) old_prints of
   1.139              SOME print => if print_stable print then SOME print else new_print pr
   1.140            | NONE => new_print pr))
   1.141 -      else filter (fn print => #persistent print andalso print_stable print) old_prints;
   1.142 +      else filter (fn print => print_persistent print andalso print_stable print) old_prints;
   1.143    in
   1.144 -    if eq_list (op = o pairself #exec_id) (old_prints, new_prints) then NONE
   1.145 -    else SOME new_prints
   1.146 +    if eq_list print_eq (old_prints, new_prints) then NONE else SOME new_prints
   1.147    end;
   1.148  
   1.149  fun print_function {name, pri, persistent} f =
   1.150 @@ -281,15 +268,29 @@
   1.151        in if do_print then Toplevel.print_state false st' else () end));
   1.152  
   1.153  
   1.154 -(* combined execution process *)
   1.155 +(* combined execution *)
   1.156 +
   1.157 +type exec = eval * print list;
   1.158 +val no_exec: exec =
   1.159 +  (Eval {exec_id = Document_ID.none, eval_process = memo_value init_eval_state}, []);
   1.160  
   1.161 -fun run_print ({name, pri, print_process, ...}: print) =
   1.162 +fun exec_ids NONE = []
   1.163 +  | exec_ids (SOME (Eval {exec_id, ...}, prints)) =
   1.164 +      exec_id :: map (fn Print {exec_id, ...} => exec_id) prints;
   1.165 +
   1.166 +local
   1.167 +
   1.168 +fun run_print (Print {name, pri, print_process, ...}) =
   1.169    (if Multithreading.enabled () then
   1.170      memo_fork {name = name, group = NONE, deps = [], pri = pri, interrupts = true}
   1.171    else memo_exec) print_process;
   1.172  
   1.173 -fun execute (({eval_process, ...}, prints): exec) =
   1.174 +in
   1.175 +
   1.176 +fun exec (Eval {eval_process, ...}, prints) =
   1.177    (memo_exec eval_process; List.app run_print prints);
   1.178  
   1.179  end;
   1.180  
   1.181 +end;
   1.182 +
     2.1 --- a/src/Pure/PIDE/document.ML	Thu Jul 11 16:01:48 2013 +0200
     2.2 +++ b/src/Pure/PIDE/document.ML	Thu Jul 11 16:26:14 2013 +0200
     2.3 @@ -334,7 +334,7 @@
     2.4                  (fn () =>
     2.5                    iterate_entries (fn (_, opt_exec) => fn () =>
     2.6                      (case opt_exec of
     2.7 -                      SOME exec => if running () then SOME (Command.execute exec) else NONE
     2.8 +                      SOME exec => if running () then SOME (Command.exec exec) else NONE
     2.9                      | NONE => NONE)) node ()));
    2.10    in () end;
    2.11