|
1 (* Title: Pure/System/isar_document.ML |
|
2 Author: Makarius |
|
3 |
|
4 Interactive Isar documents, which are structured as follows: |
|
5 |
|
6 - history: tree of documents (i.e. changes without merge) |
|
7 - document: graph of nodes (cf. theory files) |
|
8 - node: linear set of commands, potentially with proof structure |
|
9 *) |
|
10 |
|
11 structure Isar_Document: sig end = |
|
12 struct |
|
13 |
|
14 (* unique identifiers *) |
|
15 |
|
16 local |
|
17 val id_count = Synchronized.var "id" 0; |
|
18 in |
|
19 fun create_id () = |
|
20 Synchronized.change_result id_count |
|
21 (fn i => |
|
22 let val i' = i + 1 |
|
23 in (i', i') end); |
|
24 end; |
|
25 |
|
26 fun err_dup kind id = error ("Duplicate " ^ kind ^ ": " ^ Document.print_id id); |
|
27 fun err_undef kind id = error ("Undefined " ^ kind ^ ": " ^ Document.print_id id); |
|
28 |
|
29 |
|
30 (** documents **) |
|
31 |
|
32 datatype entry = Entry of {next: Document.command_id option, exec: Document.exec_id option}; |
|
33 type node = entry Inttab.table; (*unique command entries indexed by command_id, start with no_id*) |
|
34 type document = node Graph.T; (*development graph via static imports*) |
|
35 |
|
36 |
|
37 (* command entries *) |
|
38 |
|
39 fun make_entry next exec = Entry {next = next, exec = exec}; |
|
40 |
|
41 fun the_entry (node: node) (id: Document.command_id) = |
|
42 (case Inttab.lookup node id of |
|
43 NONE => err_undef "command entry" id |
|
44 | SOME (Entry entry) => entry); |
|
45 |
|
46 fun put_entry (id: Document.command_id, entry: entry) = Inttab.update (id, entry); |
|
47 |
|
48 fun put_entry_exec (id: Document.command_id) exec (node: node) = |
|
49 let val {next, ...} = the_entry node id |
|
50 in put_entry (id, make_entry next exec) node end; |
|
51 |
|
52 fun reset_entry_exec id = put_entry_exec id NONE; |
|
53 fun set_entry_exec (id, exec_id) = put_entry_exec id (SOME exec_id); |
|
54 |
|
55 |
|
56 (* iterate entries *) |
|
57 |
|
58 fun fold_entries id0 f (node: node) = |
|
59 let |
|
60 fun apply NONE x = x |
|
61 | apply (SOME id) x = |
|
62 let val entry = the_entry node id |
|
63 in apply (#next entry) (f (id, entry) x) end; |
|
64 in if Inttab.defined node id0 then apply (SOME id0) else I end; |
|
65 |
|
66 fun first_entry P (node: node) = |
|
67 let |
|
68 fun first _ NONE = NONE |
|
69 | first prev (SOME id) = |
|
70 let val entry = the_entry node id |
|
71 in if P (id, entry) then SOME (prev, id, entry) else first (SOME id) (#next entry) end; |
|
72 in first NONE (SOME Document.no_id) end; |
|
73 |
|
74 |
|
75 (* modify entries *) |
|
76 |
|
77 fun insert_after (id: Document.command_id) (id2: Document.command_id) (node: node) = |
|
78 let val {next, exec} = the_entry node id in |
|
79 node |
|
80 |> put_entry (id, make_entry (SOME id2) exec) |
|
81 |> put_entry (id2, make_entry next NONE) |
|
82 end; |
|
83 |
|
84 fun delete_after (id: Document.command_id) (node: node) = |
|
85 let val {next, exec} = the_entry node id in |
|
86 (case next of |
|
87 NONE => error ("No next entry to delete: " ^ Document.print_id id) |
|
88 | SOME id2 => |
|
89 node |> |
|
90 (case #next (the_entry node id2) of |
|
91 NONE => put_entry (id, make_entry NONE exec) |
|
92 | SOME id3 => put_entry (id, make_entry (SOME id3) exec) #> reset_entry_exec id3)) |
|
93 end; |
|
94 |
|
95 |
|
96 (* node operations *) |
|
97 |
|
98 val empty_node: node = Inttab.make [(Document.no_id, make_entry NONE (SOME Document.no_id))]; |
|
99 |
|
100 fun the_node (document: document) name = |
|
101 Graph.get_node document name handle Graph.UNDEF _ => empty_node; |
|
102 |
|
103 fun edit_node (id, SOME id2) = insert_after id id2 |
|
104 | edit_node (id, NONE) = delete_after id; |
|
105 |
|
106 fun edit_nodes (name, SOME edits) = |
|
107 Graph.default_node (name, empty_node) #> |
|
108 Graph.map_node name (fold edit_node edits) |
|
109 | edit_nodes (name, NONE) = Graph.del_node name; |
|
110 |
|
111 |
|
112 |
|
113 (** global configuration **) |
|
114 |
|
115 (* command executions *) |
|
116 |
|
117 local |
|
118 |
|
119 val global_execs = |
|
120 Unsynchronized.ref (Inttab.make [(Document.no_id, Lazy.value (SOME Toplevel.toplevel))]); |
|
121 |
|
122 in |
|
123 |
|
124 fun define_exec (id: Document.exec_id) exec = |
|
125 NAMED_CRITICAL "Isar" (fn () => |
|
126 Unsynchronized.change global_execs (Inttab.update_new (id, exec)) |
|
127 handle Inttab.DUP dup => err_dup "exec" dup); |
|
128 |
|
129 fun the_exec (id: Document.exec_id) = |
|
130 (case Inttab.lookup (! global_execs) id of |
|
131 NONE => err_undef "exec" id |
|
132 | SOME exec => exec); |
|
133 |
|
134 end; |
|
135 |
|
136 |
|
137 (* commands *) |
|
138 |
|
139 local |
|
140 |
|
141 val global_commands = Unsynchronized.ref (Inttab.make [(Document.no_id, Toplevel.empty)]); |
|
142 |
|
143 in |
|
144 |
|
145 fun define_command (id: Document.command_id) text = |
|
146 let |
|
147 val id_string = Document.print_id id; |
|
148 val tr = |
|
149 Position.setmp_thread_data (Position.id_only id_string) (fn () => |
|
150 Outer_Syntax.prepare_command (Position.id id_string) text) (); |
|
151 in |
|
152 NAMED_CRITICAL "Isar" (fn () => |
|
153 Unsynchronized.change global_commands (Inttab.update_new (id, Toplevel.put_id id_string tr)) |
|
154 handle Inttab.DUP dup => err_dup "command" dup) |
|
155 end; |
|
156 |
|
157 fun the_command (id: Document.command_id) = |
|
158 (case Inttab.lookup (! global_commands) id of |
|
159 NONE => err_undef "command" id |
|
160 | SOME tr => tr); |
|
161 |
|
162 end; |
|
163 |
|
164 |
|
165 (* document versions *) |
|
166 |
|
167 local |
|
168 |
|
169 val global_documents = Unsynchronized.ref (Inttab.make [(Document.no_id, Graph.empty: document)]); |
|
170 |
|
171 in |
|
172 |
|
173 fun define_document (id: Document.version_id) document = |
|
174 NAMED_CRITICAL "Isar" (fn () => |
|
175 Unsynchronized.change global_documents (Inttab.update_new (id, document)) |
|
176 handle Inttab.DUP dup => err_dup "document" dup); |
|
177 |
|
178 fun the_document (id: Document.version_id) = |
|
179 (case Inttab.lookup (! global_documents) id of |
|
180 NONE => err_undef "document" id |
|
181 | SOME document => document); |
|
182 |
|
183 end; |
|
184 |
|
185 |
|
186 |
|
187 (** document editing **) |
|
188 |
|
189 (* execution *) |
|
190 |
|
191 local |
|
192 |
|
193 val execution: unit future list Unsynchronized.ref = Unsynchronized.ref []; |
|
194 |
|
195 fun force_exec NONE = () |
|
196 | force_exec (SOME exec_id) = ignore (Lazy.force (the_exec exec_id)); |
|
197 |
|
198 in |
|
199 |
|
200 fun execute document = |
|
201 NAMED_CRITICAL "Isar" (fn () => |
|
202 let |
|
203 val old_execution = ! execution; |
|
204 val _ = List.app Future.cancel old_execution; |
|
205 fun await_cancellation () = uninterruptible (K Future.join_results) old_execution; |
|
206 (* FIXME proper node deps *) |
|
207 val new_execution = Graph.keys document |> map (fn name => |
|
208 Future.fork_pri 1 (fn () => |
|
209 let |
|
210 val _ = await_cancellation (); |
|
211 val exec = |
|
212 fold_entries Document.no_id (fn (_, {exec, ...}) => fn () => force_exec exec) |
|
213 (the_node document name); |
|
214 in exec () end)); |
|
215 in execution := new_execution end); |
|
216 |
|
217 end; |
|
218 |
|
219 |
|
220 (* editing *) |
|
221 |
|
222 local |
|
223 |
|
224 fun is_changed node' (id, {next = _, exec}) = |
|
225 (case try (the_entry node') id of |
|
226 NONE => true |
|
227 | SOME {next = _, exec = exec'} => exec' <> exec); |
|
228 |
|
229 fun new_exec name (id: Document.command_id) (exec_id, updates) = |
|
230 let |
|
231 val exec = the_exec exec_id; |
|
232 val exec_id' = create_id (); |
|
233 val tr = Toplevel.put_id (Document.print_id exec_id') (the_command id); |
|
234 val exec' = |
|
235 Lazy.lazy (fn () => |
|
236 (case Lazy.force exec of |
|
237 NONE => NONE |
|
238 | SOME st => Toplevel.run_command name tr st)); |
|
239 val _ = define_exec exec_id' exec'; |
|
240 in (exec_id', (id, exec_id') :: updates) end; |
|
241 |
|
242 fun updates_status new_id updates = |
|
243 implode (map (fn (id, exec_id) => |
|
244 Markup.markup (Markup.edit (Document.print_id id) (Document.print_id exec_id)) "") updates) |
|
245 |> Markup.markup Markup.assign |
|
246 |> Position.setmp_thread_data (Position.id_only (Document.print_id new_id)) Output.status; |
|
247 (*FIXME avoid setmp -- direct message argument*) |
|
248 |
|
249 in |
|
250 |
|
251 fun edit_document (old_id: Document.version_id) (new_id: Document.version_id) edits = |
|
252 NAMED_CRITICAL "Isar" (fn () => |
|
253 let |
|
254 val old_document = the_document old_id; |
|
255 val new_document = fold edit_nodes edits old_document; |
|
256 |
|
257 fun update_node name node = |
|
258 (case first_entry (is_changed (the_node old_document name)) node of |
|
259 NONE => ([], node) |
|
260 | SOME (prev, id, _) => |
|
261 let |
|
262 val prev_exec_id = the (#exec (the_entry node (the prev))); |
|
263 val (_, updates) = fold_entries id (new_exec name o #1) node (prev_exec_id, []); |
|
264 val node' = fold set_entry_exec updates node; |
|
265 in (rev updates, node') end); |
|
266 |
|
267 (* FIXME proper node deps *) |
|
268 val (updatess, new_document') = |
|
269 (Graph.keys new_document, new_document) |
|
270 |-> fold_map (fn name => Graph.map_node_yield name (update_node name)); |
|
271 |
|
272 val _ = define_document new_id new_document'; |
|
273 val _ = updates_status new_id (flat updatess); |
|
274 val _ = execute new_document'; |
|
275 in () end); |
|
276 |
|
277 end; |
|
278 |
|
279 |
|
280 |
|
281 (** Isabelle process commands **) |
|
282 |
|
283 val _ = |
|
284 Isabelle_Process.add_command "Isar_Document.define_command" |
|
285 (fn [id, text] => define_command (Document.parse_id id) text); |
|
286 |
|
287 val _ = |
|
288 Isabelle_Process.add_command "Isar_Document.edit_document" |
|
289 (fn [old_id, new_id, edits] => |
|
290 edit_document (Document.parse_id old_id) (Document.parse_id new_id) |
|
291 (XML_Data.dest_list (XML_Data.dest_pair XML_Data.dest_string |
|
292 (XML_Data.dest_option (XML_Data.dest_list |
|
293 (XML_Data.dest_pair XML_Data.dest_int |
|
294 (XML_Data.dest_option XML_Data.dest_int))))) (YXML.parse_body edits))); |
|
295 |
|
296 end; |
|
297 |