src/Pure/PIDE/document.ML
changeset 47389 e8552cba702d
parent 47388 fe4b245af74c
child 47395 e6261a493f04
     1.1 --- a/src/Pure/PIDE/document.ML	Fri Apr 06 23:34:38 2012 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Sat Apr 07 16:41:59 2012 +0200
     1.3 @@ -235,7 +235,7 @@
     1.4  
     1.5  
     1.6  
     1.7 -(** document state -- content structure and execution process **)
     1.8 +(** main state -- document structure and execution process **)
     1.9  
    1.10  abstype state = State of
    1.11   {versions: version Inttab.table,  (*version_id -> document content*)
    1.12 @@ -298,13 +298,19 @@
    1.13  
    1.14  
    1.15  
    1.16 -(** execute **)
    1.17 +(** edit operations **)
    1.18 +
    1.19 +(* execute *)
    1.20 +
    1.21 +local
    1.22  
    1.23  fun finished_theory node =
    1.24    (case Exn.capture Command.memo_result (get_result node) of
    1.25      Exn.Res (st, _) => can (Toplevel.end_theory Position.none) st
    1.26    | _ => false);
    1.27  
    1.28 +in
    1.29 +
    1.30  fun execute version_id state =
    1.31    state |> map_state (fn (versions, commands, _) =>
    1.32      let
    1.33 @@ -339,15 +345,27 @@
    1.34  
    1.35      in (versions, commands, (version_id, group, running)) end);
    1.36  
    1.37 -
    1.38 +end;
    1.39  
    1.40  
    1.41 -(** edits **)
    1.42 -
    1.43  (* update *)
    1.44  
    1.45  local
    1.46  
    1.47 +fun stable_finished_theory node =
    1.48 +  is_some (Exn.get_res (Exn.capture (fn () =>
    1.49 +    fst (Command.memo_result (get_result node))
    1.50 +    |> Toplevel.end_theory Position.none
    1.51 +    |> Global_Theory.join_proofs) ()));
    1.52 +
    1.53 +fun stable_command exec =
    1.54 +  (case Exn.capture Command.memo_result exec of
    1.55 +    Exn.Exn exn => not (Exn.is_interrupt exn)
    1.56 +  | Exn.Res (st, _) =>
    1.57 +      (case try Toplevel.theory_of st of
    1.58 +        NONE => true
    1.59 +      | SOME thy => is_some (Exn.get_res (Exn.capture Global_Theory.join_recent_proofs thy))));
    1.60 +
    1.61  fun make_required nodes =
    1.62    let
    1.63      val all_visible =
    1.64 @@ -400,7 +418,7 @@
    1.65            (case opt_exec of
    1.66              NONE => true
    1.67            | SOME (exec_id, exec) =>
    1.68 -              not (Command.memo_stable exec) orelse
    1.69 +              not (stable_command exec) orelse
    1.70                (case lookup_entry node0 id of
    1.71                  NONE => true
    1.72                | SOME (exec_id0, _) => exec_id <> exec_id0));
    1.73 @@ -453,7 +471,7 @@
    1.74      val updated =
    1.75        nodes |> Graph.schedule
    1.76          (fn deps => fn (name, node) =>
    1.77 -          if is_touched node orelse is_required name andalso not (finished_theory node) then
    1.78 +          if is_touched node orelse is_required name andalso not (stable_finished_theory node) then
    1.79              let
    1.80                val node0 = node_of old_version name;
    1.81                fun init () = init_theory deps node;