# HG changeset patch # User wenzelm # Date 1333619926 -7200 # Node ID 00f6279bb67ad2c94b74c909c477b6991187d334 # Parent 9bbf7fd96bcd8c2ff13cb5f40f8f170a83168161 Command.memo including physical interrupts (unlike Lazy.lazy); re-assign unstable exec, i.e. reset interrupted transaction; node result as direct exec -- avoid potential interrupt instability of Lazy.map; diff -r 9bbf7fd96bcd -r 00f6279bb67a src/Pure/PIDE/command.ML --- a/src/Pure/PIDE/command.ML Thu Apr 05 10:45:53 2012 +0200 +++ b/src/Pure/PIDE/command.ML Thu Apr 05 11:58:46 2012 +0200 @@ -7,13 +7,18 @@ signature COMMAND = sig val parse_command: string -> string -> Token.T list + type 'a memo + val memo: (unit -> 'a) -> 'a memo + val memo_value: 'a -> 'a memo + val memo_result: 'a memo -> 'a Exn.result + val memo_stable: 'a memo -> bool val run_command: Toplevel.transition -> Toplevel.state -> Toplevel.state * unit lazy end; structure Command: COMMAND = struct -(* parse *) +(* parse command *) fun parse_command id text = Position.setmp_thread_data (Position.id_only id) @@ -24,7 +29,37 @@ in toks end) (); -(* run *) +(* memo results *) + +datatype 'a expr = + Expr of 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_value a = Memo (Synchronized.var "Command.memo" (Result (Exn.Res a))); + +fun memo_result (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 (); (*memoing of physical interrupts!*) + in SOME (res, Result res) end)); + +fun memo_stable (Memo v) = + (case Synchronized.value v of + Result (Exn.Exn exn) => not (Exn.is_interrupt exn) + | _ => true); + +end; + + +(* run command *) local diff -r 9bbf7fd96bcd -r 00f6279bb67a src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Thu Apr 05 10:45:53 2012 +0200 +++ b/src/Pure/PIDE/document.ML Thu Apr 05 11:58:46 2012 +0200 @@ -62,8 +62,8 @@ type perspective = (command_id -> bool) * command_id option; (*visible commands, last*) structure Entries = Linear_Set(type key = command_id val ord = int_ord); -type exec = (Toplevel.state * unit lazy) lazy; (*eval/print process*) -val no_exec = (no_id, Lazy.value (Toplevel.toplevel, Lazy.value ())); +type exec = (Toplevel.state * unit lazy) Command.memo; (*eval/print process*) +val no_exec = Command.memo_value (Toplevel.toplevel, Lazy.value ()); abstype node = Node of {touched: bool, @@ -71,7 +71,7 @@ perspective: perspective, entries: (exec_id * exec) option Entries.T, (*command entries with excecutions*) last_exec: command_id option, (*last command with exec state assignment*) - result: Toplevel.state lazy} + result: exec} and version = Version of node Graph.T (*development graph wrt. static imports*) with @@ -87,11 +87,10 @@ val no_header = Exn.Exn (ERROR "Bad theory header"); val no_perspective = make_perspective []; -val no_result = Lazy.value Toplevel.toplevel; -val empty_node = make_node (false, no_header, no_perspective, Entries.empty, NONE, no_result); +val empty_node = make_node (false, no_header, no_perspective, Entries.empty, NONE, no_exec); val clear_node = map_node (fn (_, header, _, _, _, _) => - (false, header, no_perspective, Entries.empty, NONE, no_result)); + (false, header, no_perspective, Entries.empty, NONE, no_exec)); (* basic components *) @@ -159,8 +158,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 = (no_id, no_exec); +fun the_default_entry node (SOME id) = (id, (the_default (no_id, no_exec) (the_entry node id))) + | the_default_entry _ NONE = (no_id, (no_id, no_exec)); fun update_entry id exec = map_entries (Entries.update (id, exec)); @@ -193,7 +192,7 @@ fold (fn desc => update_node desc (set_touched true #> - desc <> name ? (map_entries (reset_after NONE) #> set_result no_result))) + desc <> name ? (map_entries (reset_after NONE) #> set_result no_exec))) (Graph.all_succs nodes [name]) nodes; in @@ -338,8 +337,8 @@ SOME thy => thy | NONE => Toplevel.end_theory (Position.file_only import) - (Lazy.force - (get_result (snd (Future.join (the (AList.lookup (op =) deps import)))))))); + (fst (Exn.release (Command.memo_result + (get_result (snd (Future.join (the (AList.lookup (op =) deps import)))))))))); in Thy_Load.begin_theory master_dir header parents end; fun check_theory nodes name = @@ -363,6 +362,7 @@ (case opt_exec of NONE => true | SOME (exec_id, exec) => + not (Command.memo_stable exec) orelse (case lookup_entry node0 id of NONE => true | SOME (exec_id0, _) => exec_id <> exec_id0)); @@ -395,8 +395,9 @@ #1 (Outer_Syntax.read_span (#2 (Outer_Syntax.get_syntax ())) span) |> modify_init |> Toplevel.put_id exec_id'_string); - val exec' = - snd (snd command_exec) |> Lazy.map (fn (st, _) => Command.run_command (tr ()) st); + val exec' = Command.memo (fn () => + let val (st, _) = Exn.release (Command.memo_result (snd (snd command_exec))); + in Command.run_command (tr ()) st end); val command_exec' = (command_id', (exec_id', exec')); in SOME (command_exec' :: execs, command_exec', init') end; @@ -448,8 +449,8 @@ val last_exec = if command_id = no_id then NONE else SOME command_id; val result = - if is_some (after_entry node last_exec) then no_result - else Lazy.map #1 exec; + if is_some (after_entry node last_exec) then no_exec + else exec; val node' = node |> fold reset_entry no_execs @@ -485,7 +486,7 @@ fun force_exec _ _ NONE = () | force_exec node command_id (SOME (_, exec)) = let - val (_, print) = Lazy.force exec; + val (_, print) = Exn.release (Command.memo_result exec); val _ = if #1 (get_perspective node) command_id then ignore (Lazy.future Future.default_params print)