maintain stable state of node entries from last round -- bypass slightly different Thm.join_theory_proofs;
authorwenzelm
Sun Sep 02 14:02:05 2012 +0200 (2012-09-02)
changeset 49064bd6cc0b911a1
parent 49063 f93443defa6c
child 49065 8ead9e8b15fb
maintain stable state of node entries from last round -- bypass slightly different Thm.join_theory_proofs;
src/Pure/PIDE/document.ML
     1.1 --- a/src/Pure/PIDE/document.ML	Sat Sep 01 19:46:21 2012 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Sun Sep 02 14:02:05 2012 +0200
     1.3 @@ -69,7 +69,7 @@
     1.4  abstype node = Node of
     1.5   {header: node_header,  (*master directory, theory header, errors*)
     1.6    perspective: perspective,  (*visible commands, last*)
     1.7 -  entries: (exec_id * exec) option Entries.T,  (*command entries with excecutions*)
     1.8 +  entries: (exec_id * exec) option Entries.T * bool,  (*command entries with excecutions, stable*)
     1.9    result: exec option}  (*result of last execution*)
    1.10  and version = Version of node Graph.T  (*development graph wrt. static imports*)
    1.11  with
    1.12 @@ -86,8 +86,9 @@
    1.13  val no_header = ("", Thy_Header.make ("", Position.none) [] [] [], ["Bad theory header"]);
    1.14  val no_perspective = make_perspective [];
    1.15  
    1.16 -val empty_node = make_node (no_header, no_perspective, Entries.empty, NONE);
    1.17 -val clear_node = map_node (fn (header, _, _, _) => (header, no_perspective, Entries.empty, NONE));
    1.18 +val empty_node = make_node (no_header, no_perspective, (Entries.empty, true), NONE);
    1.19 +val clear_node =
    1.20 +  map_node (fn (header, _, _, _) => (header, no_perspective, (Entries.empty, true), NONE));
    1.21  
    1.22  
    1.23  (* basic components *)
    1.24 @@ -114,11 +115,17 @@
    1.25  val visible_node = is_some o visible_last
    1.26  
    1.27  fun map_entries f =
    1.28 -  map_node (fn (header, perspective, entries, result) => (header, perspective, f entries, result));
    1.29 -fun get_entries (Node {entries, ...}) = entries;
    1.30 +  map_node (fn (header, perspective, (entries, stable), result) =>
    1.31 +    (header, perspective, (f entries, stable), result));
    1.32 +fun get_entries (Node {entries = (entries, _), ...}) = entries;
    1.33 +
    1.34 +fun entries_stable stable =
    1.35 +  map_node (fn (header, perspective, (entries, _), result) =>
    1.36 +    (header, perspective, (entries, stable), result));
    1.37 +fun stable_entries (Node {entries = (_, stable), ...}) = stable;
    1.38  
    1.39  fun iterate_entries f = Entries.iterate NONE f o get_entries;
    1.40 -fun iterate_entries_after start f (Node {entries, ...}) =
    1.41 +fun iterate_entries_after start f (Node {entries = (entries, _), ...}) =
    1.42    (case Entries.get_after entries start of
    1.43      NONE => I
    1.44    | SOME id => Entries.iterate (SOME id) f entries);
    1.45 @@ -142,15 +149,15 @@
    1.46  
    1.47  type edit = string * node_edit;
    1.48  
    1.49 -fun after_entry (Node {entries, ...}) = Entries.get_after entries;
    1.50 +val after_entry = Entries.get_after o get_entries;
    1.51  
    1.52 -fun lookup_entry (Node {entries, ...}) id =
    1.53 -  (case Entries.lookup entries id of
    1.54 +fun lookup_entry node id =
    1.55 +  (case Entries.lookup (get_entries node) id of
    1.56      NONE => NONE
    1.57    | SOME (exec, _) => exec);
    1.58  
    1.59 -fun the_entry (Node {entries, ...}) id =
    1.60 -  (case Entries.lookup entries id of
    1.61 +fun the_entry node id =
    1.62 +  (case Entries.lookup (get_entries node) id of
    1.63      NONE => err_undef "command entry" id
    1.64    | SOME (exec, _) => exec);
    1.65  
    1.66 @@ -293,6 +300,20 @@
    1.67    in (versions', commands', execution) end);
    1.68  
    1.69  
    1.70 +(* consolidated states *)
    1.71 +
    1.72 +fun stable_command (exec_id, exec) =
    1.73 +  not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures exec_id))) andalso
    1.74 +    (case Exn.capture Command.memo_result exec of
    1.75 +      Exn.Exn exn => not (Exn.is_interrupt exn)
    1.76 +    | Exn.Res _ => true);
    1.77 +
    1.78 +fun finished_theory node =
    1.79 +  (case Exn.capture (Command.memo_result o the) (get_result node) of
    1.80 +    Exn.Res ((st, _), _) => can (Toplevel.end_theory Position.none) st
    1.81 +  | _ => false);
    1.82 +
    1.83 +
    1.84  
    1.85  (** document execution **)
    1.86  
    1.87 @@ -308,11 +329,6 @@
    1.88  
    1.89  fun start_execution state =
    1.90    let
    1.91 -    fun finished_theory node =
    1.92 -      (case Exn.capture (Command.memo_result o the) (get_result node) of
    1.93 -        Exn.Res ((st, _), _) => can (Toplevel.end_theory Position.none) st
    1.94 -      | _ => false);
    1.95 -
    1.96      fun run node command_id exec =
    1.97        let
    1.98          val (_, print) = Command.memo_eval exec;
    1.99 @@ -353,20 +369,6 @@
   1.100  
   1.101  local
   1.102  
   1.103 -fun stable_finished_theory node =
   1.104 -  is_some (Exn.get_res (Exn.capture (fn () =>
   1.105 -    fst (fst (Command.memo_result (the (get_result node))))
   1.106 -    |> Toplevel.end_theory Position.none
   1.107 -    |> Thm.join_theory_proofs) ()));
   1.108 -
   1.109 -fun stable_exec_id id =
   1.110 -  not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures id)));
   1.111 -
   1.112 -fun stable_exec exec =
   1.113 -  (case Exn.capture Command.memo_result exec of
   1.114 -    Exn.Exn exn => not (Exn.is_interrupt exn)
   1.115 -  | Exn.Res _ => true);
   1.116 -
   1.117  fun make_required nodes =
   1.118    let
   1.119      val all_visible =
   1.120 @@ -426,8 +428,7 @@
   1.121              | SOME (exec_id, exec) =>
   1.122                  (case lookup_entry node0 id of
   1.123                    NONE => false
   1.124 -                | SOME (exec_id0, _) =>
   1.125 -                    exec_id = exec_id0 andalso stable_exec_id exec_id andalso stable_exec exec));
   1.126 +                | SOME (exec_id0, _) => exec_id = exec_id0 andalso stable_command (exec_id, exec)));
   1.127          in SOME (same', (prev, flags')) end
   1.128        else NONE;
   1.129      val (same, (common, flags)) =
   1.130 @@ -493,7 +494,7 @@
   1.131                  val required = is_required name;
   1.132                in
   1.133                  if updated_imports orelse AList.defined (op =) edits name orelse
   1.134 -                  not (stable_finished_theory node)
   1.135 +                  not (stable_entries node) orelse not (finished_theory node)
   1.136                  then
   1.137                    let
   1.138                      val node0 = node_of old_version name;
   1.139 @@ -531,6 +532,7 @@
   1.140                      val node' = node
   1.141                        |> fold reset_entry no_execs
   1.142                        |> fold (fn (id, exec) => update_entry id (SOME exec)) new_execs
   1.143 +                      |> entries_stable (null new_execs)
   1.144                        |> set_result result;
   1.145                      val updated_node =
   1.146                        if null no_execs andalso null new_execs then NONE