--- 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)];
--- 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
--- 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))
--- 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"
--- 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 */
--- 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