author | wenzelm |
Tue, 20 Jul 2010 20:10:27 +0200 | |
changeset 37857 | 4e4b8c0dc766 |
parent 37855 | 1ad8205078d4 |
child 37950 | bc285d91041e |
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 |
||
37184
79fe8e753e84
define_state/new_state: provide state immediately, which is now lazy;
wenzelm
parents:
37148
diff
changeset
|
114 |
local |
34206 | 115 |
|
37184
79fe8e753e84
define_state/new_state: provide state immediately, which is now lazy;
wenzelm
parents:
37148
diff
changeset
|
116 |
val global_states = Unsynchronized.ref (Symtab.make [(no_id, Lazy.value (SOME Toplevel.toplevel))]); |
79fe8e753e84
define_state/new_state: provide state immediately, which is now lazy;
wenzelm
parents:
37148
diff
changeset
|
117 |
|
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
118 |
in |
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
119 |
|
37184
79fe8e753e84
define_state/new_state: provide state immediately, which is now lazy;
wenzelm
parents:
37148
diff
changeset
|
120 |
fun define_state (id: state_id) state = |
37147
0c0ef115c7aa
further formal thread-safety (follow-up to 88300168baf8) -- in practice there is only a single Isar toplevel loop, but this is not enforced;
wenzelm
parents:
36953
diff
changeset
|
121 |
NAMED_CRITICAL "Isar" (fn () => |
37184
79fe8e753e84
define_state/new_state: provide state immediately, which is now lazy;
wenzelm
parents:
37148
diff
changeset
|
122 |
Unsynchronized.change global_states (Symtab.update_new (id, state)) |
37147
0c0ef115c7aa
further formal thread-safety (follow-up to 88300168baf8) -- in practice there is only a single Isar toplevel loop, but this is not enforced;
wenzelm
parents:
36953
diff
changeset
|
123 |
handle Symtab.DUP dup => err_dup "state" dup); |
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
124 |
|
34206 | 125 |
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
|
126 |
(case Symtab.lookup (! global_states) id of |
34206 | 127 |
NONE => err_undef "state" id |
128 |
| SOME state => state); |
|
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
129 |
|
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
130 |
end; |
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
131 |
|
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
132 |
|
34206 | 133 |
(* commands *) |
29520 | 134 |
|
34206 | 135 |
local |
37184
79fe8e753e84
define_state/new_state: provide state immediately, which is now lazy;
wenzelm
parents:
37148
diff
changeset
|
136 |
|
79fe8e753e84
define_state/new_state: provide state immediately, which is now lazy;
wenzelm
parents:
37148
diff
changeset
|
137 |
val global_commands = Unsynchronized.ref (Symtab.make [(no_id, Toplevel.empty)]); |
79fe8e753e84
define_state/new_state: provide state immediately, which is now lazy;
wenzelm
parents:
37148
diff
changeset
|
138 |
|
34206 | 139 |
in |
29520 | 140 |
|
37184
79fe8e753e84
define_state/new_state: provide state immediately, which is now lazy;
wenzelm
parents:
37148
diff
changeset
|
141 |
fun define_command (id: 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
|
142 |
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
|
143 |
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
|
144 |
handle Symtab.DUP dup => err_dup "command" dup); |
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
145 |
|
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
146 |
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
|
147 |
(case Symtab.lookup (! global_commands) id of |
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
148 |
NONE => err_undef "command" id |
29468 | 149 |
| SOME tr => tr); |
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
150 |
|
34206 | 151 |
end; |
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
152 |
|
34206 | 153 |
|
154 |
(* documents *) |
|
155 |
||
156 |
local |
|
37184
79fe8e753e84
define_state/new_state: provide state immediately, which is now lazy;
wenzelm
parents:
37148
diff
changeset
|
157 |
|
79fe8e753e84
define_state/new_state: provide state immediately, which is now lazy;
wenzelm
parents:
37148
diff
changeset
|
158 |
val global_documents = Unsynchronized.ref (Symtab.empty: document Symtab.table); |
79fe8e753e84
define_state/new_state: provide state immediately, which is now lazy;
wenzelm
parents:
37148
diff
changeset
|
159 |
|
34206 | 160 |
in |
29520 | 161 |
|
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
162 |
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
|
163 |
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
|
164 |
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
|
165 |
handle Symtab.DUP dup => err_dup "document" dup); |
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
166 |
|
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
167 |
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
|
168 |
(case Symtab.lookup (! global_documents) id of |
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
169 |
NONE => err_undef "document" id |
29517 | 170 |
| SOME document => document); |
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
171 |
|
34206 | 172 |
end; |
173 |
||
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
174 |
|
29520 | 175 |
|
176 |
(** main operations **) |
|
177 |
||
29468 | 178 |
(* begin/end document *) |
29467 | 179 |
|
34206 | 180 |
val no_entries = Symtab.make [(no_id, make_entry NONE (SOME no_id))]; |
181 |
||
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
182 |
fun begin_document (id: document_id) path = |
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
183 |
let |
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
37184
diff
changeset
|
184 |
val (dir, name) = Thy_Load.split_thy_path path; |
34206 | 185 |
val _ = define_document id (make_document dir name no_entries); |
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
186 |
in () end; |
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
187 |
|
29519 | 188 |
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
|
189 |
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
|
190 |
let |
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
191 |
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
|
192 |
val end_state = |
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
193 |
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
|
194 |
(first_entry (fn (_, {next, ...}) => is_none next) document))))); |
37148
d515609c88f7
substantial performance improvement by avoiding "re-ified" execution structure via future dependencies, instead use singleton execution (dummy future) that forces lazy state updates bottom-up;
wenzelm
parents:
37147
diff
changeset
|
195 |
val _ = (* FIXME regular execution (??) *) |
d515609c88f7
substantial performance improvement by avoiding "re-ified" execution structure via future dependencies, instead use singleton execution (dummy future) that forces lazy state updates bottom-up;
wenzelm
parents:
37147
diff
changeset
|
196 |
Future.fork (fn () => |
d515609c88f7
substantial performance improvement by avoiding "re-ified" execution structure via future dependencies, instead use singleton execution (dummy future) that forces lazy state updates bottom-up;
wenzelm
parents:
37147
diff
changeset
|
197 |
(case Lazy.force end_state of |
34207
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
198 |
SOME st => |
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
199 |
(Toplevel.run_command name (Toplevel.put_id id (Toplevel.commit_exit Position.none)) st; |
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
37184
diff
changeset
|
200 |
Thy_Info.touch_child_thys name; |
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
37184
diff
changeset
|
201 |
Thy_Info.register_thy name) |
34207
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
202 |
| 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
|
203 |
in () end); |
29468 | 204 |
|
205 |
||
206 |
(* document editing *) |
|
207 |
||
29507 | 208 |
local |
209 |
||
210 |
fun is_changed entries' (id, {next = _, state}) = |
|
211 |
(case try (the_entry entries') id of |
|
29517 | 212 |
NONE => true |
213 |
| SOME {next = _, state = state'} => state' <> state); |
|
29507 | 214 |
|
37184
79fe8e753e84
define_state/new_state: provide state immediately, which is now lazy;
wenzelm
parents:
37148
diff
changeset
|
215 |
fun new_state name (id: command_id) (state_id, updates) = |
29507 | 216 |
let |
37184
79fe8e753e84
define_state/new_state: provide state immediately, which is now lazy;
wenzelm
parents:
37148
diff
changeset
|
217 |
val state = the_state state_id; |
34206 | 218 |
val state_id' = create_id (); |
29517 | 219 |
val tr = Toplevel.put_id state_id' (the_command id); |
37184
79fe8e753e84
define_state/new_state: provide state immediately, which is now lazy;
wenzelm
parents:
37148
diff
changeset
|
220 |
val state' = |
79fe8e753e84
define_state/new_state: provide state immediately, which is now lazy;
wenzelm
parents:
37148
diff
changeset
|
221 |
Lazy.lazy (fn () => |
79fe8e753e84
define_state/new_state: provide state immediately, which is now lazy;
wenzelm
parents:
37148
diff
changeset
|
222 |
(case Lazy.force state of |
79fe8e753e84
define_state/new_state: provide state immediately, which is now lazy;
wenzelm
parents:
37148
diff
changeset
|
223 |
NONE => NONE |
79fe8e753e84
define_state/new_state: provide state immediately, which is now lazy;
wenzelm
parents:
37148
diff
changeset
|
224 |
| SOME st => Toplevel.run_command name tr st)); |
79fe8e753e84
define_state/new_state: provide state immediately, which is now lazy;
wenzelm
parents:
37148
diff
changeset
|
225 |
val _ = define_state state_id' state'; |
79fe8e753e84
define_state/new_state: provide state immediately, which is now lazy;
wenzelm
parents:
37148
diff
changeset
|
226 |
in (state_id', (id, state_id') :: updates) end; |
29468 | 227 |
|
34285
218fa4267718
always report updates -- required has "handshake";
wenzelm
parents:
34242
diff
changeset
|
228 |
fun report_updates updates = |
218fa4267718
always report updates -- required has "handshake";
wenzelm
parents:
34242
diff
changeset
|
229 |
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
|
230 |
|> Markup.markup Markup.assign |
218fa4267718
always report updates -- required has "handshake";
wenzelm
parents:
34242
diff
changeset
|
231 |
|> Output.status; |
29489
5dfe03f423c4
edit_document: proper edits/edit markup, including the document id;
wenzelm
parents:
29487
diff
changeset
|
232 |
|
37184
79fe8e753e84
define_state/new_state: provide state immediately, which is now lazy;
wenzelm
parents:
37148
diff
changeset
|
233 |
|
79fe8e753e84
define_state/new_state: provide state immediately, which is now lazy;
wenzelm
parents:
37148
diff
changeset
|
234 |
fun force_state NONE = () |
79fe8e753e84
define_state/new_state: provide state immediately, which is now lazy;
wenzelm
parents:
37148
diff
changeset
|
235 |
| force_state (SOME state_id) = ignore (Lazy.force (the_state state_id)); |
79fe8e753e84
define_state/new_state: provide state immediately, which is now lazy;
wenzelm
parents:
37148
diff
changeset
|
236 |
|
79fe8e753e84
define_state/new_state: provide state immediately, which is now lazy;
wenzelm
parents:
37148
diff
changeset
|
237 |
val execution = Unsynchronized.ref (Future.value ()); |
79fe8e753e84
define_state/new_state: provide state immediately, which is now lazy;
wenzelm
parents:
37148
diff
changeset
|
238 |
|
79fe8e753e84
define_state/new_state: provide state immediately, which is now lazy;
wenzelm
parents:
37148
diff
changeset
|
239 |
fun execute document = |
79fe8e753e84
define_state/new_state: provide state immediately, which is now lazy;
wenzelm
parents:
37148
diff
changeset
|
240 |
NAMED_CRITICAL "Isar" (fn () => |
79fe8e753e84
define_state/new_state: provide state immediately, which is now lazy;
wenzelm
parents:
37148
diff
changeset
|
241 |
let |
79fe8e753e84
define_state/new_state: provide state immediately, which is now lazy;
wenzelm
parents:
37148
diff
changeset
|
242 |
val old_execution = ! execution; |
79fe8e753e84
define_state/new_state: provide state immediately, which is now lazy;
wenzelm
parents:
37148
diff
changeset
|
243 |
val _ = Future.cancel old_execution; |
37857 | 244 |
val new_execution = Future.fork_pri 1 (fn () => |
37855
1ad8205078d4
edit_document: join parent execution in synchronous/uninterruptible mode, to prevent spurious interrupts when cascaded executions run into each other;
wenzelm
parents:
37216
diff
changeset
|
245 |
(uninterruptible (K Future.join_result) old_execution; |
37184
79fe8e753e84
define_state/new_state: provide state immediately, which is now lazy;
wenzelm
parents:
37148
diff
changeset
|
246 |
fold_entries no_id (fn (_, {state, ...}) => fn () => force_state state) document ())); |
79fe8e753e84
define_state/new_state: provide state immediately, which is now lazy;
wenzelm
parents:
37148
diff
changeset
|
247 |
in execution := new_execution end); |
79fe8e753e84
define_state/new_state: provide state immediately, which is now lazy;
wenzelm
parents:
37148
diff
changeset
|
248 |
|
29507 | 249 |
in |
250 |
||
29520 | 251 |
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
|
252 |
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
|
253 |
let |
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
254 |
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
|
255 |
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
|
256 |
|> fold (fn (id, SOME id2) => insert_after id id2 | (id, NONE) => delete_after id) edits; |
29520 | 257 |
|
34207
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
258 |
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
|
259 |
(case first_entry (is_changed old_entries) new_document of |
37148
d515609c88f7
substantial performance improvement by avoiding "re-ified" execution structure via future dependencies, instead use singleton execution (dummy future) that forces lazy state updates bottom-up;
wenzelm
parents:
37147
diff
changeset
|
260 |
NONE => ([], new_document) |
34207
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
261 |
| SOME (prev, id, _) => |
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
262 |
let |
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
263 |
val prev_state_id = the (#state (the_entry new_entries (the prev))); |
37184
79fe8e753e84
define_state/new_state: provide state immediately, which is now lazy;
wenzelm
parents:
37148
diff
changeset
|
264 |
val (_, updates) = |
79fe8e753e84
define_state/new_state: provide state immediately, which is now lazy;
wenzelm
parents:
37148
diff
changeset
|
265 |
fold_entries id (new_state name o #1) new_document (prev_state_id, []); |
79fe8e753e84
define_state/new_state: provide state immediately, which is now lazy;
wenzelm
parents:
37148
diff
changeset
|
266 |
val new_document' = new_document |> map_entries (fold set_entry_state updates); |
34207
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
267 |
in (rev updates, new_document') end); |
29520 | 268 |
|
34207
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
269 |
val _ = define_document new_id new_document'; |
37184
79fe8e753e84
define_state/new_state: provide state immediately, which is now lazy;
wenzelm
parents:
37148
diff
changeset
|
270 |
val _ = report_updates updates; |
79fe8e753e84
define_state/new_state: provide state immediately, which is now lazy;
wenzelm
parents:
37148
diff
changeset
|
271 |
val _ = execute new_document'; |
34207
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
272 |
in () end); |
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
273 |
|
29507 | 274 |
end; |
275 |
||
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
276 |
|
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
277 |
|
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
278 |
(** concrete syntax **) |
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 _ = |
36953
2af1ad9aa1a3
renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents:
36951
diff
changeset
|
281 |
Outer_Syntax.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 () => |
36953
2af1ad9aa1a3
renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents:
36951
diff
changeset
|
285 |
define_command id (Outer_Syntax.prepare_command (Position.id id) text)))); |
29459
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 _ = |
36953
2af1ad9aa1a3
renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents:
36951
diff
changeset
|
288 |
Outer_Syntax.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 _ = |
36953
2af1ad9aa1a3
renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents:
36951
diff
changeset
|
293 |
Outer_Syntax.internal_command "Isar.end_document" |
36950 | 294 |
(Parse.string >> (fn id => Toplevel.imperative (fn () => end_document id))); |
29468 | 295 |
|
296 |
val _ = |
|
36953
2af1ad9aa1a3
renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents:
36951
diff
changeset
|
297 |
Outer_Syntax.internal_command "Isar.edit_document" |
36950 | 298 |
(Parse.string -- Parse.string -- |
36951 | 299 |
Parse_Value.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 |