1.1 --- a/src/Pure/PIDE/command.ML	Tue Jul 09 16:32:51 2013 +0200
     1.2 +++ b/src/Pure/PIDE/command.ML	Tue Jul 09 17:58:38 2013 +0200
     1.3 @@ -13,7 +13,7 @@
     1.4    type print = {name: string, pri: int, exec_id: Document_ID.exec, print_process: print_process}
     1.5    type exec = eval * print list
     1.6    val no_exec: exec
     1.7 -  val exec_ids: exec -> Document_ID.exec list
     1.8 +  val exec_ids: exec option -> Document_ID.exec list
     1.9    val read: (unit -> theory) -> Token.T list -> Toplevel.transition
    1.10    val eval: (unit -> theory) -> Token.T list -> eval -> eval
    1.11    val print: string -> eval -> print list
    1.12 @@ -90,7 +90,8 @@
    1.13  type exec = eval * print list;
    1.14  val no_exec: exec = ({exec_id = Document_ID.none, eval_process = memo_value init_eval_state}, []);
    1.15  
    1.16 -fun exec_ids (({exec_id, ...}, prints): exec) = exec_id :: map #exec_id prints;
    1.17 +fun exec_ids (NONE: exec option) = []
    1.18 +  | exec_ids (SOME ({exec_id, ...}, prints)) = exec_id :: map #exec_id prints;
    1.19  
    1.20  
    1.21  (* read *)

     2.1 --- a/src/Pure/PIDE/document.ML	Tue Jul 09 16:32:51 2013 +0200
     2.2 +++ b/src/Pure/PIDE/document.ML	Tue Jul 09 17:58:38 2013 +0200
     2.3 @@ -108,6 +108,12 @@
     2.4  fun set_result result =
     2.5    map_node (fn (header, perspective, entries, _) => (header, perspective, entries, result));
     2.6  
     2.7 +fun changed_result node node' =
     2.8 +  (case (get_result node, get_result node') of
     2.9 +    (SOME eval, SOME eval') => #exec_id eval <> #exec_id eval'
    2.10 +  | (NONE, NONE) => false
    2.11 +  | _ => true);
    2.12 +
    2.13  fun finished_theory node =
    2.14    (case Exn.capture (Command.eval_result_state o the) (get_result node) of
    2.15      Exn.Res st => can (Toplevel.end_theory Position.none) st
    2.16 @@ -144,11 +150,9 @@
    2.17  fun the_default_entry node (SOME id) = (id, the_default Command.no_exec (the_entry node id))
    2.18    | the_default_entry _ NONE = (Document_ID.none, Command.no_exec);
    2.19  
    2.20 -fun update_entry id exec =
    2.21 -  map_entries (Entries.update (id, exec));
    2.22 -
    2.23 -fun reset_entry id node =
    2.24 -  if is_some (lookup_entry node id) then update_entry id NONE node else node;
    2.25 +fun assign_entry (command_id, exec) node =
    2.26 +  if is_none (Entries.lookup (get_entries node) command_id) then node
    2.27 +  else map_entries (Entries.update (command_id, exec)) node;
    2.28  
    2.29  fun reset_after id entries =
    2.30    (case Entries.get_after entries id of
    2.31 @@ -277,6 +281,9 @@
    2.32  
    2.33  end;
    2.34  
    2.35 +
    2.36 +(* remove_versions *)
    2.37 +
    2.38  fun remove_versions version_ids state = state |> map_state (fn (versions, _, execution) =>
    2.39    let
    2.40      val _ =
    2.41 @@ -327,6 +334,25 @@
    2.42  
    2.43  (** document update **)
    2.44  
    2.45 +(* exec state assignment *)
    2.46 +
    2.47 +type assign_update = Command.exec option Inttab.table;  (*command id -> exec*)
    2.48 +
    2.49 +val assign_update_empty: assign_update = Inttab.empty;
    2.50 +fun assign_update_null (tab: assign_update) = Inttab.is_empty tab;
    2.51 +fun assign_update_defined (tab: assign_update) command_id = Inttab.defined tab command_id;
    2.52 +fun assign_update_apply (tab: assign_update) node = Inttab.fold assign_entry tab node;
    2.53 +
    2.54 +fun assign_update_new upd (tab: assign_update) =
    2.55 +  Inttab.update_new upd tab
    2.56 +    handle Inttab.DUP dup => err_dup "exec state assignment" dup;
    2.57 +
    2.58 +fun assign_update_result (tab: assign_update) =
    2.59 +  Inttab.fold (fn (command_id, exec) => cons (command_id, Command.exec_ids exec)) tab [];
    2.60 +
    2.61 +
    2.62 +(* update *)
    2.63 +
    2.64  val timing = Unsynchronized.ref false;
    2.65  fun timeit msg e = cond_timeit (! timing) msg e;
    2.66  
    2.67 @@ -405,19 +431,22 @@
    2.68  
    2.69  fun illegal_init _ = error "Illegal theory header after end of theory";
    2.70  
    2.71 -fun new_exec state proper_init command_visible command_id' (execs, command_exec, init) =
    2.72 +fun new_exec state proper_init command_visible command_id' (assign_update, command_exec, init) =
    2.73    if not proper_init andalso is_none init then NONE
    2.74    else
    2.75      let
    2.76        val (_, (eval, _)) = command_exec;
    2.77        val (command_name, span) = the_command state command_id' ||> Lazy.force;
    2.78 -      val init' = if Keyword.is_theory_begin command_name then NONE else init;
    2.79 +
    2.80        val eval' = Command.eval (fn () => the_default illegal_init init span) span eval;
    2.81        val prints' = if command_visible then Command.print command_name eval' else [];
    2.82 -      val command_exec' = (command_id', (eval', prints'));
    2.83 -    in SOME (command_exec' :: execs, command_exec', init') end;
    2.84 +      val exec' = (eval', prints');
    2.85  
    2.86 -fun update_prints state node command_id =
    2.87 +      val assign_update' = assign_update_new (command_id', SOME exec') assign_update;
    2.88 +      val init' = if Keyword.is_theory_begin command_name then NONE else init;
    2.89 +    in SOME (assign_update', (command_id', (eval', prints')), init') end;
    2.90 +
    2.91 +fun update_prints state node command_id assign_update =
    2.92    (case the_entry node command_id of
    2.93      SOME (eval, prints) =>
    2.94        let
    2.95 @@ -429,10 +458,10 @@
    2.96                SOME print => if Command.stable_print print then print else new_print
    2.97              | NONE => new_print));
    2.98        in
    2.99 -        if eq_list (op = o pairself #exec_id) (prints, prints') then NONE
   2.100 -        else SOME (command_id, (eval, prints'))
   2.101 +        if eq_list (op = o pairself #exec_id) (prints, prints') then assign_update
   2.102 +        else assign_update_new (command_id, SOME (eval, prints')) assign_update
   2.103        end
   2.104 -  | NONE => NONE);
   2.105 +  | NONE => assign_update);
   2.106  
   2.107  in
   2.108  
   2.109 @@ -454,10 +483,10 @@
   2.110              (fn () =>
   2.111                let
   2.112                  val imports = map (apsnd Future.join) deps;
   2.113 -                val changed_imports = exists (#4 o #1 o #2) imports;
   2.114 +                val imports_changed = exists (#3 o #1 o #2) imports;
   2.115                  val node_required = is_required name;
   2.116                in
   2.117 -                if changed_imports orelse AList.defined (op =) edits name orelse
   2.118 +                if imports_changed orelse AList.defined (op =) edits name orelse
   2.119                    not (stable_entries node) orelse not (finished_theory node)
   2.120                  then
   2.121                    let
   2.122 @@ -472,59 +501,54 @@
   2.123                      val last_visible = visible_last node;
   2.124  
   2.125                      val (common, (still_visible, initial)) =
   2.126 -                      if changed_imports then (NONE, (true, true))
   2.127 +                      if imports_changed then (NONE, (true, true))
   2.128                        else last_common state last_visible node0 node;
   2.129 +
   2.130                      val common_command_exec = the_default_entry node common;
   2.131  
   2.132                      val (new_execs, (command_id', (eval', _)), _) =
   2.133 -                      ([], common_command_exec, if initial then SOME init else NONE) |>
   2.134 -                      (still_visible orelse node_required) ?
   2.135 +                      (assign_update_empty, common_command_exec, if initial then SOME init else NONE)
   2.136 +                      |> (still_visible orelse node_required) ?
   2.137                          iterate_entries_after common
   2.138                            (fn ((prev, id), _) => fn res =>
   2.139                              if not node_required andalso prev = last_visible then NONE
   2.140                              else new_exec state proper_init (visible_command id) id res) node;
   2.141  
   2.142                      val updated_execs =
   2.143 -                      (visible_commands, new_execs) |-> Inttab.fold (fn (id, ()) =>
   2.144 -                        if exists (fn (_, ({exec_id = id', ...}, _)) => id = id') new_execs then I
   2.145 -                        else append (the_list (update_prints state node id)));
   2.146 +                      (visible_commands, new_execs) |-> Inttab.fold (fn (command_id, ()) =>
   2.147 +                        not (assign_update_defined new_execs command_id) ?
   2.148 +                          update_prints state node command_id);
   2.149  
   2.150 -                    val no_execs =
   2.151 -                      iterate_entries_after common
   2.152 -                        (fn ((_, id0), exec0) => fn res =>
   2.153 +                    val assigned_execs =
   2.154 +                      (node0, updated_execs) |-> iterate_entries_after common
   2.155 +                        (fn ((_, command_id0), exec0) => fn res =>
   2.156                            if is_none exec0 then NONE
   2.157 -                          else if exists (fn (_, ({exec_id = id, ...}, _)) => id0 = id) updated_execs
   2.158 -                          then SOME res
   2.159 -                          else SOME (id0 :: res)) node0 [];
   2.160 +                          else if assign_update_defined updated_execs command_id0 then SOME res
   2.161 +                          else SOME (assign_update_new (command_id0, NONE) res));
   2.162  
   2.163                      val last_exec =
   2.164                        if command_id' = Document_ID.none then NONE else SOME command_id';
   2.165                      val result =
   2.166 -                      if is_some (after_entry node last_exec) then NONE
   2.167 +                      if is_none last_exec orelse is_some (after_entry node last_exec) then NONE
   2.168                        else SOME eval';
   2.169  
   2.170                      val node' = node
   2.171 -                      |> fold reset_entry no_execs
   2.172 -                      |> fold (fn (id, exec) => update_entry id (SOME exec)) updated_execs
   2.173 -                      |> entries_stable (null updated_execs)
   2.174 +                      |> assign_update_apply assigned_execs
   2.175 +                      |> entries_stable (assign_update_null updated_execs)
   2.176                        |> set_result result;
   2.177 -                    val updated_node =
   2.178 -                      if null no_execs andalso null updated_execs then NONE
   2.179 -                      else SOME (name, node');
   2.180 -                    val changed_result = not (null no_execs) orelse not (null new_execs);
   2.181 -                  in ((no_execs, updated_execs, updated_node, changed_result), node') end
   2.182 -                else (([], [], NONE, false), node)
   2.183 +                    val assigned_node =
   2.184 +                      if assign_update_null assigned_execs then NONE else SOME (name, node');
   2.185 +                    val result_changed = changed_result node0 node';
   2.186 +                  in
   2.187 +                    ((assign_update_result assigned_execs, assigned_node, result_changed), node')
   2.188 +                  end
   2.189 +                else (([], NONE, false), node)
   2.190                end))
   2.191        |> Future.joins |> map #1);
   2.192  
   2.193 -    val command_execs =
   2.194 -      map (rpair []) (maps #1 updated) @
   2.195 -      map (fn (command_id, exec) => (command_id, Command.exec_ids exec)) (maps #2 updated);
   2.196 -    val updated_nodes = map_filter #3 updated;
   2.197 -
   2.198      val state' = state
   2.199 -      |> define_version new_version_id (fold put_node updated_nodes new_version);
   2.200 -  in (command_execs, state') end;
   2.201 +      |> define_version new_version_id (fold put_node (map_filter #2 updated) new_version);
   2.202 +  in (maps #1 updated, state') end;
   2.203  
   2.204  end;
   2.205  

     3.1 --- a/src/Pure/PIDE/document.scala	Tue Jul 09 16:32:51 2013 +0200
     3.2 +++ b/src/Pure/PIDE/document.scala	Tue Jul 09 17:58:38 2013 +0200
     3.3 @@ -367,20 +367,22 @@
     3.4      {
     3.5        val version = the_version(id)
     3.6  
     3.7 +      def upd(exec_id: Document_ID.Exec, st: Command.State)
     3.8 +          : Option[(Document_ID.Exec, Command.State)] =
     3.9 +        if (execs.isDefinedAt(exec_id)) None else Some(exec_id -> st)
    3.10 +
    3.11        val (changed_commands, new_execs) =
    3.12          ((Nil: List[Command], execs) /: update) {
    3.13 -          case ((commands1, execs1), (cmd_id, exec)) =>
    3.14 -            val st1 = the_static_state(cmd_id)
    3.15 -            val command = st1.command
    3.16 -            val st0 = command.empty_state
    3.17 -
    3.18 +          case ((commands1, execs1), (command_id, exec)) =>
    3.19 +            val st = the_static_state(command_id)
    3.20 +            val command = st.command
    3.21              val commands2 = command :: commands1
    3.22              val execs2 =
    3.23                exec match {
    3.24                  case Nil => execs1
    3.25                  case eval_id :: print_ids =>
    3.26 -                  execs1 + (eval_id -> execs.getOrElse(eval_id, st1)) ++
    3.27 -                    print_ids.iterator.map(id => id -> execs.getOrElse(id, st0))
    3.28 +                  execs1 ++ upd(eval_id, st) ++
    3.29 +                    (for (id <- print_ids; up <- upd(id, command.empty_state)) yield up)
    3.30                }
    3.31              (commands2, execs2)
    3.32          }