--- a/src/Pure/PIDE/document.scala Thu Nov 11 13:23:39 2010 +0100
+++ b/src/Pure/PIDE/document.scala Thu Nov 11 16:48:46 2010 +0100
@@ -17,7 +17,8 @@
type ID = Long
- object ID {
+ object ID
+ {
def apply(id: ID): String = Markup.Long.apply(id)
def unapply(s: String): Option[ID] = Markup.Long.unapply(s)
}
@@ -34,7 +35,9 @@
/* named nodes -- development graph */
- type Node_Text_Edit = (String, List[Text.Edit]) // FIXME None: remove
+ type Text_Edit =
+ (String, // node name
+ Option[List[Text.Edit]]) // None: remove, Some: insert/remove text
type Edit[C] =
(String, // node name
@@ -133,7 +136,7 @@
class Change(
val previous: Future[Version],
- val edits: List[Node_Text_Edit],
+ val edits: List[Text_Edit],
val result: Future[(List[Edit[Command]], Version)])
{
val version: Future[Version] = result.map(_._2)
@@ -267,7 +270,7 @@
}
def extend_history(previous: Future[Version],
- edits: List[Node_Text_Edit],
+ edits: List[Text_Edit],
result: Future[(List[Edit[Command]], Version)]): (Change, State) =
{
val change = new Change(previous, edits, result)
@@ -284,9 +287,10 @@
val stable = found_stable.get
val latest = history.undo_list.head
+ // FIXME proper treatment of deleted nodes
val edits =
(pending_edits /: history.undo_list.takeWhile(_ != stable))((edits, change) =>
- (for ((a, eds) <- change.edits if a == name) yield eds).flatten ::: edits)
+ (for ((a, Some(eds)) <- change.edits if a == name) yield eds).flatten ::: edits)
lazy val reverse_edits = edits.reverse
new Snapshot