explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions;
authorwenzelm
Sat Apr 07 16:41:59 2012 +0200 (2012-04-07)
changeset 47389e8552cba702d
parent 47388 fe4b245af74c
child 47390 580c37559354
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions;
tuned;
src/Pure/PIDE/command.ML
src/Pure/PIDE/document.ML
     1.1 --- a/src/Pure/PIDE/command.ML	Fri Apr 06 23:34:38 2012 +0200
     1.2 +++ b/src/Pure/PIDE/command.ML	Sat Apr 07 16:41:59 2012 +0200
     1.3 @@ -12,7 +12,6 @@
     1.4    val memo_value: 'a -> 'a memo
     1.5    val memo_eval: 'a memo -> 'a
     1.6    val memo_result: 'a memo -> 'a
     1.7 -  val memo_stable: 'a memo -> bool
     1.8    val run_command: Toplevel.transition -> Toplevel.state -> Toplevel.state * unit lazy
     1.9  end;
    1.10  
    1.11 @@ -58,11 +57,6 @@
    1.12      Result res => Exn.release res
    1.13    | _ => raise Fail "Unfinished memo result");
    1.14  
    1.15 -fun memo_stable (Memo v) =
    1.16 -  (case Synchronized.value v of
    1.17 -    Result (Exn.Exn exn) => not (Exn.is_interrupt exn)
    1.18 -  | _ => true);
    1.19 -
    1.20  end;
    1.21  
    1.22  
     2.1 --- a/src/Pure/PIDE/document.ML	Fri Apr 06 23:34:38 2012 +0200
     2.2 +++ b/src/Pure/PIDE/document.ML	Sat Apr 07 16:41:59 2012 +0200
     2.3 @@ -235,7 +235,7 @@
     2.4  
     2.5  
     2.6  
     2.7 -(** document state -- content structure and execution process **)
     2.8 +(** main state -- document structure and execution process **)
     2.9  
    2.10  abstype state = State of
    2.11   {versions: version Inttab.table,  (*version_id -> document content*)
    2.12 @@ -298,13 +298,19 @@
    2.13  
    2.14  
    2.15  
    2.16 -(** execute **)
    2.17 +(** edit operations **)
    2.18 +
    2.19 +(* execute *)
    2.20 +
    2.21 +local
    2.22  
    2.23  fun finished_theory node =
    2.24    (case Exn.capture Command.memo_result (get_result node) of
    2.25      Exn.Res (st, _) => can (Toplevel.end_theory Position.none) st
    2.26    | _ => false);
    2.27  
    2.28 +in
    2.29 +
    2.30  fun execute version_id state =
    2.31    state |> map_state (fn (versions, commands, _) =>
    2.32      let
    2.33 @@ -339,15 +345,27 @@
    2.34  
    2.35      in (versions, commands, (version_id, group, running)) end);
    2.36  
    2.37 -
    2.38 +end;
    2.39  
    2.40  
    2.41 -(** edits **)
    2.42 -
    2.43  (* update *)
    2.44  
    2.45  local
    2.46  
    2.47 +fun stable_finished_theory node =
    2.48 +  is_some (Exn.get_res (Exn.capture (fn () =>
    2.49 +    fst (Command.memo_result (get_result node))
    2.50 +    |> Toplevel.end_theory Position.none
    2.51 +    |> Global_Theory.join_proofs) ()));
    2.52 +
    2.53 +fun stable_command exec =
    2.54 +  (case Exn.capture Command.memo_result exec of
    2.55 +    Exn.Exn exn => not (Exn.is_interrupt exn)
    2.56 +  | Exn.Res (st, _) =>
    2.57 +      (case try Toplevel.theory_of st of
    2.58 +        NONE => true
    2.59 +      | SOME thy => is_some (Exn.get_res (Exn.capture Global_Theory.join_recent_proofs thy))));
    2.60 +
    2.61  fun make_required nodes =
    2.62    let
    2.63      val all_visible =
    2.64 @@ -400,7 +418,7 @@
    2.65            (case opt_exec of
    2.66              NONE => true
    2.67            | SOME (exec_id, exec) =>
    2.68 -              not (Command.memo_stable exec) orelse
    2.69 +              not (stable_command exec) orelse
    2.70                (case lookup_entry node0 id of
    2.71                  NONE => true
    2.72                | SOME (exec_id0, _) => exec_id <> exec_id0));
    2.73 @@ -453,7 +471,7 @@
    2.74      val updated =
    2.75        nodes |> Graph.schedule
    2.76          (fn deps => fn (name, node) =>
    2.77 -          if is_touched node orelse is_required name andalso not (finished_theory node) then
    2.78 +          if is_touched node orelse is_required name andalso not (stable_finished_theory node) then
    2.79              let
    2.80                val node0 = node_of old_version name;
    2.81                fun init () = init_theory deps node;