# HG changeset patch # User wenzelm # Date 1373034148 -7200 # Node ID c81d76f7f63dda7b3121629e57e5bd2a565ead3d # Parent 21f8e0e151f5ce47340ea5e6afaeca12673c60aa tuned signature; diff -r 21f8e0e151f5 -r c81d76f7f63d src/Pure/PIDE/command.ML --- a/src/Pure/PIDE/command.ML Fri Jul 05 16:01:45 2013 +0200 +++ b/src/Pure/PIDE/command.ML Fri Jul 05 16:22:28 2013 +0200 @@ -26,6 +26,13 @@ type print = {name: string, pri: int, exec_id: Document_ID.exec, print: unit memo} val print: string -> eval -> print list val print_function: {name: string, pri: int} -> (string -> print_fn option) -> unit + type exec = Document_ID.exec * (eval * print list) + val no_exec: exec + val exec_ids: exec -> Document_ID.exec list + val exec_result: exec -> eval_state + val exec_run: exec -> unit + val stable_eval: exec -> bool + val stable_print: print -> bool end; structure Command: COMMAND = @@ -80,6 +87,8 @@ end; +(** main phases: read -- eval -- print **) + (* read *) fun read span = @@ -233,5 +242,35 @@ (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st')); in if do_print then Toplevel.print_state false st' else () end)); + + +(** managed evaluation with potential interrupts **) + +(* execution *) + +type exec = Document_ID.exec * (eval * print list); +val no_exec: exec = (Document_ID.none, (no_eval, [])); + +fun exec_ids ((exec_id, (_, prints)): exec) = exec_id :: map #exec_id prints; + +fun exec_result ((_, (eval, _)): exec) = memo_result eval; + +fun exec_run ((_, (eval, prints)): exec) = + (memo_eval eval; + prints |> List.app (fn {name, pri, print, ...} => + memo_fork {name = name, group = NONE, deps = [], pri = pri, interrupts = true} print)); + + +(* stable situations *) + +fun stable_goals exec_id = + not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures exec_id))); + +fun stable_eval ((exec_id, (eval, _)): exec) = + stable_goals exec_id andalso memo_stable eval; + +fun stable_print ({exec_id, print, ...}: print) = + stable_goals exec_id andalso memo_stable print; + end; diff -r 21f8e0e151f5 -r c81d76f7f63d src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Fri Jul 05 16:01:45 2013 +0200 +++ b/src/Pure/PIDE/document.ML Fri Jul 05 16:22:28 2013 +0200 @@ -31,22 +31,6 @@ structure Document: DOCUMENT = struct -(* command execution *) - -type exec = Document_ID.exec * (Command.eval * Command.print list); (*eval/print process*) -val no_exec: exec = (Document_ID.none, (Command.no_eval, [])); - -fun exec_ids_of ((exec_id, (_, prints)): exec) = exec_id :: map #exec_id prints; - -fun exec_result ((_, (eval, _)): exec) = Command.memo_result eval; - -fun exec_run ((_, (eval, prints)): exec) = - (Command.memo_eval eval; - prints |> List.app (fn {name, pri, print, ...} => - Command.memo_fork {name = name, group = NONE, deps = [], pri = pri, interrupts = true} print)); - - - (** document structure **) fun err_dup kind id = error ("Duplicate " ^ kind ^ ": " ^ Document_ID.print id); @@ -59,7 +43,7 @@ abstype node = Node of {header: node_header, (*master directory, theory header, errors*) perspective: perspective, (*visible commands, last visible command*) - entries: exec option Entries.T * bool, (*command entries with excecutions, stable*) + entries: Command.exec option Entries.T * bool, (*command entries with excecutions, stable*) result: Command.eval option} (*result of last execution*) and version = Version of node String_Graph.T (*development graph wrt. static imports*) with @@ -152,8 +136,8 @@ NONE => err_undef "command entry" id | SOME (exec, _) => exec); -fun the_default_entry node (SOME id) = (id, the_default no_exec (the_entry node id)) - | the_default_entry _ NONE = (Document_ID.none, no_exec); +fun the_default_entry node (SOME id) = (id, the_default Command.no_exec (the_entry node id)) + | the_default_entry _ NONE = (Document_ID.none, Command.no_exec); fun update_entry id exec = map_entries (Entries.update (id, exec)); @@ -291,17 +275,6 @@ in (versions', commands', execution) end); -(* consolidated states *) - -fun stable_goals exec_id = - not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures exec_id))); - -fun stable_eval ((exec_id, (eval, _)): exec) = - stable_goals exec_id andalso Command.memo_stable eval; - -fun stable_print ({exec_id, print, ...}: Command.print) = - stable_goals exec_id andalso Command.memo_stable print; - fun finished_theory node = (case Exn.capture (Command.memo_result o the) (get_result node) of Exn.Res {state = st, ...} => can (Toplevel.end_theory Position.none) st @@ -334,7 +307,7 @@ (fn () => iterate_entries (fn (_, opt_exec) => fn () => (case opt_exec of - SOME exec => if ! running then SOME (exec_run exec) else NONE + SOME exec => if ! running then SOME (Command.exec_run exec) else NONE | NONE => NONE)) node ())))); in () end; @@ -406,7 +379,8 @@ | SOME (exec_id, exec) => (case lookup_entry node0 id of NONE => false - | SOME (exec_id0, _) => exec_id = exec_id0 andalso stable_eval (exec_id, exec))); + | SOME (exec_id0, _) => + exec_id = exec_id0 andalso Command.stable_eval (exec_id, exec))); in SOME (same', (prev, flags')) end else NONE; val (same, (common, flags)) = @@ -434,7 +408,7 @@ val eval' = Command.memo (fn () => let - val eval_state = exec_result (snd command_exec); + val eval_state = Command.exec_result (snd command_exec); val tr = Position.setmp_thread_data (Position.id_only (Document_ID.print exec_id')) (fn () => @@ -455,7 +429,7 @@ val prints' = new_prints |> map (fn new_print => (case find_first (fn {name, ...} => name = #name new_print) prints of - SOME print => if stable_print print then print else new_print + SOME print => if Command.stable_print print then print else new_print | NONE => new_print)); in if eq_list (op = o pairself #exec_id) (prints, prints') then NONE @@ -548,7 +522,7 @@ val command_execs = map (rpair []) (maps #1 updated) @ - map (fn (command_id, exec) => (command_id, exec_ids_of exec)) (maps #2 updated); + map (fn (command_id, exec) => (command_id, Command.exec_ids exec)) (maps #2 updated); val updated_nodes = map_filter #3 updated; val state' = state