discontinued global execs: store exec value directly within entries;
authorwenzelm
Sat Sep 03 19:39:16 2011 +0200 (2011-09-03 ago)
changeset 44674bad4f9158c80
parent 44673 2fa51ac191bc
child 44675 f665a5d35a3d
discontinued global execs: store exec value directly within entries;
simplified entries: no extra copy of command_id;
src/Pure/PIDE/document.ML
     1.1 --- a/src/Pure/PIDE/document.ML	Sat Sep 03 18:08:09 2011 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Sat Sep 03 19:39:16 2011 +0200
     1.3 @@ -62,11 +62,15 @@
     1.4  type perspective = (command_id -> bool) * command_id option; (*visible commands, last*)
     1.5  structure Entries = Linear_Set(type key = command_id val ord = int_ord);
     1.6  
     1.7 +type exec = exec_id * (Toplevel.state * unit lazy) lazy;  (*eval/print process*)
     1.8 +val no_print = Lazy.value ();
     1.9 +val no_exec = (no_id, Lazy.value (Toplevel.toplevel, no_print));
    1.10 +
    1.11  abstype node = Node of
    1.12   {touched: bool,
    1.13    header: node_header,
    1.14    perspective: perspective,
    1.15 -  entries: exec_id option Entries.T,  (*command entries with excecutions*)
    1.16 +  entries: exec option Entries.T,  (*command entries with excecutions*)
    1.17    last_exec: command_id option,  (*last command with exec state assignment*)
    1.18    result: Toplevel.state lazy}
    1.19  and version = Version of node Graph.T  (*development graph wrt. static imports*)
    1.20 @@ -84,7 +88,6 @@
    1.21  
    1.22  val no_header = Exn.Exn (ERROR "Bad theory header");
    1.23  val no_perspective = make_perspective [];
    1.24 -val no_print = Lazy.value ();
    1.25  val no_result = Lazy.value Toplevel.toplevel;
    1.26  
    1.27  val empty_node = make_node (false, no_header, no_perspective, Entries.empty, NONE, no_result);
    1.28 @@ -157,8 +160,8 @@
    1.29      NONE => err_undef "command entry" id
    1.30    | SOME (exec, _) => exec);
    1.31  
    1.32 -fun the_default_entry node (SOME id) = the_default no_id (the_entry node id)
    1.33 -  | the_default_entry _ NONE = no_id;
    1.34 +fun the_default_entry node (SOME id) = (id, (the_default no_exec (the_entry node id)))
    1.35 +  | the_default_entry _ NONE = (no_id, no_exec);
    1.36  
    1.37  fun update_entry id exec =
    1.38    map_entries (Entries.update (id, exec));
    1.39 @@ -238,33 +241,30 @@
    1.40  abstype state = State of
    1.41   {versions: version Inttab.table,  (*version_id -> document content*)
    1.42    commands: (string * Toplevel.transition future) Inttab.table,  (*command_id -> name * transition*)
    1.43 -  execs: (command_id * (Toplevel.state * unit lazy) lazy) Inttab.table,
    1.44 -    (*exec_id -> command_id with eval/print process*)
    1.45    execution: version_id * Future.group}  (*current execution process*)
    1.46  with
    1.47  
    1.48 -fun make_state (versions, commands, execs, execution) =
    1.49 -  State {versions = versions, commands = commands, execs = execs, execution = execution};
    1.50 +fun make_state (versions, commands, execution) =
    1.51 +  State {versions = versions, commands = commands, execution = execution};
    1.52  
    1.53 -fun map_state f (State {versions, commands, execs, execution}) =
    1.54 -  make_state (f (versions, commands, execs, execution));
    1.55 +fun map_state f (State {versions, commands, execution}) =
    1.56 +  make_state (f (versions, commands, execution));
    1.57  
    1.58 -val empty_commands =
    1.59 +val empty_commands =  (* FIXME no_id ??? *)
    1.60    Inttab.make [(no_id, (Toplevel.name_of Toplevel.empty, Future.value Toplevel.empty))];
    1.61 -val empty_execs = Inttab.make [(no_id, (no_id, Lazy.value (Toplevel.toplevel, no_print)))];
    1.62  val empty_execution = (no_id, Future.new_group NONE);
    1.63  
    1.64  val init_state =
    1.65 -  make_state (Inttab.make [(no_id, empty_version)], empty_commands, empty_execs, empty_execution);
    1.66 +  make_state (Inttab.make [(no_id, empty_version)], empty_commands, empty_execution);
    1.67  
    1.68  
    1.69  (* document versions *)
    1.70  
    1.71  fun define_version (id: version_id) version =
    1.72 -  map_state (fn (versions, commands, execs, execution) =>
    1.73 +  map_state (fn (versions, commands, execution) =>
    1.74      let val versions' = Inttab.update_new (id, version) versions
    1.75        handle Inttab.DUP dup => err_dup "document version" dup
    1.76 -    in (versions', commands, execs, execution) end);
    1.77 +    in (versions', commands, execution) end);
    1.78  
    1.79  fun the_version (State {versions, ...}) (id: version_id) =
    1.80    (case Inttab.lookup versions id of
    1.81 @@ -278,7 +278,7 @@
    1.82  (* commands *)
    1.83  
    1.84  fun define_command (id: command_id) name text =
    1.85 -  map_state (fn (versions, commands, execs, execution) =>
    1.86 +  map_state (fn (versions, commands, execution) =>
    1.87      let
    1.88        val id_string = print_id id;
    1.89        val future =
    1.90 @@ -291,7 +291,7 @@
    1.91        val commands' =
    1.92          Inttab.update_new (id, (name, future)) commands
    1.93            handle Inttab.DUP dup => err_dup "command" dup;
    1.94 -    in (versions, commands', execs, execution) end);
    1.95 +    in (versions, commands', execution) end);
    1.96  
    1.97  fun the_command (State {commands, ...}) (id: command_id) =
    1.98    (case Inttab.lookup commands id of
    1.99 @@ -299,20 +299,6 @@
   1.100    | SOME command => command);
   1.101  
   1.102  
   1.103 -(* command executions *)
   1.104 -
   1.105 -fun define_exec (exec_id, exec) =
   1.106 -  map_state (fn (versions, commands, execs, execution) =>
   1.107 -    let val execs' = Inttab.update_new (exec_id, exec) execs
   1.108 -      handle Inttab.DUP dup => err_dup "command execution" dup
   1.109 -    in (versions, commands, execs', execution) end);
   1.110 -
   1.111 -fun the_exec (State {execs, ...}) exec_id =
   1.112 -  (case Inttab.lookup execs exec_id of
   1.113 -    NONE => err_undef "command execution" exec_id
   1.114 -  | SOME exec => exec);
   1.115 -
   1.116 -
   1.117  (* document execution *)
   1.118  
   1.119  fun cancel_execution (State {execution, ...}) = Future.cancel_group (#2 execution);
   1.120 @@ -404,7 +390,8 @@
   1.121      fun get_common ((prev, id), exec) (found, (_, flags)) =
   1.122        if found then NONE
   1.123        else
   1.124 -        let val found' = is_none exec orelse exec <> lookup_entry node0 id
   1.125 +        let val found' =
   1.126 +          is_none exec orelse op <> (pairself (Option.map #1) (exec, lookup_entry node0 id));
   1.127          in SOME (found', (prev, update_flags prev flags)) end;
   1.128      val (found, (common, flags)) =
   1.129        iterate_entries get_common node (false, (NONE, (true, true)));
   1.130 @@ -417,7 +404,7 @@
   1.131  
   1.132  fun illegal_init () = error "Illegal theory header after end of theory";
   1.133  
   1.134 -fun new_exec state bad_init command_id' (execs, exec, init) =
   1.135 +fun new_exec state bad_init command_id' (execs, command_exec, init) =
   1.136    if bad_init andalso is_none init then NONE
   1.137    else
   1.138      let
   1.139 @@ -430,8 +417,9 @@
   1.140        val tr = tr0
   1.141          |> modify_init
   1.142          |> Toplevel.put_id (print_id exec_id');
   1.143 -      val exec' = (command_id', Lazy.map (fn (st, _) => run_command tr st) (snd exec));
   1.144 -    in SOME ((exec_id', exec') :: execs, exec', init') end;
   1.145 +      val exec' = snd (snd command_exec) |> Lazy.map (fn (st, _) => run_command tr st);
   1.146 +      val command_exec' = (command_id', (exec_id', exec'));
   1.147 +    in SOME (command_exec' :: execs, command_exec', init') end;
   1.148  
   1.149  fun make_required nodes =
   1.150    let
   1.151 @@ -495,10 +483,10 @@
   1.152                      val required = is_required name;
   1.153                      val last_visible = #2 (get_perspective node);
   1.154                      val (common, (visible, initial)) = last_common state last_visible node0 node;
   1.155 -                    val common_exec = the_exec state (the_default_entry node common);
   1.156 +                    val common_command_exec = the_default_entry node common;
   1.157  
   1.158 -                    val (execs, exec, _) =
   1.159 -                      ([], common_exec, if initial then SOME init else NONE) |>
   1.160 +                    val (execs, (command_id, (_, exec)), _) =
   1.161 +                      ([], common_command_exec, if initial then SOME init else NONE) |>
   1.162                        (visible orelse required) ?
   1.163                          iterate_entries_after common
   1.164                            (fn ((prev, id), _) => fn res =>
   1.165 @@ -512,14 +500,14 @@
   1.166                            else if exists (fn (_, (id, _)) => id0 = id) execs then SOME res
   1.167                            else SOME (id0 :: res)) node0 [];
   1.168  
   1.169 -                    val last_exec = if #1 exec = no_id then NONE else SOME (#1 exec);
   1.170 +                    val last_exec = if command_id = no_id then NONE else SOME command_id;
   1.171                      val result =
   1.172                        if is_some (after_entry node last_exec) then no_result
   1.173 -                      else Lazy.map #1 (#2 exec);
   1.174 +                      else Lazy.map #1 exec;
   1.175  
   1.176                      val node' = node
   1.177                        |> fold reset_entry no_execs
   1.178 -                      |> fold (fn (exec_id, (id, _)) => update_entry id (SOME exec_id)) execs
   1.179 +                      |> fold (fn (id, exec) => update_entry id (SOME exec)) execs
   1.180                        |> set_last_exec last_exec
   1.181                        |> set_result result
   1.182                        |> set_touched false;
   1.183 @@ -529,12 +517,11 @@
   1.184  
   1.185      val command_execs =
   1.186        map (rpair NONE) (maps #1 updated) @
   1.187 -      map (fn (exec_id, (command_id, _)) => (command_id, SOME exec_id)) (maps #2 updated);
   1.188 +      map (fn (command_id, (exec_id, _)) => (command_id, SOME exec_id)) (maps #2 updated);
   1.189      val updated_nodes = maps #3 updated;
   1.190      val last_execs = map (fn (name, node) => (name, get_last_exec node)) updated_nodes;
   1.191  
   1.192      val state' = state
   1.193 -      |> fold (fold define_exec o #2) updated
   1.194        |> define_version new_id (fold put_node updated_nodes new_version);
   1.195    in ((command_execs, last_execs), state') end;
   1.196  
   1.197 @@ -544,14 +531,13 @@
   1.198  (* execute *)
   1.199  
   1.200  fun execute version_id state =
   1.201 -  state |> map_state (fn (versions, commands, execs, _) =>
   1.202 +  state |> map_state (fn (versions, commands, _) =>
   1.203      let
   1.204        val version = the_version state version_id;
   1.205  
   1.206 -      fun force_exec _ NONE = ()
   1.207 -        | force_exec node (SOME exec_id) =
   1.208 +      fun force_exec _ _ NONE = ()
   1.209 +        | force_exec node command_id (SOME (_, exec)) =
   1.210              let
   1.211 -              val (command_id, exec) = the_exec state exec_id;
   1.212                val (_, print) = Lazy.force exec;
   1.213                val _ =
   1.214                  if #1 (get_perspective node) command_id
   1.215 @@ -566,32 +552,27 @@
   1.216              (singleton o Future.forks)
   1.217                {name = "theory:" ^ name, group = SOME (Future.new_group (SOME group)),
   1.218                  deps = map (Future.task_of o #2) deps, pri = 1, interrupts = false}
   1.219 -              (iterate_entries (fn (_, exec) => fn () => SOME (force_exec node exec)) node));
   1.220 +              (iterate_entries (fn ((_, id), exec) => fn () =>
   1.221 +                SOME (force_exec node id exec)) node));
   1.222  
   1.223 -    in (versions, commands, execs, (version_id, group)) end);
   1.224 +    in (versions, commands, (version_id, group)) end);
   1.225  
   1.226  
   1.227  (* remove versions *)
   1.228  
   1.229 -fun remove_versions ids state = state |> map_state (fn (versions, _, _, execution) =>
   1.230 +fun remove_versions ids state = state |> map_state (fn (versions, _, execution) =>
   1.231    let
   1.232      val _ = member (op =) ids (#1 execution) andalso
   1.233        error ("Attempt to remove execution version " ^ print_id (#1 execution));
   1.234  
   1.235      val versions' = fold delete_version ids versions;
   1.236 -    val (commands', execs') =
   1.237 -      (versions', (empty_commands, empty_execs)) |->
   1.238 +    val commands' =
   1.239 +      (versions', empty_commands) |->
   1.240          Inttab.fold (fn (_, version) => nodes_of version |>
   1.241            Graph.fold (fn (_, (node, _)) => node |>
   1.242 -            iterate_entries (fn ((_, id), exec) => fn (commands, execs) =>
   1.243 -              let
   1.244 -                val commands' = Inttab.insert (K true) (id, the_command state id) commands;
   1.245 -                val execs' =
   1.246 -                  (case exec of
   1.247 -                    NONE => execs
   1.248 -                  | SOME exec_id => Inttab.insert (K true) (exec_id, the_exec state exec_id) execs);
   1.249 -              in SOME (commands', execs') end)));
   1.250 -  in (versions', commands', execs', execution) end);
   1.251 +            iterate_entries (fn ((_, id), _) =>
   1.252 +              SOME o Inttab.insert (K true) (id, the_command state id))));
   1.253 +  in (versions', commands', execution) end);
   1.254  
   1.255  
   1.256