# HG changeset patch # User wenzelm # Date 1281898993 -7200 # Node ID 940a404e45e274352040a7e0dbc68849711ee3ed # Parent a9cff3f2e47923fc9195e273df73797264ab1837 moved History/Snapshot to document.scala; diff -r a9cff3f2e479 -r 940a404e45e2 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Sun Aug 15 20:27:29 2010 +0200 +++ b/src/Pure/PIDE/document.scala Sun Aug 15 21:03:13 2010 +0200 @@ -30,12 +30,21 @@ - /** named document nodes **/ + /** document structure **/ + + /* named nodes -- development graph */ + + type Node_Text_Edit = (String, List[Text_Edit]) // FIXME None: remove + + type Edit[C] = + (String, // node name + Option[List[(Option[C], Option[C])]]) // None: remove, Some: insert/remove commands object Node { val empty: Node = new Node(Linear_Set()) + // FIXME not scalable def command_starts(commands: Iterator[Command], offset: Int = 0): Iterator[(Command, Int)] = { var i = offset @@ -49,8 +58,6 @@ class Node(val commands: Linear_Set[Command]) { - /* command ranges */ - def command_starts: Iterator[(Command, Int)] = Node.command_starts(commands.iterator) @@ -78,7 +85,10 @@ } - /* document versions */ + + /** versioning **/ + + /* particular document versions */ object Version { @@ -88,25 +98,7 @@ class Version(val id: Version_ID, val nodes: Map[String, Node]) - - /** changes of plain text, eventually resulting in document edits **/ - - type Node_Text_Edit = (String, List[Text_Edit]) // FIXME None: remove - - type Edit[C] = - (String, // node name - Option[List[(Option[C], Option[C])]]) // None: remove, Some: insert/remove commands - - abstract class Snapshot - { - val version: Version - val node: Node - val is_outdated: Boolean - def convert(offset: Int): Int - def revert(offset: Int): Int - def lookup_command(id: Command_ID): Option[Command] - def state(command: Command): Command.State - } + /* changes of plain text, eventually resulting in document edits */ object Change { @@ -123,6 +115,61 @@ } + /* history navigation and persistent snapshots */ + + abstract class Snapshot + { + val version: Version + val node: Node + val is_outdated: Boolean + def convert(offset: Int): Int + def revert(offset: Int): Int + def lookup_command(id: Command_ID): Option[Command] + def state(command: Command): Command.State + } + + object History + { + val init = new History(List(Change.init)) + } + + // FIXME pruning, purging of state + class History(undo_list: List[Change]) + { + require(!undo_list.isEmpty) + + def tip: Change = undo_list.head + def +(ch: Change): History = new History(ch :: undo_list) + + def snapshot(name: String, pending_edits: List[Text_Edit], state_snapshot: State): Snapshot = + { + val found_stable = undo_list.find(change => + change.is_finished && state_snapshot.is_assigned(change.current.join)) + require(found_stable.isDefined) + val stable = found_stable.get + val latest = undo_list.head + + val edits = + (pending_edits /: undo_list.takeWhile(_ != stable))((edits, change) => + (for ((a, eds) <- change.edits if a == name) yield eds).flatten ::: edits) + lazy val reverse_edits = edits.reverse + + new Snapshot + { + val version = stable.current.join + val node = version.nodes(name) + val is_outdated = !(pending_edits.isEmpty && latest == stable) + def convert(offset: Int): Int = (offset /: edits)((i, edit) => edit.convert(i)) + def revert(offset: Int): Int = (offset /: reverse_edits)((i, edit) => edit.revert(i)) + def lookup_command(id: Command_ID): Option[Command] = state_snapshot.lookup_command(id) + def state(command: Command): Command.State = + try { state_snapshot.command_state(version, command) } + catch { case _: State.Fail => command.empty_state } + } + } + } + + /** global state -- document structure and execution process **/ diff -r a9cff3f2e479 -r 940a404e45e2 src/Pure/System/session.scala --- a/src/Pure/System/session.scala Sun Aug 15 20:27:29 2010 +0200 +++ b/src/Pure/System/session.scala Sun Aug 15 21:03:13 2010 +0200 @@ -290,56 +290,26 @@ private val editor_history = new Actor { - @volatile private var history = List(Document.Change.init) + @volatile private var history = Document.History.init def snapshot(name: String, pending_edits: List[Text_Edit]): Document.Snapshot = - { - val state_snapshot = current_state() - val history_snapshot = history - - val found_stable = history_snapshot.find(change => - change.is_finished && state_snapshot.is_assigned(change.current.join)) - require(found_stable.isDefined) - val stable = found_stable.get - val latest = history_snapshot.head - - val edits = - (pending_edits /: history_snapshot.takeWhile(_ != stable))((edits, change) => - (for ((a, eds) <- change.edits if a == name) yield eds).flatten ::: edits) - lazy val reverse_edits = edits.reverse - - new Document.Snapshot { - val version = stable.current.join - val node = version.nodes(name) - val is_outdated = !(pending_edits.isEmpty && latest == stable) - def convert(offset: Int): Int = (offset /: edits)((i, edit) => edit.convert(i)) - def revert(offset: Int): Int = (offset /: reverse_edits)((i, edit) => edit.revert(i)) - def lookup_command(id: Document.Command_ID): Option[Command] = - state_snapshot.lookup_command(id) - def state(command: Command): Command.State = - try { state_snapshot.command_state(version, command) } - catch { case _: Document.State.Fail => command.empty_state } - } - } + history.snapshot(name, pending_edits, current_state()) def act { loop { react { case Edit_Version(edits) => - val history_snapshot = history - require(!history_snapshot.isEmpty) - - val prev = history_snapshot.head.current + val prev = history.tip.current val result = isabelle.Future.fork { val previous = prev.join val former_assignment = current_state().the_assignment(previous).join // FIXME async!? Thy_Syntax.text_edits(Session.this, previous, edits) } - val new_change = new Document.Change(prev, edits, result) - history ::= new_change - new_change.current.map(_ => session_actor ! new_change) + val change = new Document.Change(prev, edits, result) + history += change + change.current.map(_ => session_actor ! change) reply(()) case bad => System.err.println("editor_model: ignoring bad message " + bad)