src/Pure/PIDE/document.ML
changeset 44673 2fa51ac191bc
parent 44660 90bab3febb6c
child 44674 bad4f9158c80
     1.1 --- a/src/Pure/PIDE/document.ML	Sat Sep 03 12:31:27 2011 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Sat Sep 03 18:08:09 2011 +0200
     1.3 @@ -30,6 +30,7 @@
     1.4    val update: version_id -> version_id -> edit list -> state ->
     1.5      ((command_id * exec_id option) list * (string * command_id option) list) * state
     1.6    val execute: version_id -> state -> state
     1.7 +  val remove_versions: version_id list -> state -> state
     1.8    val state: unit -> state
     1.9    val change_state: (state -> state) -> unit
    1.10  end;
    1.11 @@ -239,7 +240,7 @@
    1.12    commands: (string * Toplevel.transition future) Inttab.table,  (*command_id -> name * transition*)
    1.13    execs: (command_id * (Toplevel.state * unit lazy) lazy) Inttab.table,
    1.14      (*exec_id -> command_id with eval/print process*)
    1.15 -  execution: Future.group}  (*global execution process*)
    1.16 +  execution: version_id * Future.group}  (*current execution process*)
    1.17  with
    1.18  
    1.19  fun make_state (versions, commands, execs, execution) =
    1.20 @@ -248,11 +249,13 @@
    1.21  fun map_state f (State {versions, commands, execs, execution}) =
    1.22    make_state (f (versions, commands, execs, execution));
    1.23  
    1.24 +val empty_commands =
    1.25 +  Inttab.make [(no_id, (Toplevel.name_of Toplevel.empty, Future.value Toplevel.empty))];
    1.26 +val empty_execs = Inttab.make [(no_id, (no_id, Lazy.value (Toplevel.toplevel, no_print)))];
    1.27 +val empty_execution = (no_id, Future.new_group NONE);
    1.28 +
    1.29  val init_state =
    1.30 -  make_state (Inttab.make [(no_id, empty_version)],
    1.31 -    Inttab.make [(no_id, (Toplevel.name_of Toplevel.empty, Future.value Toplevel.empty))],
    1.32 -    Inttab.make [(no_id, (no_id, Lazy.value (Toplevel.toplevel, no_print)))],
    1.33 -    Future.new_group NONE);
    1.34 +  make_state (Inttab.make [(no_id, empty_version)], empty_commands, empty_execs, empty_execution);
    1.35  
    1.36  
    1.37  (* document versions *)
    1.38 @@ -268,6 +271,9 @@
    1.39      NONE => err_undef "document version" id
    1.40    | SOME version => version);
    1.41  
    1.42 +fun delete_version (id: version_id) versions = Inttab.delete id versions
    1.43 +  handle Inttab.UNDEF _ => err_undef "document version" id;
    1.44 +
    1.45  
    1.46  (* commands *)
    1.47  
    1.48 @@ -309,7 +315,7 @@
    1.49  
    1.50  (* document execution *)
    1.51  
    1.52 -fun cancel_execution (State {execution, ...}) = Future.cancel_group execution;
    1.53 +fun cancel_execution (State {execution, ...}) = Future.cancel_group (#2 execution);
    1.54  
    1.55  end;
    1.56  
    1.57 @@ -553,16 +559,39 @@
    1.58                  else ();
    1.59              in () end;
    1.60  
    1.61 -      val execution = Future.new_group NONE;
    1.62 +      val group = Future.new_group NONE;
    1.63        val _ =
    1.64          nodes_of version |> Graph.schedule
    1.65            (fn deps => fn (name, node) =>
    1.66              (singleton o Future.forks)
    1.67 -              {name = "theory:" ^ name, group = SOME (Future.new_group (SOME execution)),
    1.68 +              {name = "theory:" ^ name, group = SOME (Future.new_group (SOME group)),
    1.69                  deps = map (Future.task_of o #2) deps, pri = 1, interrupts = false}
    1.70                (iterate_entries (fn (_, exec) => fn () => SOME (force_exec node exec)) node));
    1.71  
    1.72 -    in (versions, commands, execs, execution) end);
    1.73 +    in (versions, commands, execs, (version_id, group)) end);
    1.74 +
    1.75 +
    1.76 +(* remove versions *)
    1.77 +
    1.78 +fun remove_versions ids state = state |> map_state (fn (versions, _, _, execution) =>
    1.79 +  let
    1.80 +    val _ = member (op =) ids (#1 execution) andalso
    1.81 +      error ("Attempt to remove execution version " ^ print_id (#1 execution));
    1.82 +
    1.83 +    val versions' = fold delete_version ids versions;
    1.84 +    val (commands', execs') =
    1.85 +      (versions', (empty_commands, empty_execs)) |->
    1.86 +        Inttab.fold (fn (_, version) => nodes_of version |>
    1.87 +          Graph.fold (fn (_, (node, _)) => node |>
    1.88 +            iterate_entries (fn ((_, id), exec) => fn (commands, execs) =>
    1.89 +              let
    1.90 +                val commands' = Inttab.insert (K true) (id, the_command state id) commands;
    1.91 +                val execs' =
    1.92 +                  (case exec of
    1.93 +                    NONE => execs
    1.94 +                  | SOME exec_id => Inttab.insert (K true) (exec_id, the_exec state exec_id) execs);
    1.95 +              in SOME (commands', execs') end)));
    1.96 +  in (versions', commands', execs', execution) end);
    1.97  
    1.98  
    1.99