src/Pure/PIDE/document.ML
changeset 47345 193251980a73
parent 47344 ca5eb90cc84a
child 47346 cd3ab7625519
     1.1 --- a/src/Pure/PIDE/document.ML	Thu Apr 05 14:34:54 2012 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Thu Apr 05 22:33:52 2012 +0200
     1.3 @@ -27,10 +27,10 @@
     1.4    val define_command: command_id -> string -> string -> state -> state
     1.5    val discontinue_execution: state -> unit
     1.6    val cancel_execution: state -> Future.task list
     1.7 +  val execute: version_id -> state -> state
     1.8    val update_perspective: version_id -> version_id -> string -> command_id list -> state -> state
     1.9    val update: version_id -> version_id -> edit list -> state ->
    1.10      ((command_id * exec_id option) list * (string * command_id option) list) * state
    1.11 -  val execute: version_id -> state -> state
    1.12    val remove_versions: version_id list -> state -> state
    1.13    val state: unit -> state
    1.14    val change_state: (state -> state) -> unit
    1.15 @@ -111,6 +111,10 @@
    1.16    map_node (fn (touched, header, _, entries, last_exec, result) =>
    1.17      (touched, header, make_perspective ids, entries, last_exec, result));
    1.18  
    1.19 +val visible_command = #1 o get_perspective;
    1.20 +val visible_last = #2 o get_perspective;
    1.21 +val visible_node = is_some o visible_last
    1.22 +
    1.23  fun map_entries f =
    1.24    map_node (fn (touched, header, perspective, entries, last_exec, result) =>
    1.25      (touched, header, perspective, f entries, last_exec, result));
    1.26 @@ -293,7 +297,7 @@
    1.27  
    1.28  (* document execution *)
    1.29  
    1.30 -fun discontinue_execution  (State {execution = (_, _, running), ...}) = running := false;
    1.31 +fun discontinue_execution (State {execution = (_, _, running), ...}) = running := false;
    1.32  
    1.33  fun cancel_execution (State {execution = (_, group, _), ...}) = Future.cancel_group group;
    1.34  
    1.35 @@ -301,6 +305,49 @@
    1.36  
    1.37  
    1.38  
    1.39 +(** execute **)
    1.40 +
    1.41 +fun finished_theory node =
    1.42 +  (case Exn.capture Command.memo_result (get_result node) of
    1.43 +    Exn.Res (st, _) => can (Toplevel.end_theory Position.none) st
    1.44 +  | _ => false);
    1.45 +
    1.46 +fun execute version_id state =
    1.47 +  state |> map_state (fn (versions, commands, _) =>
    1.48 +    let
    1.49 +      val version = the_version state version_id;
    1.50 +
    1.51 +      val group = Future.new_group NONE;
    1.52 +      val running = Unsynchronized.ref true;
    1.53 +
    1.54 +      fun run _ _ NONE = ()
    1.55 +        | run node command_id (SOME (_, exec)) =
    1.56 +            let
    1.57 +              val (_, print) = Command.memo_eval exec;
    1.58 +              val _ =
    1.59 +                if visible_command node command_id
    1.60 +                then ignore (Lazy.future Future.default_params print)
    1.61 +                else ();
    1.62 +            in () end;
    1.63 +
    1.64 +      val _ =
    1.65 +        nodes_of version |> Graph.schedule
    1.66 +          (fn deps => fn (name, node) =>
    1.67 +            if not (visible_node node) andalso finished_theory node then
    1.68 +              Future.value ()
    1.69 +            else
    1.70 +              (singleton o Future.forks)
    1.71 +                {name = "theory:" ^ name, group = SOME (Future.new_group (SOME group)),
    1.72 +                  deps = map (Future.task_of o #2) deps, pri = 1, interrupts = false}
    1.73 +                (fn () =>
    1.74 +                  iterate_entries (fn ((_, id), exec) => fn () =>
    1.75 +                    if ! running then SOME (run node id exec) else NONE) node ()));
    1.76 +
    1.77 +    in (versions, commands, (version_id, group, running)) end);
    1.78 +
    1.79 +
    1.80 +
    1.81 +
    1.82  (** update **)
    1.83  
    1.84  (* perspective *)
    1.85 @@ -320,11 +367,14 @@
    1.86  fun make_required nodes =
    1.87    let
    1.88      val all_visible =
    1.89 -      Graph.fold (fn (a, (node, _)) => is_some (#2 (get_perspective node)) ? cons a) nodes []
    1.90 -      |> Graph.all_preds nodes;
    1.91 +      Graph.fold (fn (a, (node, _)) => visible_node node ? cons a) nodes []
    1.92 +      |> Graph.all_preds nodes
    1.93 +      |> map (rpair ()) |> Symtab.make;
    1.94 +
    1.95      val required =
    1.96 -      fold (fn a => exists (fn b => Graph.is_edge nodes (a, b)) all_visible ? Symtab.update (a, ()))
    1.97 -        all_visible Symtab.empty;
    1.98 +      Symtab.fold (fn (a, ()) =>
    1.99 +        exists (Symtab.defined all_visible) (Graph.immediate_succs nodes a) ?
   1.100 +          Symtab.update (a, ())) all_visible Symtab.empty;
   1.101    in Symtab.defined required end;
   1.102  
   1.103  fun init_theory deps node =
   1.104 @@ -419,7 +469,7 @@
   1.105      val updated =
   1.106        nodes |> Graph.schedule
   1.107          (fn deps => fn (name, node) =>
   1.108 -          if is_touched node orelse is_required name then
   1.109 +          if is_touched node orelse is_required name andalso not (finished_theory node) then
   1.110              let
   1.111                val node0 = node_of old_version name;
   1.112                fun init () = init_theory deps node;
   1.113 @@ -432,7 +482,7 @@
   1.114                  (fn () =>
   1.115                    let
   1.116                      val required = is_required name;
   1.117 -                    val last_visible = #2 (get_perspective node);
   1.118 +                    val last_visible = visible_last node;
   1.119                      val (common, (visible, initial)) = last_common state last_visible node0 node;
   1.120                      val common_command_exec = the_default_entry node common;
   1.121  
   1.122 @@ -480,39 +530,6 @@
   1.123  end;
   1.124  
   1.125  
   1.126 -(* execute *)
   1.127 -
   1.128 -fun execute version_id state =
   1.129 -  state |> map_state (fn (versions, commands, _) =>
   1.130 -    let
   1.131 -      val version = the_version state version_id;
   1.132 -
   1.133 -      val group = Future.new_group NONE;
   1.134 -      val running = Unsynchronized.ref true;
   1.135 -
   1.136 -      fun run _ _ NONE = ()
   1.137 -        | run node command_id (SOME (_, exec)) =
   1.138 -            let
   1.139 -              val (_, print) = Command.memo_eval exec;
   1.140 -              val _ =
   1.141 -                if #1 (get_perspective node) command_id
   1.142 -                then ignore (Lazy.future Future.default_params print)
   1.143 -                else ();
   1.144 -            in () end;
   1.145 -
   1.146 -      val _ =
   1.147 -        nodes_of version |> Graph.schedule
   1.148 -          (fn deps => fn (name, node) =>
   1.149 -            (singleton o Future.forks)
   1.150 -              {name = "theory:" ^ name, group = SOME (Future.new_group (SOME group)),
   1.151 -                deps = map (Future.task_of o #2) deps, pri = 1, interrupts = false}
   1.152 -              (fn () =>
   1.153 -                iterate_entries (fn ((_, id), exec) => fn () =>
   1.154 -                  if ! running then SOME (run node id exec) else NONE) node ()));
   1.155 -
   1.156 -    in (versions, commands, (version_id, group, running)) end);
   1.157 -
   1.158 -
   1.159  (* remove versions *)
   1.160  
   1.161  fun remove_versions ids state = state |> map_state (fn (versions, _, execution) =>