# HG changeset patch
# User wenzelm
# Date 1315077335 -7200
# Node ID 7de87f1ae96533ca4edf1c45d00652642969cff7
# Parent  f665a5d35a3de59f27d140433a8f7b01e9c0e098
Document.removed_versions on Scala side;

diff -r f665a5d35a3d -r 7de87f1ae965 src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Sat Sep 03 19:47:31 2011 +0200
+++ b/src/Pure/General/markup.ML	Sat Sep 03 21:15:35 2011 +0200
@@ -116,6 +116,7 @@
   val badN: string val bad: T
   val functionN: string
   val assign_execs: Properties.T
+  val removed_versions: Properties.T
   val invoke_scala: string -> string -> Properties.T
   val cancel_scala: string -> Properties.T
   val no_output: Output.output * Output.output
@@ -367,6 +368,7 @@
 val functionN = "function"
 
 val assign_execs = [(functionN, "assign_execs")];
+val removed_versions = [(functionN, "removed_versions")];
 
 fun invoke_scala name id = [(functionN, "invoke_scala"), (nameN, name), (idN, id)];
 fun cancel_scala id = [(functionN, "cancel_scala"), (idN, id)];
diff -r f665a5d35a3d -r 7de87f1ae965 src/Pure/General/markup.scala
--- a/src/Pure/General/markup.scala	Sat Sep 03 19:47:31 2011 +0200
+++ b/src/Pure/General/markup.scala	Sat Sep 03 21:15:35 2011 +0200
@@ -274,6 +274,7 @@
   val Function = new Properties.String(FUNCTION)
 
   val Assign_Execs: Properties.T = List((FUNCTION, "assign_execs"))
+  val Removed_Versions: Properties.T = List((FUNCTION, "removed_versions"))
 
   val INVOKE_SCALA = "invoke_scala"
   object Invoke_Scala
diff -r f665a5d35a3d -r 7de87f1ae965 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Sat Sep 03 19:47:31 2011 +0200
+++ b/src/Pure/PIDE/document.scala	Sat Sep 03 21:15:35 2011 +0200
@@ -264,7 +264,6 @@
     val commands: Map[Command_ID, Command.State] = Map(),  // static markup from define_command
     val execs: Map[Exec_ID, Command.State] = Map(),  // dynamic markup from execution
     val assignments: Map[Version_ID, State.Assignment] = Map(),
-    val disposed: Set[ID] = Set(),  // FIXME unused!?
     val history: History = History.init)
   {
     private def fail[A]: A = throw new State.Fail(this)
@@ -272,7 +271,6 @@
     def define_version(version: Version, assignment: State.Assignment): State =
     {
       val id = version.id
-      if (versions.isDefinedAt(id) || disposed(id)) fail
       copy(versions = versions + (id -> version),
         assignments = assignments + (id -> assignment.unfinished))
     }
@@ -280,7 +278,6 @@
     def define_command(command: Command): State =
     {
       val id = command.id
-      if (commands.isDefinedAt(id) || disposed(id)) fail
       copy(commands = commands + (id -> command.empty_state))
     }
 
@@ -389,6 +386,30 @@
       }
     }
 
+    def removed_versions(removed: List[Version_ID]): State =
+    {
+      val versions1 = versions -- removed
+      val assignments1 = assignments -- removed
+      var commands1 = Map.empty[Command_ID, Command.State]
+      var execs1 = Map.empty[Exec_ID, Command.State]
+      for {
+        (version_id, version) <- versions1.iterator
+        val command_execs = assignments1(version_id).command_execs
+        (_, node) <- version.nodes.iterator
+        command <- node.commands.iterator
+      } {
+        val id = command.id
+        if (!commands1.isDefinedAt(id) && commands.isDefinedAt(id))
+          commands1 += (id -> commands(id))
+        if (command_execs.isDefinedAt(id)) {
+          val exec_id = command_execs(id)
+          if (!execs1.isDefinedAt(exec_id) && execs.isDefinedAt(exec_id))
+            execs1 += (exec_id -> execs(exec_id))
+        }
+      }
+      copy(versions = versions1, commands = commands1, execs = execs1, assignments = assignments1)
+    }
+
     def command_state(version: Version, command: Command): Command.State =
     {
       require(is_assigned(version))
diff -r f665a5d35a3d -r 7de87f1ae965 src/Pure/PIDE/isar_document.ML
--- a/src/Pure/PIDE/isar_document.ML	Sat Sep 03 19:47:31 2011 +0200
+++ b/src/Pure/PIDE/isar_document.ML	Sat Sep 03 21:15:35 2011 +0200
@@ -71,7 +71,9 @@
         val versions =
           YXML.parse_body versions_yxml |>
             let open XML.Decode in list int end;
-      in Document.remove_versions versions state end));
+        val state1 = Document.remove_versions versions state;
+        val _ = Output.raw_message Markup.removed_versions versions_yxml;
+      in state1 end));
 
 val _ =
   Isabelle_Process.add_command "Isar_Document.invoke_scala"
diff -r f665a5d35a3d -r 7de87f1ae965 src/Pure/PIDE/isar_document.scala
--- a/src/Pure/PIDE/isar_document.scala	Sat Sep 03 19:47:31 2011 +0200
+++ b/src/Pure/PIDE/isar_document.scala	Sat Sep 03 21:15:35 2011 +0200
@@ -26,6 +26,20 @@
       }
   }
 
+  object Removed
+  {
+    def unapply(text: String): Option[List[Document.Version_ID]] =
+      try {
+        import XML.Decode._
+        Some(list(long)(YXML.parse_body(text)))
+      }
+      catch {
+        case ERROR(_) => None
+        case _: XML.XML_Atom => None
+        case _: XML.XML_Body => None
+      }
+  }
+
 
   /* toplevel transactions */
 
diff -r f665a5d35a3d -r 7de87f1ae965 src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Sat Sep 03 19:47:31 2011 +0200
+++ b/src/Pure/System/session.scala	Sat Sep 03 21:15:35 2011 +0200
@@ -42,6 +42,8 @@
   val output_delay = Time.seconds(0.1)  // prover output (markup, common messages)
   val update_delay = Time.seconds(0.5)  // GUI layout updates
   val load_delay = Time.seconds(0.5)  // file load operations (new buffers etc.)
+  val prune_delay = Time.seconds(60.0)  // prune history -- delete old versions
+  val prune_size = 0  // size of retained history
 
 
   /* pervasive event buses */
@@ -180,6 +182,8 @@
     val this_actor = self
     var prover: Option[Isabelle_Process with Isar_Document] = None
 
+    var prune_next = System.currentTimeMillis() + prune_delay.ms
+
 
     /* perspective */
 
@@ -239,6 +243,16 @@
     //}}}
 
 
+    /* removed versions */
+
+    def handle_removed(removed: List[Document.Version_ID])
+    //{{{
+    {
+      global_state.change(_.removed_versions(removed))
+    }
+    //}}}
+
+
     /* resulting changes */
 
     def handle_change(change: Change_Node)
@@ -295,6 +309,19 @@
               catch { case _: Document.State.Fail => bad_result(result) }
             case _ => bad_result(result)
           }
+          // FIXME separate timeout event/message!?
+          if (prover.isDefined && System.currentTimeMillis() > prune_next) {
+            val old_versions = global_state.change_yield(_.prune_history(prune_size))
+            if (!old_versions.isEmpty) prover.get.remove_versions(old_versions)
+            prune_next = System.currentTimeMillis() + prune_delay.ms
+          }
+        case Markup.Removed_Versions if result.is_raw =>
+          XML.content(result.body).mkString match {
+            case Isar_Document.Removed(removed) =>
+              try { handle_removed(removed) }
+              catch { case _: Document.State.Fail => bad_result(result) }
+            case _ => bad_result(result)
+          }
         case Markup.Invoke_Scala(name, id) if result.is_raw =>
           Future.fork {
             val arg = XML.content(result.body).mkString