# HG changeset patch
# User wenzelm
# Date 1315066089 -7200
# Node ID 2fa51ac191bcdb100c66d1dacebf17011b0739ae
# Parent  07dad1433cd73056ad4c5e762031b8ac14805994
Document.remove_versions on ML side;

diff -r 07dad1433cd7 -r 2fa51ac191bc src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Sat Sep 03 12:31:27 2011 +0200
+++ b/src/Pure/PIDE/document.ML	Sat Sep 03 18:08:09 2011 +0200
@@ -30,6 +30,7 @@
   val update: version_id -> version_id -> edit list -> state ->
     ((command_id * exec_id option) list * (string * command_id option) list) * state
   val execute: version_id -> state -> state
+  val remove_versions: version_id list -> state -> state
   val state: unit -> state
   val change_state: (state -> state) -> unit
 end;
@@ -239,7 +240,7 @@
   commands: (string * Toplevel.transition future) Inttab.table,  (*command_id -> name * transition*)
   execs: (command_id * (Toplevel.state * unit lazy) lazy) Inttab.table,
     (*exec_id -> command_id with eval/print process*)
-  execution: Future.group}  (*global execution process*)
+  execution: version_id * Future.group}  (*current execution process*)
 with
 
 fun make_state (versions, commands, execs, execution) =
@@ -248,11 +249,13 @@
 fun map_state f (State {versions, commands, execs, execution}) =
   make_state (f (versions, commands, execs, execution));
 
+val empty_commands =
+  Inttab.make [(no_id, (Toplevel.name_of Toplevel.empty, Future.value Toplevel.empty))];
+val empty_execs = Inttab.make [(no_id, (no_id, Lazy.value (Toplevel.toplevel, no_print)))];
+val empty_execution = (no_id, Future.new_group NONE);
+
 val init_state =
-  make_state (Inttab.make [(no_id, empty_version)],
-    Inttab.make [(no_id, (Toplevel.name_of Toplevel.empty, Future.value Toplevel.empty))],
-    Inttab.make [(no_id, (no_id, Lazy.value (Toplevel.toplevel, no_print)))],
-    Future.new_group NONE);
+  make_state (Inttab.make [(no_id, empty_version)], empty_commands, empty_execs, empty_execution);
 
 
 (* document versions *)
@@ -268,6 +271,9 @@
     NONE => err_undef "document version" id
   | SOME version => version);
 
+fun delete_version (id: version_id) versions = Inttab.delete id versions
+  handle Inttab.UNDEF _ => err_undef "document version" id;
+
 
 (* commands *)
 
@@ -309,7 +315,7 @@
 
 (* document execution *)
 
-fun cancel_execution (State {execution, ...}) = Future.cancel_group execution;
+fun cancel_execution (State {execution, ...}) = Future.cancel_group (#2 execution);
 
 end;
 
@@ -553,16 +559,39 @@
                 else ();
             in () end;
 
-      val execution = Future.new_group NONE;
+      val group = Future.new_group NONE;
       val _ =
         nodes_of version |> Graph.schedule
           (fn deps => fn (name, node) =>
             (singleton o Future.forks)
-              {name = "theory:" ^ name, group = SOME (Future.new_group (SOME execution)),
+              {name = "theory:" ^ name, group = SOME (Future.new_group (SOME group)),
                 deps = map (Future.task_of o #2) deps, pri = 1, interrupts = false}
               (iterate_entries (fn (_, exec) => fn () => SOME (force_exec node exec)) node));
 
-    in (versions, commands, execs, execution) end);
+    in (versions, commands, execs, (version_id, group)) end);
+
+
+(* remove versions *)
+
+fun remove_versions ids state = state |> map_state (fn (versions, _, _, execution) =>
+  let
+    val _ = member (op =) ids (#1 execution) andalso
+      error ("Attempt to remove execution version " ^ print_id (#1 execution));
+
+    val versions' = fold delete_version ids versions;
+    val (commands', execs') =
+      (versions', (empty_commands, empty_execs)) |->
+        Inttab.fold (fn (_, version) => nodes_of version |>
+          Graph.fold (fn (_, (node, _)) => node |>
+            iterate_entries (fn ((_, id), exec) => fn (commands, execs) =>
+              let
+                val commands' = Inttab.insert (K true) (id, the_command state id) commands;
+                val execs' =
+                  (case exec of
+                    NONE => execs
+                  | SOME exec_id => Inttab.insert (K true) (exec_id, the_exec state exec_id) execs);
+              in SOME (commands', execs') end)));
+  in (versions', commands', execs', execution) end);
 
 
 
diff -r 07dad1433cd7 -r 2fa51ac191bc src/Pure/PIDE/isar_document.ML
--- a/src/Pure/PIDE/isar_document.ML	Sat Sep 03 12:31:27 2011 +0200
+++ b/src/Pure/PIDE/isar_document.ML	Sat Sep 03 18:08:09 2011 +0200
@@ -65,6 +65,15 @@
       in state2 end));
 
 val _ =
+  Isabelle_Process.add_command "Isar_Document.remove_versions"
+    (fn [versions_yxml] => Document.change_state (fn state =>
+      let
+        val versions =
+          YXML.parse_body versions_yxml |>
+            let open XML.Decode in list int end;
+      in Document.remove_versions versions state end));
+
+val _ =
   Isabelle_Process.add_command "Isar_Document.invoke_scala"
     (fn [id, tag, res] => Invoke_Scala.fulfill_method id tag res);
 
diff -r 07dad1433cd7 -r 2fa51ac191bc src/Pure/PIDE/isar_document.scala
--- a/src/Pure/PIDE/isar_document.scala	Sat Sep 03 12:31:27 2011 +0200
+++ b/src/Pure/PIDE/isar_document.scala	Sat Sep 03 18:08:09 2011 +0200
@@ -188,6 +188,14 @@
     input("Isar_Document.update", Document.ID(old_id), Document.ID(new_id), edits_yxml)
   }
 
+  def remove_versions(versions: List[Document.Version])
+  {
+    val versions_yxml =
+      { import XML.Encode._
+        YXML.string_of_body(list(long)(versions.map(_.id))) }
+    input("Isar_Document.remove_versions", versions_yxml)
+  }
+
 
   /* method invocation service */