include Document.History in Document.State -- just one universal session state maintained by main actor;
authorwenzelm
Sat Aug 28 17:27:38 2010 +0200 (2010-08-28)
changeset 388414df7b76249a0
parent 38840 ec75dc58688b
child 38842 f762b33e0821
include Document.History in Document.State -- just one universal session state maintained by main actor;
Session.command_change_buffer: thread actor ensures asynchronous dispatch;
misc tuning;
src/Pure/PIDE/document.scala
src/Pure/System/session.scala
     1.1 --- a/src/Pure/PIDE/document.scala	Sat Aug 28 17:20:53 2010 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Sat Aug 28 17:27:38 2010 +0200
     1.3 @@ -116,7 +116,25 @@
     1.4    }
     1.5  
     1.6  
     1.7 -  /* history navigation and persistent snapshots */
     1.8 +  /* history navigation */
     1.9 +
    1.10 +  object History
    1.11 +  {
    1.12 +    val init = new History(List(Change.init))
    1.13 +  }
    1.14 +
    1.15 +  // FIXME pruning, purging of state
    1.16 +  class History(val undo_list: List[Change])
    1.17 +  {
    1.18 +    require(!undo_list.isEmpty)
    1.19 +
    1.20 +    def tip: Change = undo_list.head
    1.21 +    def +(change: Change): History = new History(change :: undo_list)
    1.22 +  }
    1.23 +
    1.24 +
    1.25 +
    1.26 +  /** global state -- document structure, execution process, editing history **/
    1.27  
    1.28    abstract class Snapshot
    1.29    {
    1.30 @@ -131,52 +149,6 @@
    1.31      def revert(range: Text.Range): Text.Range = range.map(revert(_))
    1.32    }
    1.33  
    1.34 -  object History
    1.35 -  {
    1.36 -    val init = new History(List(Change.init))
    1.37 -  }
    1.38 -
    1.39 -  // FIXME pruning, purging of state
    1.40 -  class History(undo_list: List[Change])
    1.41 -  {
    1.42 -    require(!undo_list.isEmpty)
    1.43 -
    1.44 -    def tip: Change = undo_list.head
    1.45 -    def +(ch: Change): History = new History(ch :: undo_list)
    1.46 -
    1.47 -    def snapshot(name: String, pending_edits: List[Text.Edit], state_snapshot: State): Snapshot =
    1.48 -    {
    1.49 -      val found_stable = undo_list.find(change =>
    1.50 -        change.is_finished && state_snapshot.is_assigned(change.current.join))
    1.51 -      require(found_stable.isDefined)
    1.52 -      val stable = found_stable.get
    1.53 -      val latest = undo_list.head
    1.54 -
    1.55 -      val edits =
    1.56 -        (pending_edits /: undo_list.takeWhile(_ != stable))((edits, change) =>
    1.57 -            (for ((a, eds) <- change.edits if a == name) yield eds).flatten ::: edits)
    1.58 -      lazy val reverse_edits = edits.reverse
    1.59 -
    1.60 -      new Snapshot
    1.61 -      {
    1.62 -        val version = stable.current.join
    1.63 -        val node = version.nodes(name)
    1.64 -        val is_outdated = !(pending_edits.isEmpty && latest == stable)
    1.65 -        def lookup_command(id: Command_ID): Option[Command] = state_snapshot.lookup_command(id)
    1.66 -        def state(command: Command): Command.State =
    1.67 -          try { state_snapshot.command_state(version, command) }
    1.68 -          catch { case _: State.Fail => command.empty_state }
    1.69 -
    1.70 -        def convert(offset: Text.Offset) = (offset /: edits)((i, edit) => edit.convert(i))
    1.71 -        def revert(offset: Text.Offset) = (offset /: reverse_edits)((i, edit) => edit.revert(i))
    1.72 -      }
    1.73 -    }
    1.74 -  }
    1.75 -
    1.76 -
    1.77 -
    1.78 -  /** global state -- document structure and execution process **/
    1.79 -
    1.80    object State
    1.81    {
    1.82      class Fail(state: State) extends Exception
    1.83 @@ -202,7 +174,8 @@
    1.84      val commands: Map[Command_ID, Command.State] = Map(),
    1.85      val execs: Map[Exec_ID, (Command.State, Set[Version])] = Map(),
    1.86      val assignments: Map[Version, State.Assignment] = Map(),
    1.87 -    val disposed: Set[ID] = Set())  // FIXME unused!?
    1.88 +    val disposed: Set[ID] = Set(),  // FIXME unused!?
    1.89 +    val history: History = History.init)
    1.90    {
    1.91      private def fail[A]: A = throw new State.Fail(this)
    1.92  
    1.93 @@ -265,11 +238,44 @@
    1.94          case None => false
    1.95        }
    1.96  
    1.97 -    def command_state(version: Version, command: Command): Command.State =
    1.98 +    def extend_history(previous: Future[Version],
    1.99 +        edits: List[Node_Text_Edit],
   1.100 +        result: Future[(List[Edit[Command]], Version)]): (Change, State) =
   1.101 +    {
   1.102 +      val change = new Change(previous, edits, result)
   1.103 +      (change, copy(history = history + change))
   1.104 +    }
   1.105 +
   1.106 +
   1.107 +    // persistent user-view
   1.108 +    def snapshot(name: String, pending_edits: List[Text.Edit]): Snapshot =
   1.109      {
   1.110 -      val assgn = the_assignment(version)
   1.111 -      require(assgn.is_finished)
   1.112 -      the_exec_state(assgn.join.getOrElse(command, fail))
   1.113 +      val found_stable = history.undo_list.find(change =>
   1.114 +        change.is_finished && is_assigned(change.current.join))
   1.115 +      require(found_stable.isDefined)
   1.116 +      val stable = found_stable.get
   1.117 +      val latest = history.undo_list.head
   1.118 +
   1.119 +      val edits =
   1.120 +        (pending_edits /: history.undo_list.takeWhile(_ != stable))((edits, change) =>
   1.121 +            (for ((a, eds) <- change.edits if a == name) yield eds).flatten ::: edits)
   1.122 +      lazy val reverse_edits = edits.reverse
   1.123 +
   1.124 +      new Snapshot
   1.125 +      {
   1.126 +        val version = stable.current.join
   1.127 +        val node = version.nodes(name)
   1.128 +        val is_outdated = !(pending_edits.isEmpty && latest == stable)
   1.129 +
   1.130 +        def lookup_command(id: Command_ID): Option[Command] = State.this.lookup_command(id)
   1.131 +
   1.132 +        def state(command: Command): Command.State =
   1.133 +          try { the_exec_state(the_assignment(version).join.getOrElse(command, fail)) }
   1.134 +          catch { case _: State.Fail => command.empty_state }
   1.135 +
   1.136 +        def convert(offset: Text.Offset) = (offset /: edits)((i, edit) => edit.convert(i))
   1.137 +        def revert(offset: Text.Offset) = (offset /: reverse_edits)((i, edit) => edit.revert(i))
   1.138 +      }
   1.139      }
   1.140    }
   1.141  }
     2.1 --- a/src/Pure/System/session.scala	Sat Aug 28 17:20:53 2010 +0200
     2.2 +++ b/src/Pure/System/session.scala	Sat Aug 28 17:27:38 2010 +0200
     2.3 @@ -57,17 +57,64 @@
     2.4  
     2.5  
     2.6  
     2.7 -  /** main actor **/
     2.8 +  /** buffered command changes (delay_first discipline) **/
     2.9 +
    2.10 +  private case object Stop
    2.11 +
    2.12 +  private val command_change_buffer = Simple_Thread.actor("command_change_buffer", daemon = true)
    2.13 +  //{{{
    2.14 +  {
    2.15 +    import scala.compat.Platform.currentTime
    2.16 +
    2.17 +    var changed: Set[Command] = Set()
    2.18 +    var flush_time: Option[Long] = None
    2.19 +
    2.20 +    def flush_timeout: Long =
    2.21 +      flush_time match {
    2.22 +        case None => 5000L
    2.23 +        case Some(time) => (time - currentTime) max 0
    2.24 +      }
    2.25 +
    2.26 +    def flush()
    2.27 +    {
    2.28 +      if (!changed.isEmpty) commands_changed.event(Session.Commands_Changed(changed))
    2.29 +      changed = Set()
    2.30 +      flush_time = None
    2.31 +    }
    2.32 +
    2.33 +    def invoke()
    2.34 +    {
    2.35 +      val now = currentTime
    2.36 +      flush_time match {
    2.37 +        case None => flush_time = Some(now + output_delay)
    2.38 +        case Some(time) => if (now >= time) flush()
    2.39 +      }
    2.40 +    }
    2.41 +
    2.42 +    var finished = false
    2.43 +    while (!finished) {
    2.44 +      receiveWithin(flush_timeout) {
    2.45 +        case command: Command => changed += command; invoke()
    2.46 +        case TIMEOUT => flush()
    2.47 +        case Stop => finished = true
    2.48 +        case bad => System.err.println("command_change_buffer: ignoring bad message " + bad)
    2.49 +      }
    2.50 +    }
    2.51 +  }
    2.52 +  //}}}
    2.53 +
    2.54 +
    2.55 +
    2.56 +  /** main protocol actor **/
    2.57  
    2.58    @volatile private var syntax = new Outer_Syntax(system.symbols)
    2.59    def current_syntax(): Outer_Syntax = syntax
    2.60  
    2.61 -  @volatile private var global_state = Document.State.init
    2.62 -  private def change_state(f: Document.State => Document.State) { global_state = f(global_state) }
    2.63 -  def current_state(): Document.State = global_state
    2.64 +  private val global_state = new Volatile(Document.State.init)
    2.65 +  def current_state(): Document.State = global_state.peek()
    2.66  
    2.67 +  private case class Edit_Version(edits: List[Document.Node_Text_Edit])
    2.68    private case class Started(timeout: Int, args: List[String])
    2.69 -  private case object Stop
    2.70  
    2.71    private val session_actor = Simple_Thread.actor("session_actor", daemon = true)
    2.72    {
    2.73 @@ -84,7 +131,7 @@
    2.74        val previous = change.previous.join
    2.75        val (node_edits, current) = change.result.join
    2.76  
    2.77 -      var former_assignment = current_state().the_assignment(previous).join
    2.78 +      var former_assignment = global_state.peek().the_assignment(previous).join
    2.79        for {
    2.80          (name, Some(cmd_edits)) <- node_edits
    2.81          (prev, None) <- cmd_edits
    2.82 @@ -103,8 +150,8 @@
    2.83                      c2 match {
    2.84                        case None => None
    2.85                        case Some(command) =>
    2.86 -                        if (current_state().lookup_command(command.id).isEmpty) {
    2.87 -                          change_state(_.define_command(command))
    2.88 +                        if (global_state.peek().lookup_command(command.id).isEmpty) {
    2.89 +                          global_state.change(_.define_command(command))
    2.90                            prover.define_command(command.id, system.symbols.encode(command.source))
    2.91                          }
    2.92                          Some(command.id)
    2.93 @@ -113,7 +160,7 @@
    2.94                }
    2.95              (name -> Some(ids))
    2.96          }
    2.97 -      change_state(_.define_version(current, former_assignment))
    2.98 +      global_state.change(_.define_version(current, former_assignment))
    2.99        prover.edit_version(previous.id, current.id, id_edits)
   2.100      }
   2.101      //}}}
   2.102 @@ -134,16 +181,15 @@
   2.103        result.properties match {
   2.104          case Position.Id(state_id) =>
   2.105            try {
   2.106 -            val (st, state) = global_state.accumulate(state_id, result.message)
   2.107 -            global_state = state
   2.108 -            indicate_command_change(st.command)
   2.109 +            val st = global_state.change_yield(_.accumulate(state_id, result.message))
   2.110 +            command_change_buffer ! st.command
   2.111            }
   2.112            catch { case _: Document.State.Fail => bad_result(result) }
   2.113          case _ =>
   2.114            if (result.is_status) {
   2.115              result.body match {
   2.116                case List(Isar_Document.Assign(id, edits)) =>
   2.117 -                try { change_state(_.assign(id, edits)) }
   2.118 +                try { global_state.change(_.assign(id, edits)) }
   2.119                  catch { case _: Document.State.Fail => bad_result(result) }
   2.120                case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
   2.121                case List(Keyword.Keyword_Decl(name)) => syntax += name
   2.122 @@ -202,6 +248,19 @@
   2.123      var finished = false
   2.124      while (!finished) {
   2.125        receive {
   2.126 +        case Edit_Version(edits) =>
   2.127 +          val previous = global_state.peek().history.tip.current
   2.128 +          val result = Future.fork { Thy_Syntax.text_edits(Session.this, previous.join, edits) }
   2.129 +          val change = global_state.change_yield(_.extend_history(previous, edits, result))
   2.130 +          val this_actor = self; result.map(_ => this_actor ! change)
   2.131 +          reply(())
   2.132 +
   2.133 +        case change: Document.Change if prover != null =>
   2.134 +          handle_change(change)
   2.135 +
   2.136 +        case result: Isabelle_Process.Result =>
   2.137 +          handle_result(result)
   2.138 +
   2.139          case Started(timeout, args) =>
   2.140            if (prover == null) {
   2.141              prover = new Isabelle_Process(system, self, args:_*) with Isar_Document
   2.142 @@ -219,12 +278,6 @@
   2.143              finished = true
   2.144            }
   2.145  
   2.146 -        case change: Document.Change if prover != null =>
   2.147 -          handle_change(change)
   2.148 -
   2.149 -        case result: Isabelle_Process.Result =>
   2.150 -          handle_result(result)
   2.151 -
   2.152          case TIMEOUT =>  // FIXME clarify!
   2.153  
   2.154          case bad if prover != null =>
   2.155 @@ -235,95 +288,15 @@
   2.156  
   2.157  
   2.158  
   2.159 -  /** buffered command changes (delay_first discipline) **/
   2.160 -
   2.161 -  private val command_change_buffer = actor
   2.162 -  //{{{
   2.163 -  {
   2.164 -    import scala.compat.Platform.currentTime
   2.165 -
   2.166 -    var changed: Set[Command] = Set()
   2.167 -    var flush_time: Option[Long] = None
   2.168 -
   2.169 -    def flush_timeout: Long =
   2.170 -      flush_time match {
   2.171 -        case None => 5000L
   2.172 -        case Some(time) => (time - currentTime) max 0
   2.173 -      }
   2.174 -
   2.175 -    def flush()
   2.176 -    {
   2.177 -      if (!changed.isEmpty) commands_changed.event(Session.Commands_Changed(changed))
   2.178 -      changed = Set()
   2.179 -      flush_time = None
   2.180 -    }
   2.181 -
   2.182 -    def invoke()
   2.183 -    {
   2.184 -      val now = currentTime
   2.185 -      flush_time match {
   2.186 -        case None => flush_time = Some(now + output_delay)
   2.187 -        case Some(time) => if (now >= time) flush()
   2.188 -      }
   2.189 -    }
   2.190 -
   2.191 -    loop {
   2.192 -      reactWithin(flush_timeout) {
   2.193 -        case command: Command => changed += command; invoke()
   2.194 -        case TIMEOUT => flush()
   2.195 -        case bad => System.err.println("command_change_buffer: ignoring bad message " + bad)
   2.196 -      }
   2.197 -    }
   2.198 -  }
   2.199 -  //}}}
   2.200 -
   2.201 -  def indicate_command_change(command: Command)
   2.202 -  {
   2.203 -    command_change_buffer ! command
   2.204 -  }
   2.205 -
   2.206 -
   2.207 -
   2.208 -  /** editor history **/
   2.209 -
   2.210 -  private case class Edit_Version(edits: List[Document.Node_Text_Edit])
   2.211 -
   2.212 -  @volatile private var history = Document.History.init
   2.213 -
   2.214 -  def snapshot(name: String, pending_edits: List[Text.Edit]): Document.Snapshot =
   2.215 -    history.snapshot(name, pending_edits, current_state())
   2.216 -
   2.217 -  private val editor_history = actor
   2.218 -  {
   2.219 -    loop {
   2.220 -      react {
   2.221 -        case Edit_Version(edits) =>
   2.222 -          val prev = history.tip.current
   2.223 -          val result =
   2.224 -            // FIXME potential denial-of-service concerning worker pool (!?!?)
   2.225 -            isabelle.Future.fork {
   2.226 -              val previous = prev.join
   2.227 -              val former_assignment = current_state().the_assignment(previous).join  // FIXME async!?
   2.228 -              Thy_Syntax.text_edits(Session.this, previous, edits)
   2.229 -            }
   2.230 -          val change = new Document.Change(prev, edits, result)
   2.231 -          history += change
   2.232 -          change.current.map(_ => session_actor ! change)
   2.233 -          reply(())
   2.234 -
   2.235 -        case bad => System.err.println("editor_model: ignoring bad message " + bad)
   2.236 -      }
   2.237 -    }
   2.238 -  }
   2.239 -
   2.240 -
   2.241 -
   2.242    /** main methods **/
   2.243  
   2.244    def started(timeout: Int, args: List[String]): Option[String] =
   2.245      (session_actor !? Started(timeout, args)).asInstanceOf[Option[String]]
   2.246  
   2.247 -  def stop() { session_actor ! Stop }
   2.248 +  def stop() { command_change_buffer ! Stop; session_actor ! Stop }
   2.249 +
   2.250 +  def edit_version(edits: List[Document.Node_Text_Edit]) { session_actor !? Edit_Version(edits) }
   2.251  
   2.252 -  def edit_version(edits: List[Document.Node_Text_Edit]) { editor_history !? Edit_Version(edits) }
   2.253 +  def snapshot(name: String, pending_edits: List[Text.Edit]): Document.Snapshot =
   2.254 +    global_state.peek().snapshot(name, pending_edits)
   2.255  }