author | wenzelm |
Sat, 15 May 2010 23:16:32 +0200 | |
changeset 36950 | 75b8f26f2f07 |
parent 34285 | 218fa4267718 |
child 36951 | 985c197f2fe9 |
permissions | -rw-r--r-- |
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/Isar/isar_document.ML |
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
3 |
|
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
4 |
Interactive Isar documents. |
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
5 |
*) |
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
6 |
|
34212
8c3e1f73953d
eliminated Markup.edits/EDITS: Isar.edit_document reports Markup.edit/EDIT while running under new document id;
wenzelm
parents:
34207
diff
changeset
|
7 |
structure Isar_Document: sig end = |
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
8 |
struct |
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
9 |
|
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
10 |
(* unique identifiers *) |
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
11 |
|
29484 | 12 |
type state_id = string; |
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
13 |
type command_id = string; |
29484 | 14 |
type document_id = string; |
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
15 |
|
34206 | 16 |
val no_id = ""; |
17 |
||
18 |
local |
|
19 |
val id_count = Synchronized.var "id" 0; |
|
20 |
in |
|
21 |
fun create_id () = |
|
22 |
Synchronized.change_result id_count |
|
23 |
(fn i => |
|
24 |
let val i' = i + 1 |
|
25 |
in ("i" ^ string_of_int i', i') end); |
|
26 |
end; |
|
29467 | 27 |
|
28 |
fun err_dup kind id = error ("Duplicate " ^ kind ^ ": " ^ quote id); |
|
34206 | 29 |
fun err_undef kind id = error ("Undefined " ^ kind ^ ": " ^ quote id); |
29467 | 30 |
|
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
31 |
|
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
32 |
|
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
33 |
(** documents **) |
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
34 |
|
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
35 |
(* command entries *) |
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
36 |
|
29484 | 37 |
datatype entry = Entry of {next: command_id option, state: state_id option}; |
38 |
fun make_entry next state = Entry {next = next, state = state}; |
|
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
39 |
|
29467 | 40 |
fun the_entry entries (id: command_id) = |
41 |
(case Symtab.lookup entries id of |
|
42 |
NONE => err_undef "document entry" id |
|
43 |
| SOME (Entry entry) => entry); |
|
44 |
||
45 |
fun put_entry (id: command_id, entry: entry) = Symtab.update (id, entry); |
|
46 |
||
29489
5dfe03f423c4
edit_document: proper edits/edit markup, including the document id;
wenzelm
parents:
29487
diff
changeset
|
47 |
fun put_entry_state (id: command_id) state entries = |
5dfe03f423c4
edit_document: proper edits/edit markup, including the document id;
wenzelm
parents:
29487
diff
changeset
|
48 |
let val {next, ...} = the_entry entries id |
5dfe03f423c4
edit_document: proper edits/edit markup, including the document id;
wenzelm
parents:
29487
diff
changeset
|
49 |
in put_entry (id, make_entry next state) entries end; |
5dfe03f423c4
edit_document: proper edits/edit markup, including the document id;
wenzelm
parents:
29487
diff
changeset
|
50 |
|
29490 | 51 |
fun reset_entry_state id = put_entry_state id NONE; |
52 |
fun set_entry_state (id, state_id) = put_entry_state id (SOME state_id); |
|
29489
5dfe03f423c4
edit_document: proper edits/edit markup, including the document id;
wenzelm
parents:
29487
diff
changeset
|
53 |
|
5dfe03f423c4
edit_document: proper edits/edit markup, including the document id;
wenzelm
parents:
29487
diff
changeset
|
54 |
|
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
55 |
(* document *) |
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
56 |
|
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
57 |
datatype document = Document of |
34206 | 58 |
{dir: Path.T, (*master directory*) |
59 |
name: string, (*theory name*) |
|
60 |
entries: entry Symtab.table}; (*unique command entries indexed by command_id, start with no_id*) |
|
29467 | 61 |
|
34206 | 62 |
fun make_document dir name entries = |
63 |
Document {dir = dir, name = name, entries = entries}; |
|
29467 | 64 |
|
34206 | 65 |
fun map_entries f (Document {dir, name, entries}) = |
66 |
make_document dir name (f entries); |
|
29467 | 67 |
|
68 |
||
29484 | 69 |
(* iterate entries *) |
29468 | 70 |
|
29507 | 71 |
fun fold_entries id0 f (Document {entries, ...}) = |
29468 | 72 |
let |
73 |
fun apply NONE x = x |
|
29507 | 74 |
| apply (SOME id) x = |
75 |
let val entry = the_entry entries id |
|
76 |
in apply (#next entry) (f (id, entry) x) end; |
|
77 |
in if Symtab.defined entries id0 then apply (SOME id0) else I end; |
|
29468 | 78 |
|
34206 | 79 |
fun first_entry P (Document {entries, ...}) = |
29467 | 80 |
let |
29517 | 81 |
fun first _ NONE = NONE |
82 |
| first prev (SOME id) = |
|
29507 | 83 |
let val entry = the_entry entries id |
29519 | 84 |
in if P (id, entry) then SOME (prev, id, entry) else first (SOME id) (#next entry) end; |
34206 | 85 |
in first NONE (SOME no_id) end; |
29468 | 86 |
|
87 |
||
88 |
(* modify entries *) |
|
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
89 |
|
29484 | 90 |
fun insert_after (id: command_id) (id2: command_id) = map_entries (fn entries => |
91 |
let val {next, state} = the_entry entries id in |
|
92 |
entries |
|
93 |
|> put_entry (id, make_entry (SOME id2) state) |
|
94 |
|> put_entry (id2, make_entry next NONE) |
|
29467 | 95 |
end); |
96 |
||
29468 | 97 |
fun delete_after (id: command_id) = map_entries (fn entries => |
29484 | 98 |
let val {next, state} = the_entry entries id in |
99 |
(case next of |
|
100 |
NONE => error ("No next entry to delete: " ^ quote id) |
|
101 |
| SOME id2 => |
|
102 |
entries |> |
|
29467 | 103 |
(case #next (the_entry entries id2) of |
29484 | 104 |
NONE => put_entry (id, make_entry NONE state) |
29490 | 105 |
| SOME id3 => put_entry (id, make_entry (SOME id3) state) #> reset_entry_state id3)) |
29467 | 106 |
end); |
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
107 |
|
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
108 |
|
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
109 |
|
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
110 |
(** global configuration **) |
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
111 |
|
34206 | 112 |
(* states *) |
113 |
||
114 |
val empty_state = Future.value (SOME Toplevel.toplevel); |
|
115 |
||
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
116 |
local |
34206 | 117 |
|
34207
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
118 |
val global_states = Unsynchronized.ref (Symtab.make [(no_id, empty_state)]); |
34206 | 119 |
|
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
120 |
in |
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
121 |
|
34206 | 122 |
fun define_state (id: state_id) = |
34207
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
123 |
Unsynchronized.change global_states (Symtab.update_new (id, empty_state)) |
34206 | 124 |
handle Symtab.DUP dup => err_dup "state" dup; |
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
125 |
|
34206 | 126 |
fun put_state (id: state_id) state = |
34207
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
127 |
Unsynchronized.change global_states (Symtab.update (id, state)); |
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
128 |
|
34206 | 129 |
fun the_state (id: state_id) = |
34207
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
130 |
(case Symtab.lookup (! global_states) id of |
34206 | 131 |
NONE => err_undef "state" id |
132 |
| SOME state => state); |
|
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
133 |
|
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
134 |
end; |
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
135 |
|
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
136 |
|
34206 | 137 |
(* commands *) |
29520 | 138 |
|
34206 | 139 |
local |
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
140 |
|
34207
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
141 |
val global_commands = Unsynchronized.ref (Symtab.make [(no_id, Toplevel.empty)]); |
29520 | 142 |
|
34206 | 143 |
in |
29520 | 144 |
|
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
145 |
fun define_command id tr = |
34207
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
146 |
NAMED_CRITICAL "Isar" (fn () => |
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
147 |
Unsynchronized.change global_commands (Symtab.update_new (id, Toplevel.put_id id tr)) |
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
148 |
handle Symtab.DUP dup => err_dup "command" dup); |
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
149 |
|
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
150 |
fun the_command (id: command_id) = |
34207
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
151 |
(case Symtab.lookup (! global_commands) id of |
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
152 |
NONE => err_undef "command" id |
29468 | 153 |
| SOME tr => tr); |
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
154 |
|
34206 | 155 |
end; |
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
156 |
|
34206 | 157 |
|
158 |
(* documents *) |
|
159 |
||
160 |
local |
|
161 |
||
34207
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
162 |
val global_documents = Unsynchronized.ref (Symtab.empty: document Symtab.table); |
34206 | 163 |
|
164 |
in |
|
29520 | 165 |
|
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
166 |
fun define_document (id: document_id) document = |
34207
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
167 |
NAMED_CRITICAL "Isar" (fn () => |
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
168 |
Unsynchronized.change global_documents (Symtab.update_new (id, document)) |
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
169 |
handle Symtab.DUP dup => err_dup "document" dup); |
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
170 |
|
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
171 |
fun the_document (id: document_id) = |
34207
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
172 |
(case Symtab.lookup (! global_documents) id of |
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
173 |
NONE => err_undef "document" id |
29517 | 174 |
| SOME document => document); |
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
175 |
|
34206 | 176 |
end; |
177 |
||
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
178 |
|
29520 | 179 |
|
180 |
(** main operations **) |
|
181 |
||
29468 | 182 |
(* begin/end document *) |
29467 | 183 |
|
34206 | 184 |
val no_entries = Symtab.make [(no_id, make_entry NONE (SOME no_id))]; |
185 |
||
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
186 |
fun begin_document (id: document_id) path = |
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
187 |
let |
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
188 |
val (dir, name) = ThyLoad.split_thy_path path; |
34206 | 189 |
val _ = define_document id (make_document dir name no_entries); |
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
190 |
in () end; |
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
191 |
|
29519 | 192 |
fun end_document (id: document_id) = |
34207
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
193 |
NAMED_CRITICAL "Isar" (fn () => |
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
194 |
let |
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
195 |
val document as Document {name, ...} = the_document id; |
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
196 |
val end_state = |
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
197 |
the_state (the (#state (#3 (the |
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
198 |
(first_entry (fn (_, {next, ...}) => is_none next) document))))); |
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
199 |
val _ = |
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
200 |
Future.fork_deps [end_state] (fn () => |
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
201 |
(case Future.join end_state of |
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
202 |
SOME st => |
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
203 |
(Toplevel.run_command name (Toplevel.put_id id (Toplevel.commit_exit Position.none)) st; |
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
204 |
ThyInfo.touch_child_thys name; |
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
205 |
ThyInfo.register_thy name) |
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
206 |
| NONE => error ("Failed to finish theory " ^ quote name))); |
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
207 |
in () end); |
29468 | 208 |
|
209 |
||
210 |
(* document editing *) |
|
211 |
||
29507 | 212 |
local |
213 |
||
214 |
fun is_changed entries' (id, {next = _, state}) = |
|
215 |
(case try (the_entry entries') id of |
|
29517 | 216 |
NONE => true |
217 |
| SOME {next = _, state = state'} => state' <> state); |
|
29507 | 218 |
|
29517 | 219 |
fun new_state name (id, _) (state_id, updates) = |
29507 | 220 |
let |
34206 | 221 |
val state_id' = create_id (); |
29520 | 222 |
val _ = define_state state_id'; |
29517 | 223 |
val tr = Toplevel.put_id state_id' (the_command id); |
29520 | 224 |
fun make_state' () = |
225 |
let |
|
226 |
val state = the_state state_id; |
|
227 |
val state' = |
|
228 |
Future.fork_deps [state] (fn () => |
|
229 |
(case Future.join state of |
|
230 |
NONE => NONE |
|
231 |
| SOME st => Toplevel.run_command name tr st)); |
|
232 |
in put_state state_id' state' end; |
|
233 |
in (state_id', ((id, state_id'), make_state') :: updates) end; |
|
29468 | 234 |
|
34285
218fa4267718
always report updates -- required has "handshake";
wenzelm
parents:
34242
diff
changeset
|
235 |
fun report_updates updates = |
218fa4267718
always report updates -- required has "handshake";
wenzelm
parents:
34242
diff
changeset
|
236 |
implode (map (fn (id, state_id) => Markup.markup (Markup.edit id state_id) "") updates) |
218fa4267718
always report updates -- required has "handshake";
wenzelm
parents:
34242
diff
changeset
|
237 |
|> Markup.markup Markup.assign |
218fa4267718
always report updates -- required has "handshake";
wenzelm
parents:
34242
diff
changeset
|
238 |
|> Output.status; |
29489
5dfe03f423c4
edit_document: proper edits/edit markup, including the document id;
wenzelm
parents:
29487
diff
changeset
|
239 |
|
29507 | 240 |
in |
241 |
||
29520 | 242 |
fun edit_document (old_id: document_id) (new_id: document_id) edits = |
34207
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
243 |
NAMED_CRITICAL "Isar" (fn () => |
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
244 |
let |
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
245 |
val old_document as Document {name, entries = old_entries, ...} = the_document old_id; |
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
246 |
val new_document as Document {entries = new_entries, ...} = old_document |
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
247 |
|> fold (fn (id, SOME id2) => insert_after id id2 | (id, NONE) => delete_after id) edits; |
29520 | 248 |
|
34207
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
249 |
fun cancel_old id = fold_entries id |
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
250 |
(fn (_, {state = SOME state_id, ...}) => K (Future.cancel (the_state state_id)) | _ => K ()) |
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
251 |
old_document (); |
29520 | 252 |
|
34207
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
253 |
val (updates, new_document') = |
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
254 |
(case first_entry (is_changed old_entries) new_document of |
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
255 |
NONE => |
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
256 |
(case first_entry (is_changed new_entries) old_document of |
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
257 |
NONE => ([], new_document) |
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
258 |
| SOME (_, id, _) => (cancel_old id; ([], new_document))) |
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
259 |
| SOME (prev, id, _) => |
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
260 |
let |
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
261 |
val _ = cancel_old id; |
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
262 |
val prev_state_id = the (#state (the_entry new_entries (the prev))); |
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
263 |
val (_, updates) = fold_entries id (new_state name) new_document (prev_state_id, []); |
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
264 |
val new_document' = new_document |> map_entries (fold (set_entry_state o #1) updates); |
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
265 |
in (rev updates, new_document') end); |
29520 | 266 |
|
34207
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
267 |
val _ = define_document new_id new_document'; |
34212
8c3e1f73953d
eliminated Markup.edits/EDITS: Isar.edit_document reports Markup.edit/EDIT while running under new document id;
wenzelm
parents:
34207
diff
changeset
|
268 |
val _ = report_updates (map #1 updates); |
34207
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
269 |
val _ = List.app (fn (_, run) => run ()) updates; |
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
270 |
in () end); |
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
271 |
|
29507 | 272 |
end; |
273 |
||
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
274 |
|
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
275 |
|
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
276 |
(** concrete syntax **) |
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
277 |
|
36950 | 278 |
local structure V = ValueParse in |
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
279 |
|
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
280 |
val _ = |
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
281 |
OuterSyntax.internal_command "Isar.define_command" |
36950 | 282 |
(Parse.string -- Parse.string >> (fn (id, text) => |
32573 | 283 |
Toplevel.position (Position.id_only id) o |
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
284 |
Toplevel.imperative (fn () => |
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
285 |
define_command id (OuterSyntax.prepare_command (Position.id id) text)))); |
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
286 |
|
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
287 |
val _ = |
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
288 |
OuterSyntax.internal_command "Isar.begin_document" |
36950 | 289 |
(Parse.string -- Parse.string >> (fn (id, path) => |
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
290 |
Toplevel.imperative (fn () => begin_document id (Path.explode path)))); |
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
291 |
|
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
292 |
val _ = |
29468 | 293 |
OuterSyntax.internal_command "Isar.end_document" |
36950 | 294 |
(Parse.string >> (fn id => Toplevel.imperative (fn () => end_document id))); |
29468 | 295 |
|
296 |
val _ = |
|
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
297 |
OuterSyntax.internal_command "Isar.edit_document" |
36950 | 298 |
(Parse.string -- Parse.string -- |
299 |
V.list (Parse.string -- (Parse.string >> SOME) || Parse.string >> rpair NONE) |
|
34212
8c3e1f73953d
eliminated Markup.edits/EDITS: Isar.edit_document reports Markup.edit/EDIT while running under new document id;
wenzelm
parents:
34207
diff
changeset
|
300 |
>> (fn ((id, new_id), edits) => |
8c3e1f73953d
eliminated Markup.edits/EDITS: Isar.edit_document reports Markup.edit/EDIT while running under new document id;
wenzelm
parents:
34207
diff
changeset
|
301 |
Toplevel.position (Position.id_only new_id) o |
8c3e1f73953d
eliminated Markup.edits/EDITS: Isar.edit_document reports Markup.edit/EDIT while running under new document id;
wenzelm
parents:
34207
diff
changeset
|
302 |
Toplevel.imperative (fn () => edit_document id new_id edits))); |
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
303 |
|
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
304 |
end; |
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
305 |
|
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
306 |
end; |
29467 | 307 |