69 make_document dir name start (f entries); |
69 make_document dir name start (f entries); |
70 |
70 |
71 |
71 |
72 (* iterate entries *) |
72 (* iterate entries *) |
73 |
73 |
74 fun fold_entries opt_id f (Document {start, entries, ...}) = |
74 fun fold_entries id0 f (Document {entries, ...}) = |
75 let |
75 let |
76 fun apply NONE x = x |
76 fun apply NONE x = x |
77 | apply (SOME id) x = apply (#next (the_entry entries id)) (f id x); |
77 | apply (SOME id) x = |
78 in if is_some opt_id then apply opt_id else apply (SOME start) end; |
78 let val entry = the_entry entries id |
79 |
79 in apply (#next entry) (f (id, entry) x) end; |
80 fun find_entries P (Document {start, entries, ...}) = |
80 in if Symtab.defined entries id0 then apply (SOME id0) else I end; |
|
81 |
|
82 fun first_entry P (Document {start, entries, ...}) = |
81 let |
83 let |
82 fun find _ NONE = NONE |
84 fun find _ NONE = NONE |
83 | find prev (SOME id) = |
85 | find prev (SOME id) = |
84 if P id then SOME (prev, id) |
86 let val entry = the_entry entries id |
85 else find (SOME id) (#next (the_entry entries id)); |
87 in if P (id, entry) then SOME (prev, id) else find (SOME id) (#next entry) end; |
86 in find NONE (SOME start) end; |
88 in find NONE (SOME start) end; |
87 |
89 |
88 |
90 |
89 (* modify entries *) |
91 (* modify entries *) |
90 |
92 |
177 fun end_document (id: document_id) = error "FIXME"; |
179 fun end_document (id: document_id) = error "FIXME"; |
178 |
180 |
179 |
181 |
180 (* document editing *) |
182 (* document editing *) |
181 |
183 |
182 fun update_state tr state = Future.fork_deps [state] (fn () => |
184 local |
183 (case Future.join state of NONE => NONE | SOME st => Toplevel.run_command tr st)); |
185 |
|
186 fun is_changed entries' (id, {next = _, state}) = |
|
187 (case try (the_entry entries') id of |
|
188 SOME {next = _, state = state'} => state' <> state |
|
189 | _ => true); |
|
190 |
|
191 fun cancel_state (id, {next = _, state = SOME state_id}) () = Future.cancel (the_state state_id) |
|
192 | cancel_state _ () = (); |
|
193 |
|
194 fun update_state tr state state_id' = |
|
195 Future.fork_deps [state] (fn () => |
|
196 (case Future.join state of |
|
197 NONE => NONE |
|
198 | SOME st => Toplevel.run_command (Toplevel.put_id state_id' tr) st)); |
|
199 |
|
200 fun new_state (id, _) (state_id, updates) = |
|
201 let |
|
202 val state_id' = new_id (); |
|
203 val state' = update_state (the_command id) (the_state state_id) state_id'; |
|
204 val _ = define_state state_id' state'; |
|
205 in (state_id', (id, state_id') :: updates) end; |
184 |
206 |
185 fun update_states old_document new_document = |
207 fun update_states old_document new_document = |
186 let |
208 let |
|
209 fun cancel_old id = fold_entries id cancel_state old_document (); |
|
210 |
187 val Document {entries = old_entries, ...} = old_document; |
211 val Document {entries = old_entries, ...} = old_document; |
188 val Document {entries = new_entries, ...} = new_document; |
212 val Document {entries = new_entries, ...} = new_document; |
189 |
|
190 fun is_changed id = |
|
191 (case try (the_entry new_entries) id of |
|
192 SOME {state = SOME _, ...} => false |
|
193 | _ => true); |
|
194 |
|
195 fun cancel_state id () = |
|
196 (case the_entry old_entries id of |
|
197 {state = SOME state_id, ...} => Future.cancel (the_state state_id) |
|
198 | _ => ()); |
|
199 |
|
200 fun new_state id (state_id, updates) = |
|
201 let |
|
202 val state_id' = new_id (); |
|
203 val state' = update_state (the_command id) (the_state state_id); |
|
204 val _ = define_state state_id' state'; |
|
205 in (state_id', (id, state_id') :: updates) end; |
|
206 in |
213 in |
207 (case find_entries is_changed old_document of |
214 (case first_entry (is_changed old_entries) new_document of |
208 NONE => ([], new_document) |
215 NONE => |
|
216 (case first_entry (is_changed new_entries) old_document of |
|
217 NONE => ([], new_document) |
|
218 | SOME (_, id) => (cancel_old id; ([], new_document))) |
209 | SOME (prev, id) => |
219 | SOME (prev, id) => |
210 let |
220 let |
211 val _ = fold_entries (SOME id) cancel_state old_document (); |
221 val _ = cancel_old id; |
212 val prev_state_id = the (#state (the_entry new_entries (the prev))); |
222 val prev_state_id = the (#state (the_entry new_entries (the prev))); |
213 val (_, updates) = fold_entries (SOME id) new_state new_document (prev_state_id, []); |
223 val (_, updates) = fold_entries id new_state new_document (prev_state_id, []); |
214 val new_document' = new_document |> map_entries (fold set_entry_state updates); |
224 val new_document' = new_document |> map_entries (fold set_entry_state updates); |
215 in (updates, new_document') end) |
225 in (rev updates, new_document') end) |
216 end; |
226 end; |
217 |
227 |
218 fun report_updates _ [] = () |
228 fun report_updates _ [] = () |
219 | report_updates (document_id: document_id) updates = |
229 | report_updates (document_id: document_id) updates = |
220 implode (map (fn (id, state_id) => Markup.markup (Markup.edit id state_id) "") updates) |
230 implode (map (fn (id, state_id) => Markup.markup (Markup.edit id state_id) "") updates) |
221 |> Markup.markup (Markup.edits document_id) |
231 |> Markup.markup (Markup.edits document_id) |
222 |> Output.status; |
232 |> Output.status; |
|
233 |
|
234 in |
223 |
235 |
224 fun edit_document (id: document_id) (id': document_id) edits = |
236 fun edit_document (id: document_id) (id': document_id) edits = |
225 let |
237 let |
226 val document = Document (the_document id); |
238 val document = Document (the_document id); |
227 val (updates, document') = |
239 val (updates, document') = |