45 type Result = (Document, List[Structure_Edit]) |
45 type Result = (Document, List[Structure_Edit]) |
46 |
46 |
47 def text_edits(session: Session, old_doc: Document, new_id: Isar_Document.Document_ID, |
47 def text_edits(session: Session, old_doc: Document, new_id: Isar_Document.Document_ID, |
48 edits: List[Text_Edit]): Result = |
48 edits: List[Text_Edit]): Result = |
49 { |
49 { |
|
50 require(old_doc.assignment.is_finished) |
|
51 val doc0 = |
|
52 Document_Body(old_doc.tokens, old_doc.token_start, old_doc.commands, old_doc.assignment.join) |
|
53 |
50 val changes = new mutable.ListBuffer[Structure_Edit] |
54 val changes = new mutable.ListBuffer[Structure_Edit] |
51 val new_doc = (old_doc /: edits)((doc1: Document, edit: Text_Edit) => |
55 val doc = (doc0 /: edits)((doc1: Document_Body, edit: Text_Edit) => |
52 { |
56 { |
53 val (doc2, chgs) = doc1.text_edit(session, edit, new_id) // FIXME odd multiple use of id |
57 val (doc2, chgs) = doc1.text_edit(session, edit) |
54 changes ++ chgs |
58 changes ++ chgs |
55 doc2 |
59 doc2 |
56 }) |
60 }) |
|
61 val new_doc = new Document(new_id, doc.tokens, doc.token_start, doc.commands, doc.states) |
57 (new_doc, changes.toList) |
62 (new_doc, changes.toList) |
58 } |
63 } |
59 } |
64 } |
60 |
65 |
61 |
66 private case class Document_Body( |
62 class Document( |
67 val tokens: Linear_Set[Token], // FIXME plain List, inside Command |
63 val id: Isar_Document.Document_ID, |
68 val token_start: Map[Token, Int], // FIXME eliminate |
64 val tokens: Linear_Set[Token], // FIXME plain List, inside Command |
69 val commands: Linear_Set[Command], |
65 val token_start: Map[Token, Int], // FIXME eliminate |
70 val states: Map[Command, Command]) |
66 val commands: Linear_Set[Command], |
|
67 old_states: Map[Command, Command]) |
|
68 { |
71 { |
69 def content = Token.string_from_tokens(Nil ++ tokens, token_start) |
72 /* token view */ |
70 |
73 |
71 |
74 def text_edit(session: Session, e: Text_Edit): (Document_Body, List[Document.Structure_Edit]) = |
72 /* command/state assignment */ |
|
73 |
|
74 val assignment = Future.promise[Map[Command, Command]] |
|
75 def is_assigned = assignment.is_finished |
|
76 |
|
77 @volatile private var tmp_states = old_states |
|
78 |
|
79 def assign_states(new_states: List[(Command, Command)]) |
|
80 { |
|
81 assignment.fulfill(tmp_states ++ new_states) |
|
82 tmp_states = Map() |
|
83 } |
|
84 |
|
85 def current_state(cmd: Command): State = |
|
86 { |
|
87 require(assignment.is_finished) |
|
88 (assignment.join)(cmd).current_state |
|
89 } |
|
90 |
|
91 |
|
92 |
|
93 /** token view **/ |
|
94 |
|
95 def text_edit(session: Session, e: Text_Edit, id: String): Document.Result = |
|
96 { |
75 { |
97 case class TextChange(start: Int, added: String, removed: String) |
76 case class TextChange(start: Int, added: String, removed: String) |
98 val change = e match { |
77 val change = e match { |
99 case Text_Edit.Insert(s, a) => TextChange(s, a, "") |
78 case Text_Edit.Insert(s, a) => TextChange(s, a, "") |
100 case Text_Edit.Remove(s, r) => TextChange(s, "", r) |
79 case Text_Edit.Remove(s, r) => TextChange(s, "", r) |
164 case _ => |
143 case _ => |
165 } |
144 } |
166 } |
145 } |
167 val insert = new_tokens.reverse |
146 val insert = new_tokens.reverse |
168 val new_token_list = begin ::: insert ::: old_suffix |
147 val new_token_list = begin ::: insert ::: old_suffix |
169 token_changed(session, id, begin.lastOption, insert, |
148 token_changed(session, begin.lastOption, insert, |
170 old_suffix.firstOption, new_token_list, start) |
149 old_suffix.firstOption, new_token_list, start) |
171 } |
150 } |
172 |
151 |
173 |
152 |
174 /** command view **/ |
153 /* command view */ |
175 |
154 |
176 private def token_changed( |
155 private def token_changed( |
177 session: Session, |
156 session: Session, |
178 new_id: String, |
|
179 before_change: Option[Token], |
157 before_change: Option[Token], |
180 inserted_tokens: List[Token], |
158 inserted_tokens: List[Token], |
181 after_change: Option[Token], |
159 after_change: Option[Token], |
182 new_tokens: List[Token], |
160 new_tokens: List[Token], |
183 new_token_start: Map[Token, Int]): |
161 new_token_start: Map[Token, Int]): (Document_Body, Document.Structure_Change) = |
184 Document.Result = |
162 { |
185 { |
|
186 require(assignment.is_finished) |
|
187 |
|
188 val new_tokenset = Linear_Set[Token]() ++ new_tokens |
163 val new_tokenset = Linear_Set[Token]() ++ new_tokens |
189 val cmd_before_change = before_change match { |
164 val cmd_before_change = before_change match { |
190 case None => None |
165 case None => None |
191 case Some(bc) => |
166 case Some(bc) => |
192 val cmd_with_bc = commands.find(_.contains(bc)).get |
167 val cmd_with_bc = commands.find(_.contains(bc)).get |
259 delete_between(cmd_before_change, cmd_after_change). |
234 delete_between(cmd_before_change, cmd_after_change). |
260 append_after(cmd_before_change, inserted_commands) |
235 append_after(cmd_before_change, inserted_commands) |
261 |
236 |
262 |
237 |
263 val doc = |
238 val doc = |
264 new Document(new_id, new_tokenset, new_token_start, new_commandset, |
239 new Document_Body(new_tokenset, new_token_start, new_commandset, states -- removed_commands) |
265 assignment.join -- removed_commands) |
|
266 |
240 |
267 val removes = |
241 val removes = |
268 for (cmd <- removed_commands) yield (cmd_before_change -> None) |
242 for (cmd <- removed_commands) yield (cmd_before_change -> None) |
269 val inserts = |
243 val inserts = |
270 for (cmd <- inserted_commands) yield (doc.commands.prev(cmd) -> Some(cmd)) |
244 for (cmd <- inserted_commands) yield (doc.commands.prev(cmd) -> Some(cmd)) |
271 |
245 |
272 return (doc, removes.toList ++ inserts) |
246 (doc, removes.toList ++ inserts) |
273 } |
247 } |
|
248 } |
|
249 |
|
250 class Document( |
|
251 val id: Isar_Document.Document_ID, |
|
252 val tokens: Linear_Set[Token], // FIXME plain List, inside Command |
|
253 val token_start: Map[Token, Int], // FIXME eliminate |
|
254 val commands: Linear_Set[Command], |
|
255 old_states: Map[Command, Command]) |
|
256 { |
|
257 def content = Token.string_from_tokens(Nil ++ tokens, token_start) |
|
258 |
|
259 |
|
260 /* command/state assignment */ |
|
261 |
|
262 val assignment = Future.promise[Map[Command, Command]] |
|
263 |
|
264 @volatile private var tmp_states = old_states |
|
265 |
|
266 def assign_states(new_states: List[(Command, Command)]) |
|
267 { |
|
268 assignment.fulfill(tmp_states ++ new_states) |
|
269 tmp_states = Map() |
|
270 } |
|
271 |
|
272 def current_state(cmd: Command): State = |
|
273 { |
|
274 require(assignment.is_finished) |
|
275 (assignment.join)(cmd).current_state |
|
276 } |
|
277 |
274 |
278 |
275 val commands_offsets = { |
279 val commands_offsets = { |
276 var last_stop = 0 |
280 var last_stop = 0 |
277 (for (c <- commands) yield { |
281 (for (c <- commands) yield { |
278 val r = c -> (last_stop, c.stop(this)) |
282 val r = c -> (last_stop, c.stop(this)) |