# HG changeset patch # User wenzelm # Date 1373552774 -7200 # Node ID 75afb82daf5c1ed3b98a79c34188546a05228e22 # Parent d7871f38ffb4490b6c9137ff8fb5bf5b8b663cdb more abstract types; tuned signature; diff -r d7871f38ffb4 -r 75afb82daf5c src/Pure/PIDE/command.ML --- a/src/Pure/PIDE/command.ML Thu Jul 11 16:01:48 2013 +0200 +++ b/src/Pure/PIDE/command.ML Thu Jul 11 16:26:14 2013 +0200 @@ -6,25 +6,21 @@ signature COMMAND = sig - type eval_process - type eval = {exec_id: Document_ID.exec, eval_process: eval_process} + val read: (unit -> theory) -> Token.T list -> Toplevel.transition + type eval val eval_result_state: eval -> Toplevel.state val eval_same: eval * eval -> bool - type print_process - type print = - {name: string, pri: int, persistent: bool, - exec_id: Document_ID.exec, print_process: print_process} - type exec = eval * print list - val no_exec: exec - val exec_ids: exec option -> Document_ID.exec list - val read: (unit -> theory) -> Token.T list -> Toplevel.transition val eval: (unit -> theory) -> Token.T list -> eval -> eval + type print val print: bool -> string -> eval -> print list -> print list option type print_fn = Toplevel.transition -> Toplevel.state -> unit val print_function: {name: string, pri: int, persistent: bool} -> ({command_name: string} -> print_fn option) -> unit val no_print_function: string -> unit - val execute: exec -> unit + type exec = eval * print list + val no_exec: exec + val exec_ids: exec option -> Document_ID.exec list + val exec: exec -> unit end; structure Command: COMMAND = @@ -78,34 +74,6 @@ (** main phases of execution **) -(* type definitions *) - -type eval_state = - {failed: bool, malformed: bool, command: Toplevel.transition, state: Toplevel.state}; -val init_eval_state = - {failed = false, malformed = false, command = Toplevel.empty, state = Toplevel.toplevel}; - -type eval_process = eval_state memo; -type eval = {exec_id: Document_ID.exec, eval_process: eval_process}; - -fun eval_result ({eval_process, ...}: eval) = memo_result eval_process; -val eval_result_state = #state o eval_result; - -fun eval_same ({exec_id, ...}: eval, {exec_id = exec_id', ...}: eval) = - exec_id = exec_id' andalso Exec.is_stable exec_id; - -type print_process = unit memo; -type print = - {name: string, pri: int, persistent: bool, - exec_id: Document_ID.exec, print_process: print_process}; - -type exec = eval * print list; -val no_exec: exec = ({exec_id = Document_ID.none, eval_process = memo_value init_eval_state}, []); - -fun exec_ids (NONE: exec option) = [] - | exec_ids (SOME ({exec_id, ...}, prints)) = exec_id :: map #exec_id prints; - - (* read *) fun read init span = @@ -138,6 +106,19 @@ (* eval *) +type eval_state = + {failed: bool, malformed: bool, command: Toplevel.transition, state: Toplevel.state}; +val init_eval_state = + {failed = false, malformed = false, command = Toplevel.empty, state = Toplevel.toplevel}; + +datatype eval = Eval of {exec_id: Document_ID.exec, eval_process: eval_state memo}; + +fun eval_result (Eval {eval_process, ...}) = memo_result eval_process; +val eval_result_state = #state o eval_result; + +fun eval_same (Eval {exec_id, ...}, Eval {exec_id = exec_id', ...}) = + exec_id = exec_id' andalso Exec.is_stable exec_id; + local fun run int tr st = @@ -198,13 +179,17 @@ Position.setmp_thread_data (Position.id_only (Document_ID.print exec_id)) (fn () => read init span |> Toplevel.exec_id exec_id) (); in eval_state span tr (eval_result eval0) end; - in {exec_id = exec_id, eval_process = memo exec_id process} end; + in Eval {exec_id = exec_id, eval_process = memo exec_id process} end; end; (* print *) +datatype print = Print of + {name: string, pri: int, persistent: bool, + exec_id: Document_ID.exec, print_process: unit memo}; + type print_fn = Toplevel.transition -> Toplevel.state -> unit; local @@ -216,7 +201,9 @@ (Toplevel.setmp_thread_position tr o Runtime.controlled_execution) e () handle exn => List.app (Future.error_msg (Toplevel.pos_of tr)) (ML_Compiler.exn_messages_ids exn); -fun print_stable (print: print) = Exec.is_stable (#exec_id print); +fun print_persistent (Print {persistent, ...}) = persistent; +fun print_stable (Print {exec_id, ...}) = Exec.is_stable exec_id; +fun print_eq (Print {exec_id, ...}, Print {exec_id = exec_id', ...}) = exec_id = exec_id'; in @@ -236,8 +223,9 @@ else print_error tr (fn () => print_fn tr st') end; in - {name = name, pri = pri, persistent = persistent, - exec_id = exec_id, print_process = memo exec_id process} + Print { + name = name, pri = pri, persistent = persistent, + exec_id = exec_id, print_process = memo exec_id process} end; in (case Exn.capture (Runtime.controlled_execution get_fn) {command_name = command_name} of @@ -249,13 +237,12 @@ val new_prints = if command_visible then rev (Synchronized.value print_functions) |> map_filter (fn pr => - (case find_first (equal (fst pr) o #name) old_prints of + (case find_first (fn Print {name, ...} => name = fst pr) old_prints of SOME print => if print_stable print then SOME print else new_print pr | NONE => new_print pr)) - else filter (fn print => #persistent print andalso print_stable print) old_prints; + else filter (fn print => print_persistent print andalso print_stable print) old_prints; in - if eq_list (op = o pairself #exec_id) (old_prints, new_prints) then NONE - else SOME new_prints + if eq_list print_eq (old_prints, new_prints) then NONE else SOME new_prints end; fun print_function {name, pri, persistent} f = @@ -281,15 +268,29 @@ in if do_print then Toplevel.print_state false st' else () end)); -(* combined execution process *) +(* combined execution *) + +type exec = eval * print list; +val no_exec: exec = + (Eval {exec_id = Document_ID.none, eval_process = memo_value init_eval_state}, []); -fun run_print ({name, pri, print_process, ...}: print) = +fun exec_ids NONE = [] + | exec_ids (SOME (Eval {exec_id, ...}, prints)) = + exec_id :: map (fn Print {exec_id, ...} => exec_id) prints; + +local + +fun run_print (Print {name, pri, print_process, ...}) = (if Multithreading.enabled () then memo_fork {name = name, group = NONE, deps = [], pri = pri, interrupts = true} else memo_exec) print_process; -fun execute (({eval_process, ...}, prints): exec) = +in + +fun exec (Eval {eval_process, ...}, prints) = (memo_exec eval_process; List.app run_print prints); end; +end; + diff -r d7871f38ffb4 -r 75afb82daf5c src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Thu Jul 11 16:01:48 2013 +0200 +++ b/src/Pure/PIDE/document.ML Thu Jul 11 16:26:14 2013 +0200 @@ -334,7 +334,7 @@ (fn () => iterate_entries (fn (_, opt_exec) => fn () => (case opt_exec of - SOME exec => if running () then SOME (Command.execute exec) else NONE + SOME exec => if running () then SOME (Command.exec exec) else NONE | NONE => NONE)) node ())); in () end;