src/Pure/PIDE/document.ML
changeset 44476 e8a87398f35d
parent 44446 f9334afb6945
child 44478 4fdb1009a370
     1.1 --- a/src/Pure/PIDE/document.ML	Thu Aug 25 13:24:41 2011 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Thu Aug 25 16:44:06 2011 +0200
     1.3 @@ -28,7 +28,8 @@
     1.4    val join_commands: state -> unit
     1.5    val cancel_execution: state -> Future.task list
     1.6    val update_perspective: version_id -> version_id -> string -> command_id list -> state -> state
     1.7 -  val edit: version_id -> version_id -> edit list -> state -> (command_id * exec_id) list * state
     1.8 +  val edit: version_id -> version_id -> edit list -> state ->
     1.9 +    ((command_id * exec_id) list * (string * command_id option) list) * state
    1.10    val execute: version_id -> state -> state
    1.11    val state: unit -> state
    1.12    val change_state: (state -> state) -> unit
    1.13 @@ -58,7 +59,7 @@
    1.14  (** document structure **)
    1.15  
    1.16  type node_header = (string * string list * (string * bool) list) Exn.result;
    1.17 -type perspective = (command_id -> bool) * command_id list; (*visible commands, canonical order*)
    1.18 +type perspective = (command_id -> bool) * command_id option; (*visible commands, last*)
    1.19  structure Entries = Linear_Set(type key = command_id val ord = int_ord);
    1.20  
    1.21  abstype node = Node of
    1.22 @@ -66,58 +67,63 @@
    1.23    header: node_header,
    1.24    perspective: perspective,
    1.25    entries: exec_id option Entries.T,  (*command entries with excecutions*)
    1.26 +  last_exec: command_id option,  (*last command with exec state assignment*)
    1.27    result: Toplevel.state lazy}
    1.28  and version = Version of node Graph.T  (*development graph wrt. static imports*)
    1.29  with
    1.30  
    1.31 -fun make_node (touched, header, perspective, entries, result) =
    1.32 +fun make_node (touched, header, perspective, entries, last_exec, result) =
    1.33    Node {touched = touched, header = header, perspective = perspective,
    1.34 -    entries = entries, result = result};
    1.35 +    entries = entries, last_exec = last_exec, result = result};
    1.36  
    1.37 -fun map_node f (Node {touched, header, perspective, entries, result}) =
    1.38 -  make_node (f (touched, header, perspective, entries, result));
    1.39 +fun map_node f (Node {touched, header, perspective, entries, last_exec, result}) =
    1.40 +  make_node (f (touched, header, perspective, entries, last_exec, result));
    1.41  
    1.42 -fun make_perspective ids : perspective =
    1.43 -  (Inttab.defined (Inttab.make (map (rpair ()) ids)), ids);
    1.44 +fun make_perspective command_ids : perspective =
    1.45 +  (Inttab.defined (Inttab.make (map (rpair ()) command_ids)), try List.last command_ids);
    1.46  
    1.47 +val no_header = Exn.Exn (ERROR "Bad theory header");
    1.48  val no_perspective = make_perspective [];
    1.49  val no_print = Lazy.value ();
    1.50  val no_result = Lazy.value Toplevel.toplevel;
    1.51  
    1.52 -val empty_node =
    1.53 -  make_node (false, Exn.Exn (ERROR "Bad theory header"), no_perspective, Entries.empty, no_result);
    1.54 -
    1.55 -val clear_node =
    1.56 -  map_node (fn (_, header, _, _, _) => (false, header, no_perspective, Entries.empty, no_result));
    1.57 +val empty_node = make_node (false, no_header, no_perspective, Entries.empty, NONE, no_result);
    1.58 +val clear_node = map_node (fn (_, header, _, _, _, _) =>
    1.59 +  (false, header, no_perspective, Entries.empty, NONE, no_result));
    1.60  
    1.61  
    1.62  (* basic components *)
    1.63  
    1.64  fun is_touched (Node {touched, ...}) = touched;
    1.65  fun set_touched touched =
    1.66 -  map_node (fn (_, header, perspective, entries, result) =>
    1.67 -    (touched, header, perspective, entries, result));
    1.68 +  map_node (fn (_, header, perspective, entries, last_exec, result) =>
    1.69 +    (touched, header, perspective, entries, last_exec, result));
    1.70  
    1.71  fun get_header (Node {header, ...}) = header;
    1.72  fun set_header header =
    1.73 -  map_node (fn (touched, _, perspective, entries, result) =>
    1.74 -    (touched, header, perspective, entries, result));
    1.75 +  map_node (fn (touched, _, perspective, entries, last_exec, result) =>
    1.76 +    (touched, header, perspective, entries, last_exec, result));
    1.77  
    1.78  fun get_perspective (Node {perspective, ...}) = perspective;
    1.79  fun set_perspective ids =
    1.80 -  map_node (fn (touched, header, _, entries, result) =>
    1.81 -    (touched, header, make_perspective ids, entries, result));
    1.82 +  map_node (fn (touched, header, _, entries, last_exec, result) =>
    1.83 +    (touched, header, make_perspective ids, entries, last_exec, result));
    1.84  
    1.85  fun map_entries f =
    1.86 -  map_node (fn (touched, header, perspective, entries, result) =>
    1.87 -    (touched, header, perspective, f entries, result));
    1.88 +  map_node (fn (touched, header, perspective, entries, last_exec, result) =>
    1.89 +    (touched, header, perspective, f entries, last_exec, result));
    1.90  fun fold_entries start f (Node {entries, ...}) = Entries.fold start f entries;
    1.91  fun first_entry start P (Node {entries, ...}) = Entries.get_first start P entries;
    1.92  
    1.93 +fun get_last_exec (Node {last_exec, ...}) = last_exec;
    1.94 +fun set_last_exec last_exec =
    1.95 +  map_node (fn (touched, header, perspective, entries, _, result) =>
    1.96 +    (touched, header, perspective, entries, last_exec, result));
    1.97 +
    1.98  fun get_theory pos (Node {result, ...}) = Toplevel.end_theory pos (Lazy.force result);
    1.99  fun set_result result =
   1.100 -  map_node (fn (touched, header, perspective, entries, _) =>
   1.101 -    (touched, header, perspective, entries, result));
   1.102 +  map_node (fn (touched, header, perspective, entries, last_exec, _) =>
   1.103 +    (touched, header, perspective, entries, last_exec, result));
   1.104  
   1.105  fun get_node nodes name = Graph.get_node nodes name handle Graph.UNDEF _ => empty_node;
   1.106  fun default_node name = Graph.default_node (name, empty_node);
   1.107 @@ -137,9 +143,14 @@
   1.108  fun the_entry (Node {entries, ...}) id =
   1.109    (case Entries.lookup entries id of
   1.110      NONE => err_undef "command entry" id
   1.111 -  | SOME entry => entry);
   1.112 +  | SOME (exec, _) => exec);
   1.113  
   1.114 -fun update_entry (id, exec_id) =
   1.115 +fun is_last_entry (Node {entries, ...}) id =
   1.116 +  (case Entries.lookup entries id of
   1.117 +    SOME (_, SOME _) => false
   1.118 +  | _ => true);
   1.119 +
   1.120 +fun update_entry id exec_id =
   1.121    map_entries (Entries.update (id, SOME exec_id));
   1.122  
   1.123  fun reset_after id entries =
   1.124 @@ -382,17 +393,19 @@
   1.125                (#2 (Future.join (the (AList.lookup (op =) deps import))))));
   1.126    in Thy_Load.begin_theory dir thy_name imports files parents end;
   1.127  
   1.128 -fun new_exec state init command_id (assigns, execs, exec) =
   1.129 +fun new_exec state init command_id' (execs, exec) =
   1.130    let
   1.131 -    val command = the_command state command_id;
   1.132 +    val command' = the_command state command_id';
   1.133      val exec_id' = new_id ();
   1.134 -    val exec' = exec |> Lazy.map (fn (st, _) =>
   1.135 -      let val tr =
   1.136 -        Future.join command
   1.137 -        |> Toplevel.modify_init init
   1.138 -        |> Toplevel.put_id (print_id exec_id');
   1.139 -      in run_command tr st end);
   1.140 -  in ((command_id, exec_id') :: assigns, (exec_id', (command_id, exec')) :: execs, exec') end;
   1.141 +    val exec' =
   1.142 +      snd exec |> Lazy.map (fn (st, _) =>
   1.143 +        let val tr =
   1.144 +          Future.join command'
   1.145 +          |> Toplevel.modify_init init
   1.146 +          |> Toplevel.put_id (print_id exec_id');
   1.147 +        in run_command tr st end)
   1.148 +      |> pair command_id';
   1.149 +  in ((exec_id', exec') :: execs, exec') end;
   1.150  
   1.151  in
   1.152  
   1.153 @@ -402,13 +415,13 @@
   1.154      val _ = Time.now ();  (* FIXME odd workaround for polyml-5.4.0/x86_64 *)
   1.155      val new_version = fold edit_nodes edits old_version;
   1.156  
   1.157 -    val updates =
   1.158 +    val updated =
   1.159        nodes_of new_version |> Graph.schedule
   1.160          (fn deps => fn (name, node) =>
   1.161 -          if not (is_touched node) then Future.value (([], [], []), node)
   1.162 +          if not (is_touched node) then Future.value (([], []), node)
   1.163            else
   1.164              (case first_entry NONE (is_changed (node_of old_version name)) node of
   1.165 -              NONE => Future.value (([], [], []), set_touched false node)
   1.166 +              NONE => Future.value (([], []), set_touched false node)
   1.167              | SOME ((prev, id), _) =>
   1.168                  let
   1.169                    fun init () = init_theory deps name node;
   1.170 @@ -422,22 +435,32 @@
   1.171                            (case prev of
   1.172                              NONE => no_id
   1.173                            | SOME prev_id => the_default no_id (the_entry node prev_id));
   1.174 -                        val (assigns, execs, last_exec) =
   1.175 +                        val (execs, last_exec as (last_id, _)) =
   1.176                            fold_entries (SOME id) (new_exec state init o #2 o #1)
   1.177 -                            node ([], [], #2 (the_exec state prev_exec));
   1.178 -                        val node' = node
   1.179 -                          |> fold update_entry assigns
   1.180 -                          |> set_result (Lazy.map #1 last_exec)
   1.181 +                            node ([], the_exec state prev_exec);
   1.182 +                        val node' =
   1.183 +                          fold (fn (exec_id, (command_id, _)) => update_entry command_id exec_id)
   1.184 +                            execs node;
   1.185 +                        val result =
   1.186 +                          if is_last_entry node' last_id
   1.187 +                          then Lazy.map #1 (#2 last_exec)
   1.188 +                          else no_result;
   1.189 +                        val node'' = node'
   1.190 +                          |> set_last_exec (if last_id = no_id then NONE else SOME last_id)
   1.191 +                          |> set_result result
   1.192                            |> set_touched false;
   1.193 -                      in ((assigns, execs, [(name, node')]), node') end)
   1.194 +                      in ((execs, [(name, node'')]), node'') end)
   1.195                  end))
   1.196 -      |> Future.joins |> map #1;
   1.197 +      |> Future.joins |> map #1 |> rev;  (* FIXME why rev? *)
   1.198 +
   1.199 +    val updated_nodes = maps #2 updated;
   1.200 +    val assignment = map (fn (exec_id, (command_id, _)) => (command_id, exec_id)) (maps #1 updated);
   1.201 +    val last_execs = map (fn (name, node) => (name, get_last_exec node)) updated_nodes;
   1.202  
   1.203      val state' = state
   1.204 -      |> fold (fold define_exec o #2) updates
   1.205 -      |> define_version new_id (fold (fold put_node o #3) updates new_version);
   1.206 -
   1.207 -  in (maps #1 (rev updates), state') end;
   1.208 +      |> fold (fold define_exec o #1) updated
   1.209 +      |> define_version new_id (fold put_node updated_nodes new_version);
   1.210 +  in ((assignment, last_execs), state') end;
   1.211  
   1.212  end;
   1.213