diff -r fe4b245af74c -r e8552cba702d src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Fri Apr 06 23:34:38 2012 +0200 +++ b/src/Pure/PIDE/document.ML Sat Apr 07 16:41:59 2012 +0200 @@ -235,7 +235,7 @@ -(** document state -- content structure and execution process **) +(** main state -- document structure and execution process **) abstype state = State of {versions: version Inttab.table, (*version_id -> document content*) @@ -298,13 +298,19 @@ -(** execute **) +(** edit operations **) + +(* execute *) + +local fun finished_theory node = (case Exn.capture Command.memo_result (get_result node) of Exn.Res (st, _) => can (Toplevel.end_theory Position.none) st | _ => false); +in + fun execute version_id state = state |> map_state (fn (versions, commands, _) => let @@ -339,15 +345,27 @@ in (versions, commands, (version_id, group, running)) end); - +end; -(** edits **) - (* update *) local +fun stable_finished_theory node = + is_some (Exn.get_res (Exn.capture (fn () => + fst (Command.memo_result (get_result node)) + |> Toplevel.end_theory Position.none + |> Global_Theory.join_proofs) ())); + +fun stable_command exec = + (case Exn.capture Command.memo_result exec of + Exn.Exn exn => not (Exn.is_interrupt exn) + | Exn.Res (st, _) => + (case try Toplevel.theory_of st of + NONE => true + | SOME thy => is_some (Exn.get_res (Exn.capture Global_Theory.join_recent_proofs thy)))); + fun make_required nodes = let val all_visible = @@ -400,7 +418,7 @@ (case opt_exec of NONE => true | SOME (exec_id, exec) => - not (Command.memo_stable exec) orelse + not (stable_command exec) orelse (case lookup_entry node0 id of NONE => true | SOME (exec_id0, _) => exec_id <> exec_id0)); @@ -453,7 +471,7 @@ val updated = nodes |> Graph.schedule (fn deps => fn (name, node) => - if is_touched node orelse is_required name andalso not (finished_theory node) then + if is_touched node orelse is_required name andalso not (stable_finished_theory node) then let val node0 = node_of old_version name; fun init () = init_theory deps node;