12 import scala.annotation.tailrec |
12 import scala.annotation.tailrec |
13 |
13 |
14 |
14 |
15 object Document |
15 object Document |
16 { |
16 { |
17 /* unique identifiers */ |
17 /* formal identifiers */ |
18 |
18 |
|
19 type Version_ID = String |
|
20 type Command_ID = String |
19 type State_ID = String |
21 type State_ID = String |
20 type Command_ID = String |
|
21 type Version_ID = String |
|
22 |
22 |
23 val NO_ID = "" |
23 val NO_ID = "" |
24 |
24 |
25 |
25 |
26 /* command start positions */ |
26 |
27 |
27 /** named document nodes **/ |
28 def command_starts(commands: Iterator[Command], offset: Int = 0): Iterator[(Command, Int)] = |
|
29 { |
|
30 var i = offset |
|
31 for (command <- commands) yield { |
|
32 val start = i |
|
33 i += command.length |
|
34 (command, start) |
|
35 } |
|
36 } |
|
37 |
|
38 |
|
39 /* named document nodes */ |
|
40 |
28 |
41 object Node |
29 object Node |
42 { |
30 { |
43 val empty: Node = new Node(Linear_Set()) |
31 val empty: Node = new Node(Linear_Set()) |
|
32 |
|
33 def command_starts(commands: Iterator[Command], offset: Int = 0): Iterator[(Command, Int)] = |
|
34 { |
|
35 var i = offset |
|
36 for (command <- commands) yield { |
|
37 val start = i |
|
38 i += command.length |
|
39 (command, start) |
|
40 } |
|
41 } |
44 } |
42 } |
45 |
43 |
46 class Node(val commands: Linear_Set[Command]) |
44 class Node(val commands: Linear_Set[Command]) |
47 { |
45 { |
48 /* command ranges */ |
46 /* command ranges */ |
49 |
47 |
50 def command_starts: Iterator[(Command, Int)] = |
48 def command_starts: Iterator[(Command, Int)] = |
51 Document.command_starts(commands.iterator) |
49 Node.command_starts(commands.iterator) |
52 |
50 |
53 def command_start(cmd: Command): Option[Int] = |
51 def command_start(cmd: Command): Option[Int] = |
54 command_starts.find(_._1 == cmd).map(_._2) |
52 command_starts.find(_._1 == cmd).map(_._2) |
55 |
53 |
56 def command_range(i: Int): Iterator[(Command, Int)] = |
54 def command_range(i: Int): Iterator[(Command, Int)] = |
83 doc |
81 doc |
84 } |
82 } |
85 |
83 |
86 |
84 |
87 |
85 |
88 /** editing **/ |
86 /** changes of plain text, eventually resulting in document edits **/ |
89 |
87 |
90 type Node_Text_Edit = (String, List[Text_Edit]) // FIXME None: remove |
88 type Node_Text_Edit = (String, List[Text_Edit]) // FIXME None: remove |
91 |
89 |
92 type Edit[C] = |
90 type Edit[C] = |
93 (String, // node name |
91 (String, // node name |
94 Option[List[(Option[C], Option[C])]]) // None: remove, Some: insert/remove commands |
92 Option[List[(Option[C], Option[C])]]) // None: remove, Some: insert/remove commands |
95 |
93 |
|
94 abstract class Snapshot |
|
95 { |
|
96 val document: Document |
|
97 val node: Document.Node |
|
98 val is_outdated: Boolean |
|
99 def convert(offset: Int): Int |
|
100 def revert(offset: Int): Int |
|
101 } |
|
102 |
|
103 object Change |
|
104 { |
|
105 val init = new Change(NO_ID, None, Nil, Future.value(Nil, Document.init)) |
|
106 } |
|
107 |
|
108 class Change( |
|
109 val id: Version_ID, |
|
110 val parent: Option[Change], |
|
111 val edits: List[Node_Text_Edit], |
|
112 val result: Future[(List[Edit[Command]], Document)]) |
|
113 { |
|
114 def ancestors: Iterator[Change] = new Iterator[Change] |
|
115 { |
|
116 private var state: Option[Change] = Some(Change.this) |
|
117 def hasNext = state.isDefined |
|
118 def next = |
|
119 state match { |
|
120 case Some(change) => state = change.parent; change |
|
121 case None => throw new NoSuchElementException("next on empty iterator") |
|
122 } |
|
123 } |
|
124 |
|
125 def join_document: Document = result.join._2 |
|
126 def is_assigned: Boolean = result.is_finished && join_document.assignment.is_finished |
|
127 |
|
128 def snapshot(name: String, pending_edits: List[Text_Edit]): Snapshot = |
|
129 { |
|
130 val latest = Change.this |
|
131 val stable = latest.ancestors.find(_.is_assigned) |
|
132 require(stable.isDefined) |
|
133 |
|
134 val edits = |
|
135 (pending_edits /: latest.ancestors.takeWhile(_ != stable.get))((edits, change) => |
|
136 (for ((a, eds) <- change.edits if a == name) yield eds).flatten ::: edits) |
|
137 lazy val reverse_edits = edits.reverse |
|
138 |
|
139 new Snapshot { |
|
140 val document = stable.get.join_document |
|
141 val node = document.nodes(name) |
|
142 val is_outdated = !(pending_edits.isEmpty && latest == stable.get) |
|
143 def convert(offset: Int): Int = (offset /: edits)((i, edit) => edit.convert(i)) |
|
144 def revert(offset: Int): Int = (offset /: reverse_edits)((i, edit) => edit.revert(i)) |
|
145 } |
|
146 } |
|
147 } |
|
148 |
|
149 |
|
150 |
|
151 /** editing **/ |
|
152 |
96 def text_edits(session: Session, old_doc: Document, new_id: Version_ID, |
153 def text_edits(session: Session, old_doc: Document, new_id: Version_ID, |
97 edits: List[Node_Text_Edit]): (List[Edit[Command]], Document) = |
154 edits: List[Node_Text_Edit]): (List[Edit[Command]], Document) = |
98 { |
155 { |
99 require(old_doc.assignment.is_finished) |
156 require(old_doc.assignment.is_finished) |
100 |
157 |
112 @tailrec def edit_text(eds: List[Text_Edit], |
169 @tailrec def edit_text(eds: List[Text_Edit], |
113 commands: Linear_Set[Command]): Linear_Set[Command] = |
170 commands: Linear_Set[Command]): Linear_Set[Command] = |
114 { |
171 { |
115 eds match { |
172 eds match { |
116 case e :: es => |
173 case e :: es => |
117 command_starts(commands.iterator).find { |
174 Node.command_starts(commands.iterator).find { |
118 case (cmd, cmd_start) => |
175 case (cmd, cmd_start) => |
119 e.can_edit(cmd.source, cmd_start) || |
176 e.can_edit(cmd.source, cmd_start) || |
120 e.is_insert && e.start == cmd_start + cmd.length |
177 e.is_insert && e.start == cmd_start + cmd.length |
121 } match { |
178 } match { |
122 case Some((cmd, cmd_start)) if e.can_edit(cmd.source, cmd_start) => |
179 case Some((cmd, cmd_start)) if e.can_edit(cmd.source, cmd_start) => |