# HG changeset patch # User wenzelm # Date 1373546531 -7200 # Node ID 40298d3834639eaca7cfaa6dd97539e6b5ff42b2 # Parent 76883c1e1c530d3424aad9d2c5383c28c3e4aaec global management of command execution fragments; tuned; diff -r 76883c1e1c53 -r 40298d383463 src/Pure/PIDE/command.ML --- a/src/Pure/PIDE/command.ML Thu Jul 11 12:28:24 2013 +0200 +++ b/src/Pure/PIDE/command.ML Thu Jul 11 14:42:11 2013 +0200 @@ -9,6 +9,7 @@ type eval_process type eval = {exec_id: Document_ID.exec, eval_process: eval_process} val eval_result_state: eval -> Toplevel.state + val eval_same: eval * eval -> bool type print_process type print = {name: string, pri: int, persistent: bool, @@ -16,9 +17,6 @@ type exec = eval * print list val no_exec: exec val exec_ids: exec option -> Document_ID.exec list - val stable_eval: eval -> bool - val stable_print: print -> bool - val same_eval: eval * eval -> bool val read: (unit -> theory) -> Token.T list -> Toplevel.transition val eval: (unit -> theory) -> Token.T list -> eval -> eval val print: bool -> string -> eval -> print list -> print list option @@ -35,40 +33,42 @@ (** memo results -- including physical interrupts! **) datatype 'a expr = - Expr of unit -> 'a | + Expr of Document_ID.exec * (unit -> 'a) | Result of 'a Exn.result; abstype 'a memo = Memo of 'a expr Synchronized.var with -fun memo e = Memo (Synchronized.var "Command.memo" (Expr e)); +fun memo exec_id e = Memo (Synchronized.var "Command.memo" (Expr (exec_id, e))); fun memo_value a = Memo (Synchronized.var "Command.memo" (Result (Exn.Res a))); -fun memo_eval (Memo v) = - (case Synchronized.value v of - Result res => res - | _ => - Synchronized.guarded_access v - (fn Result res => SOME (res, Result res) - | Expr e => - let val res = Exn.capture e (); (*sic!*) - in SOME (res, Result res) end)) - |> Exn.release; - -fun memo_fork params (Memo v) = - (case Synchronized.value v of - Result _ => () - | _ => ignore ((singleton o Future.forks) params (fn () => memo_eval (Memo v)))); - fun memo_result (Memo v) = (case Synchronized.value v of Result res => Exn.release res | _ => raise Fail "Unfinished memo result"); -fun memo_stable (Memo v) = +fun memo_exec (Memo v) = (case Synchronized.value v of - Expr _ => true - | Result res => not (Exn.is_interrupt_exn res)); + Result res => res + | _ => + Synchronized.guarded_access v + (fn Result res => SOME (res, Result res) + | Expr (exec_id, e) => + uninterruptible (fn restore_attributes => fn () => + let + val _ = Exec.running exec_id; + val res = Exn.capture (restore_attributes e) (); + val _ = + if Exn.is_interrupt_exn res + then Exec.canceled exec_id + else Exec.finished exec_id; + in SOME (res, Result res) end) ())) + |> Exn.release; + +fun memo_fork params (Memo v) = + (case Synchronized.value v of + Result _ => () + | _ => ignore ((singleton o Future.forks) params (fn () => memo_exec (Memo v)))); end; @@ -76,7 +76,7 @@ (** main phases of execution **) -(* basic type definitions *) +(* type definitions *) type eval_state = {failed: bool, malformed: bool, command: Toplevel.transition, state: Toplevel.state}; @@ -89,6 +89,9 @@ 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, @@ -101,21 +104,6 @@ | exec_ids (SOME ({exec_id, ...}, prints)) = exec_id :: map #exec_id prints; -(* stable results *) - -fun stable_goals exec_id = - not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures exec_id))); - -fun stable_eval ({exec_id, eval_process}: eval) = - stable_goals exec_id andalso memo_stable eval_process; - -fun stable_print ({exec_id, print_process, ...}: print) = - stable_goals exec_id andalso memo_stable print_process; - -fun same_eval (eval: eval, eval': eval) = - #exec_id eval = #exec_id eval' andalso stable_eval eval'; - - (* read *) fun read init span = @@ -208,7 +196,7 @@ 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 process} end; + in {exec_id = exec_id, eval_process = memo exec_id process} end; end; @@ -226,6 +214,8 @@ (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); + in fun print command_visible command_name eval old_prints = @@ -245,7 +235,7 @@ end; in {name = name, pri = pri, persistent = persistent, - exec_id = exec_id, print_process = memo process} + 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 @@ -258,9 +248,9 @@ if command_visible then rev (Synchronized.value print_functions) |> map_filter (fn pr => (case find_first (equal (fst pr) o #name) old_prints of - SOME print => if stable_print print then SOME print else new_print pr + SOME print => if print_stable print then SOME print else new_print pr | NONE => new_print pr)) - else filter (fn print => #persistent print andalso stable_print print) old_prints; + else filter (fn 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 @@ -289,15 +279,15 @@ in if do_print then Toplevel.print_state false st' else () end)); -(* overall execution process *) +(* combined execution process *) fun run_print ({name, pri, print_process, ...}: print) = (if Multithreading.enabled () then memo_fork {name = name, group = NONE, deps = [], pri = pri, interrupts = true} - else memo_eval) print_process; + else memo_exec) print_process; fun execute (({eval_process, ...}, prints): exec) = - (memo_eval eval_process; List.app run_print prints); + (memo_exec eval_process; List.app run_print prints); end; diff -r 76883c1e1c53 -r 40298d383463 src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Thu Jul 11 12:28:24 2013 +0200 +++ b/src/Pure/PIDE/document.ML Thu Jul 11 14:42:11 2013 +0200 @@ -421,7 +421,7 @@ val flags' = update_flags prev flags; val same' = (case (lookup_entry node0 command_id, opt_exec) of - (SOME (eval0, _), SOME (eval, _)) => Command.same_eval (eval0, eval) + (SOME (eval0, _), SOME (eval, _)) => Command.eval_same (eval0, eval) | _ => false); val assign_update' = assign_update |> same' ? (case opt_exec of diff -r 76883c1e1c53 -r 40298d383463 src/Pure/PIDE/exec.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/PIDE/exec.ML Thu Jul 11 14:42:11 2013 +0200 @@ -0,0 +1,46 @@ +(* Title: Pure/PIDE/exec.ML + Author: Makarius + +Global management of command execution fragments. +*) + +signature EXEC = +sig + val is_stable: Document_ID.exec -> bool + val running: Document_ID.exec -> unit + val finished: Document_ID.exec -> unit + val canceled: Document_ID.exec -> unit + val purge_unstable: unit -> unit +end; + +structure Exec: EXEC = +struct + +val running_execs = + Synchronized.var "Exec.running_execs" (Inttab.empty: {stable: bool} Inttab.table); + +fun is_stable exec_id = + not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures exec_id))) andalso + (case Inttab.lookup (Synchronized.value running_execs) exec_id of + NONE => true + | SOME {stable} => stable); + +fun running exec_id = + Synchronized.change running_execs (Inttab.update_new (exec_id, {stable = true})); + +fun finished exec_id = + Synchronized.change running_execs (Inttab.delete exec_id); + +fun canceled exec_id = + Synchronized.change running_execs (Inttab.update (exec_id, {stable = false})); + +fun purge_unstable () = + Synchronized.guarded_access running_execs + (fn tab => + let + val unstable = Inttab.fold (fn (exec_id, {stable = false}) => cons exec_id | _ => I) tab []; + val tab' = fold Inttab.delete unstable tab; + in SOME ((), tab') end); + +end; + diff -r 76883c1e1c53 -r 40298d383463 src/Pure/PIDE/protocol.ML --- a/src/Pure/PIDE/protocol.ML Thu Jul 11 12:28:24 2013 +0200 +++ b/src/Pure/PIDE/protocol.ML Thu Jul 11 14:42:11 2013 +0200 @@ -60,6 +60,7 @@ |> YXML.string_of_body); val _ = List.app Future.cancel_group (Goal.reset_futures ()); + val _ = Exec.purge_unstable (); val _ = Isabelle_Process.reset_tracing (); val _ = Event_Timer.request (Time.+ (Time.now (), seconds 0.02)) diff -r 76883c1e1c53 -r 40298d383463 src/Pure/ROOT --- a/src/Pure/ROOT Thu Jul 11 12:28:24 2013 +0200 +++ b/src/Pure/ROOT Thu Jul 11 14:42:11 2013 +0200 @@ -150,6 +150,7 @@ "ML/ml_syntax.ML" "ML/ml_thms.ML" "PIDE/active.ML" + "PIDE/exec.ML" "PIDE/command.ML" "PIDE/document.ML" "PIDE/document_id.ML" diff -r 76883c1e1c53 -r 40298d383463 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Thu Jul 11 12:28:24 2013 +0200 +++ b/src/Pure/ROOT.ML Thu Jul 11 14:42:11 2013 +0200 @@ -267,6 +267,7 @@ use "Isar/outer_syntax.ML"; use "General/graph_display.ML"; use "Thy/present.ML"; +use "PIDE/exec.ML"; use "PIDE/command.ML"; use "Thy/thy_load.ML"; use "Thy/thy_info.ML";