Document.removed_versions on Scala side;
authorwenzelm
Sat Sep 03 21:15:35 2011 +0200 (2011-09-03)
changeset 446767de87f1ae965
parent 44675 f665a5d35a3d
child 44677 3fb27b19e058
Document.removed_versions on Scala side;
src/Pure/General/markup.ML
src/Pure/General/markup.scala
src/Pure/PIDE/document.scala
src/Pure/PIDE/isar_document.ML
src/Pure/PIDE/isar_document.scala
src/Pure/System/session.scala
     1.1 --- a/src/Pure/General/markup.ML	Sat Sep 03 19:47:31 2011 +0200
     1.2 +++ b/src/Pure/General/markup.ML	Sat Sep 03 21:15:35 2011 +0200
     1.3 @@ -116,6 +116,7 @@
     1.4    val badN: string val bad: T
     1.5    val functionN: string
     1.6    val assign_execs: Properties.T
     1.7 +  val removed_versions: Properties.T
     1.8    val invoke_scala: string -> string -> Properties.T
     1.9    val cancel_scala: string -> Properties.T
    1.10    val no_output: Output.output * Output.output
    1.11 @@ -367,6 +368,7 @@
    1.12  val functionN = "function"
    1.13  
    1.14  val assign_execs = [(functionN, "assign_execs")];
    1.15 +val removed_versions = [(functionN, "removed_versions")];
    1.16  
    1.17  fun invoke_scala name id = [(functionN, "invoke_scala"), (nameN, name), (idN, id)];
    1.18  fun cancel_scala id = [(functionN, "cancel_scala"), (idN, id)];
     2.1 --- a/src/Pure/General/markup.scala	Sat Sep 03 19:47:31 2011 +0200
     2.2 +++ b/src/Pure/General/markup.scala	Sat Sep 03 21:15:35 2011 +0200
     2.3 @@ -274,6 +274,7 @@
     2.4    val Function = new Properties.String(FUNCTION)
     2.5  
     2.6    val Assign_Execs: Properties.T = List((FUNCTION, "assign_execs"))
     2.7 +  val Removed_Versions: Properties.T = List((FUNCTION, "removed_versions"))
     2.8  
     2.9    val INVOKE_SCALA = "invoke_scala"
    2.10    object Invoke_Scala
     3.1 --- a/src/Pure/PIDE/document.scala	Sat Sep 03 19:47:31 2011 +0200
     3.2 +++ b/src/Pure/PIDE/document.scala	Sat Sep 03 21:15:35 2011 +0200
     3.3 @@ -264,7 +264,6 @@
     3.4      val commands: Map[Command_ID, Command.State] = Map(),  // static markup from define_command
     3.5      val execs: Map[Exec_ID, Command.State] = Map(),  // dynamic markup from execution
     3.6      val assignments: Map[Version_ID, State.Assignment] = Map(),
     3.7 -    val disposed: Set[ID] = Set(),  // FIXME unused!?
     3.8      val history: History = History.init)
     3.9    {
    3.10      private def fail[A]: A = throw new State.Fail(this)
    3.11 @@ -272,7 +271,6 @@
    3.12      def define_version(version: Version, assignment: State.Assignment): State =
    3.13      {
    3.14        val id = version.id
    3.15 -      if (versions.isDefinedAt(id) || disposed(id)) fail
    3.16        copy(versions = versions + (id -> version),
    3.17          assignments = assignments + (id -> assignment.unfinished))
    3.18      }
    3.19 @@ -280,7 +278,6 @@
    3.20      def define_command(command: Command): State =
    3.21      {
    3.22        val id = command.id
    3.23 -      if (commands.isDefinedAt(id) || disposed(id)) fail
    3.24        copy(commands = commands + (id -> command.empty_state))
    3.25      }
    3.26  
    3.27 @@ -389,6 +386,30 @@
    3.28        }
    3.29      }
    3.30  
    3.31 +    def removed_versions(removed: List[Version_ID]): State =
    3.32 +    {
    3.33 +      val versions1 = versions -- removed
    3.34 +      val assignments1 = assignments -- removed
    3.35 +      var commands1 = Map.empty[Command_ID, Command.State]
    3.36 +      var execs1 = Map.empty[Exec_ID, Command.State]
    3.37 +      for {
    3.38 +        (version_id, version) <- versions1.iterator
    3.39 +        val command_execs = assignments1(version_id).command_execs
    3.40 +        (_, node) <- version.nodes.iterator
    3.41 +        command <- node.commands.iterator
    3.42 +      } {
    3.43 +        val id = command.id
    3.44 +        if (!commands1.isDefinedAt(id) && commands.isDefinedAt(id))
    3.45 +          commands1 += (id -> commands(id))
    3.46 +        if (command_execs.isDefinedAt(id)) {
    3.47 +          val exec_id = command_execs(id)
    3.48 +          if (!execs1.isDefinedAt(exec_id) && execs.isDefinedAt(exec_id))
    3.49 +            execs1 += (exec_id -> execs(exec_id))
    3.50 +        }
    3.51 +      }
    3.52 +      copy(versions = versions1, commands = commands1, execs = execs1, assignments = assignments1)
    3.53 +    }
    3.54 +
    3.55      def command_state(version: Version, command: Command): Command.State =
    3.56      {
    3.57        require(is_assigned(version))
     4.1 --- a/src/Pure/PIDE/isar_document.ML	Sat Sep 03 19:47:31 2011 +0200
     4.2 +++ b/src/Pure/PIDE/isar_document.ML	Sat Sep 03 21:15:35 2011 +0200
     4.3 @@ -71,7 +71,9 @@
     4.4          val versions =
     4.5            YXML.parse_body versions_yxml |>
     4.6              let open XML.Decode in list int end;
     4.7 -      in Document.remove_versions versions state end));
     4.8 +        val state1 = Document.remove_versions versions state;
     4.9 +        val _ = Output.raw_message Markup.removed_versions versions_yxml;
    4.10 +      in state1 end));
    4.11  
    4.12  val _ =
    4.13    Isabelle_Process.add_command "Isar_Document.invoke_scala"
     5.1 --- a/src/Pure/PIDE/isar_document.scala	Sat Sep 03 19:47:31 2011 +0200
     5.2 +++ b/src/Pure/PIDE/isar_document.scala	Sat Sep 03 21:15:35 2011 +0200
     5.3 @@ -26,6 +26,20 @@
     5.4        }
     5.5    }
     5.6  
     5.7 +  object Removed
     5.8 +  {
     5.9 +    def unapply(text: String): Option[List[Document.Version_ID]] =
    5.10 +      try {
    5.11 +        import XML.Decode._
    5.12 +        Some(list(long)(YXML.parse_body(text)))
    5.13 +      }
    5.14 +      catch {
    5.15 +        case ERROR(_) => None
    5.16 +        case _: XML.XML_Atom => None
    5.17 +        case _: XML.XML_Body => None
    5.18 +      }
    5.19 +  }
    5.20 +
    5.21  
    5.22    /* toplevel transactions */
    5.23  
     6.1 --- a/src/Pure/System/session.scala	Sat Sep 03 19:47:31 2011 +0200
     6.2 +++ b/src/Pure/System/session.scala	Sat Sep 03 21:15:35 2011 +0200
     6.3 @@ -42,6 +42,8 @@
     6.4    val output_delay = Time.seconds(0.1)  // prover output (markup, common messages)
     6.5    val update_delay = Time.seconds(0.5)  // GUI layout updates
     6.6    val load_delay = Time.seconds(0.5)  // file load operations (new buffers etc.)
     6.7 +  val prune_delay = Time.seconds(60.0)  // prune history -- delete old versions
     6.8 +  val prune_size = 0  // size of retained history
     6.9  
    6.10  
    6.11    /* pervasive event buses */
    6.12 @@ -180,6 +182,8 @@
    6.13      val this_actor = self
    6.14      var prover: Option[Isabelle_Process with Isar_Document] = None
    6.15  
    6.16 +    var prune_next = System.currentTimeMillis() + prune_delay.ms
    6.17 +
    6.18  
    6.19      /* perspective */
    6.20  
    6.21 @@ -239,6 +243,16 @@
    6.22      //}}}
    6.23  
    6.24  
    6.25 +    /* removed versions */
    6.26 +
    6.27 +    def handle_removed(removed: List[Document.Version_ID])
    6.28 +    //{{{
    6.29 +    {
    6.30 +      global_state.change(_.removed_versions(removed))
    6.31 +    }
    6.32 +    //}}}
    6.33 +
    6.34 +
    6.35      /* resulting changes */
    6.36  
    6.37      def handle_change(change: Change_Node)
    6.38 @@ -295,6 +309,19 @@
    6.39                catch { case _: Document.State.Fail => bad_result(result) }
    6.40              case _ => bad_result(result)
    6.41            }
    6.42 +          // FIXME separate timeout event/message!?
    6.43 +          if (prover.isDefined && System.currentTimeMillis() > prune_next) {
    6.44 +            val old_versions = global_state.change_yield(_.prune_history(prune_size))
    6.45 +            if (!old_versions.isEmpty) prover.get.remove_versions(old_versions)
    6.46 +            prune_next = System.currentTimeMillis() + prune_delay.ms
    6.47 +          }
    6.48 +        case Markup.Removed_Versions if result.is_raw =>
    6.49 +          XML.content(result.body).mkString match {
    6.50 +            case Isar_Document.Removed(removed) =>
    6.51 +              try { handle_removed(removed) }
    6.52 +              catch { case _: Document.State.Fail => bad_result(result) }
    6.53 +            case _ => bad_result(result)
    6.54 +          }
    6.55          case Markup.Invoke_Scala(name, id) if result.is_raw =>
    6.56            Future.fork {
    6.57              val arg = XML.content(result.body).mkString