author | wenzelm |
Thu, 05 Aug 2010 14:35:35 +0200 | |
changeset 38150 | 67fc24df3721 |
parent 37953 | ddc3b72f9a42 |
child 38157 | d5d0af46f1ec |
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 |
|
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
4 |
Interactive Isar documents, which are structured as follows: |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
5 |
|
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
6 |
- history: tree of documents (i.e. changes without merge) |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
7 |
- document: graph of nodes (cf. theory files) |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
8 |
- node: linear set of commands, potentially with proof structure |
29459
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 |
|
34212
8c3e1f73953d
eliminated Markup.edits/EDITS: Isar.edit_document reports Markup.edit/EDIT while running under new document id;
wenzelm
parents:
34207
diff
changeset
|
11 |
structure Isar_Document: sig end = |
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
12 |
struct |
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
13 |
|
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
14 |
(* unique identifiers *) |
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
15 |
|
34206 | 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" ^ string_of_int i', i') end); |
|
24 |
end; |
|
29467 | 25 |
|
26 |
fun err_dup kind id = error ("Duplicate " ^ kind ^ ": " ^ quote id); |
|
34206 | 27 |
fun err_undef kind id = error ("Undefined " ^ kind ^ ": " ^ quote id); |
29467 | 28 |
|
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
29 |
|
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
30 |
|
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
31 |
(** documents **) |
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
32 |
|
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
33 |
datatype entry = Entry of {next: Document.command_id option, state: Document.state_id option}; |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
34 |
type node = entry Symtab.table; (*unique command entries indexed by command_id, start with no_id*) |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
35 |
type document = node Graph.T; (*development graph via static imports*) |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
36 |
|
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
37 |
|
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
38 |
(* command entries *) |
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
39 |
|
29484 | 40 |
fun make_entry next state = Entry {next = next, state = state}; |
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
41 |
|
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
42 |
fun the_entry (node: node) (id: Document.command_id) = |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
43 |
(case Symtab.lookup node id of |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
44 |
NONE => err_undef "command entry" id |
29467 | 45 |
| SOME (Entry entry) => entry); |
46 |
||
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
47 |
fun put_entry (id: Document.command_id, entry: entry) = Symtab.update (id, entry); |
29467 | 48 |
|
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
49 |
fun put_entry_state (id: Document.command_id) state (node: node) = |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
50 |
let val {next, ...} = the_entry node id |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
51 |
in put_entry (id, make_entry next state) node end; |
29489
5dfe03f423c4
edit_document: proper edits/edit markup, including the document id;
wenzelm
parents:
29487
diff
changeset
|
52 |
|
29490 | 53 |
fun reset_entry_state id = put_entry_state id NONE; |
54 |
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
|
55 |
|
5dfe03f423c4
edit_document: proper edits/edit markup, including the document id;
wenzelm
parents:
29487
diff
changeset
|
56 |
|
29484 | 57 |
(* iterate entries *) |
29468 | 58 |
|
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
59 |
fun fold_entries id0 f (node: node) = |
29468 | 60 |
let |
61 |
fun apply NONE x = x |
|
29507 | 62 |
| apply (SOME id) x = |
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
63 |
let val entry = the_entry node id |
29507 | 64 |
in apply (#next entry) (f (id, entry) x) end; |
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
65 |
in if Symtab.defined node id0 then apply (SOME id0) else I end; |
29468 | 66 |
|
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
67 |
fun first_entry P (node: node) = |
29467 | 68 |
let |
29517 | 69 |
fun first _ NONE = NONE |
70 |
| first prev (SOME id) = |
|
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
71 |
let val entry = the_entry node id |
29519 | 72 |
in if P (id, entry) then SOME (prev, id, entry) else first (SOME id) (#next entry) end; |
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
73 |
in first NONE (SOME Document.no_id) end; |
29468 | 74 |
|
75 |
||
76 |
(* modify entries *) |
|
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
77 |
|
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
78 |
fun insert_after (id: Document.command_id) (id2: Document.command_id) (node: node) = |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
79 |
let val {next, state} = the_entry node id in |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
80 |
node |
29484 | 81 |
|> put_entry (id, make_entry (SOME id2) state) |
82 |
|> put_entry (id2, make_entry next NONE) |
|
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
83 |
end; |
29467 | 84 |
|
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
85 |
fun delete_after (id: Document.command_id) (node: node) = |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
86 |
let val {next, state} = the_entry node id in |
29484 | 87 |
(case next of |
88 |
NONE => error ("No next entry to delete: " ^ quote id) |
|
89 |
| SOME id2 => |
|
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
90 |
node |> |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
91 |
(case #next (the_entry node id2) of |
29484 | 92 |
NONE => put_entry (id, make_entry NONE state) |
29490 | 93 |
| SOME id3 => put_entry (id, make_entry (SOME id3) state) #> reset_entry_state id3)) |
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
94 |
end; |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
95 |
|
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
96 |
|
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
97 |
(* node operations *) |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
98 |
|
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
99 |
val empty_node: node = Symtab.make [(Document.no_id, make_entry NONE (SOME Document.no_id))]; |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
100 |
|
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
101 |
fun the_node (document: document) name = |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
102 |
Graph.get_node document name handle Graph.UNDEF _ => empty_node; |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
103 |
|
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
104 |
fun edit_node (id, SOME id2) = insert_after id id2 |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
105 |
| edit_node (id, NONE) = delete_after id; |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
106 |
|
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
107 |
fun edit_nodes (name, NONE) = Graph.del_node name |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
108 |
| edit_nodes (name, SOME edits) = |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
109 |
Graph.default_node (name, empty_node) #> |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
110 |
Graph.map_node name (fold edit_node edits); |
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
111 |
|
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
112 |
|
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
113 |
|
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
114 |
(** global configuration **) |
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
115 |
|
34206 | 116 |
(* states *) |
117 |
||
37184
79fe8e753e84
define_state/new_state: provide state immediately, which is now lazy;
wenzelm
parents:
37148
diff
changeset
|
118 |
local |
34206 | 119 |
|
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
120 |
val global_states = |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
121 |
Unsynchronized.ref (Symtab.make [(Document.no_id, Lazy.value (SOME Toplevel.toplevel))]); |
37184
79fe8e753e84
define_state/new_state: provide state immediately, which is now lazy;
wenzelm
parents:
37148
diff
changeset
|
122 |
|
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
123 |
in |
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
124 |
|
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
125 |
fun define_state (id: Document.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
|
126 |
NAMED_CRITICAL "Isar" (fn () => |
37184
79fe8e753e84
define_state/new_state: provide state immediately, which is now lazy;
wenzelm
parents:
37148
diff
changeset
|
127 |
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
|
128 |
handle Symtab.DUP dup => err_dup "state" dup); |
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
129 |
|
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
130 |
fun the_state (id: Document.state_id) = |
34207
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
131 |
(case Symtab.lookup (! global_states) id of |
34206 | 132 |
NONE => err_undef "state" id |
133 |
| SOME state => state); |
|
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
134 |
|
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
135 |
end; |
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
136 |
|
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
137 |
|
34206 | 138 |
(* commands *) |
29520 | 139 |
|
34206 | 140 |
local |
37184
79fe8e753e84
define_state/new_state: provide state immediately, which is now lazy;
wenzelm
parents:
37148
diff
changeset
|
141 |
|
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
142 |
val global_commands = Unsynchronized.ref (Symtab.make [(Document.no_id, Toplevel.empty)]); |
37184
79fe8e753e84
define_state/new_state: provide state immediately, which is now lazy;
wenzelm
parents:
37148
diff
changeset
|
143 |
|
34206 | 144 |
in |
29520 | 145 |
|
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
146 |
fun define_command (id: Document.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
|
147 |
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
|
148 |
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
|
149 |
handle Symtab.DUP dup => err_dup "command" dup); |
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
150 |
|
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
151 |
fun the_command (id: Document.command_id) = |
34207
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
152 |
(case Symtab.lookup (! global_commands) id of |
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
153 |
NONE => err_undef "command" id |
29468 | 154 |
| SOME tr => tr); |
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
155 |
|
34206 | 156 |
end; |
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
157 |
|
34206 | 158 |
|
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
159 |
(* document versions *) |
34206 | 160 |
|
161 |
local |
|
37184
79fe8e753e84
define_state/new_state: provide state immediately, which is now lazy;
wenzelm
parents:
37148
diff
changeset
|
162 |
|
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
163 |
val global_documents = Unsynchronized.ref (Symtab.make [(Document.no_id, Graph.empty: document)]); |
37184
79fe8e753e84
define_state/new_state: provide state immediately, which is now lazy;
wenzelm
parents:
37148
diff
changeset
|
164 |
|
34206 | 165 |
in |
29520 | 166 |
|
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
167 |
fun define_document (id: Document.version_id) document = |
34207
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
168 |
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
|
169 |
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
|
170 |
handle Symtab.DUP dup => err_dup "document" dup); |
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
171 |
|
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
172 |
fun the_document (id: Document.version_id) = |
34207
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
173 |
(case Symtab.lookup (! global_documents) id of |
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
174 |
NONE => err_undef "document" id |
29517 | 175 |
| SOME document => document); |
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
176 |
|
34206 | 177 |
end; |
178 |
||
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
179 |
|
29520 | 180 |
|
181 |
(** main operations **) |
|
182 |
||
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
183 |
(* execution *) |
29468 | 184 |
|
29507 | 185 |
local |
186 |
||
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
187 |
val execution: unit future list Unsynchronized.ref = Unsynchronized.ref []; |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
188 |
|
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
189 |
fun force_state NONE = () |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
190 |
| force_state (SOME state_id) = ignore (Lazy.force (the_state state_id)); |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
191 |
|
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
192 |
in |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
193 |
|
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
194 |
fun execute document = |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
195 |
NAMED_CRITICAL "Isar" (fn () => |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
196 |
let |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
197 |
val old_execution = ! execution; |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
198 |
val _ = List.app Future.cancel old_execution; |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
199 |
fun await_cancellation () = uninterruptible (K Future.join_results) old_execution; |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
200 |
(* FIXME proper node deps *) |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
201 |
val new_execution = Graph.keys document |> map (fn name => |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
202 |
Future.fork_pri 1 (fn () => |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
203 |
let |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
204 |
val _ = await_cancellation (); |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
205 |
val exec = |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
206 |
fold_entries Document.no_id (fn (_, {state, ...}) => fn () => force_state state) |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
207 |
(the_node document name); |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
208 |
in exec () end)); |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
209 |
in execution := new_execution end); |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
210 |
|
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
211 |
end; |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
212 |
|
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
213 |
|
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
214 |
(* editing *) |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
215 |
|
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
216 |
local |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
217 |
|
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
218 |
fun is_changed node' (id, {next = _, state}) = |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
219 |
(case try (the_entry node') id of |
29517 | 220 |
NONE => true |
221 |
| SOME {next = _, state = state'} => state' <> state); |
|
29507 | 222 |
|
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
223 |
fun new_state name (id: Document.command_id) (state_id, updates) = |
29507 | 224 |
let |
37184
79fe8e753e84
define_state/new_state: provide state immediately, which is now lazy;
wenzelm
parents:
37148
diff
changeset
|
225 |
val state = the_state state_id; |
34206 | 226 |
val state_id' = create_id (); |
29517 | 227 |
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
|
228 |
val state' = |
79fe8e753e84
define_state/new_state: provide state immediately, which is now lazy;
wenzelm
parents:
37148
diff
changeset
|
229 |
Lazy.lazy (fn () => |
79fe8e753e84
define_state/new_state: provide state immediately, which is now lazy;
wenzelm
parents:
37148
diff
changeset
|
230 |
(case Lazy.force state of |
79fe8e753e84
define_state/new_state: provide state immediately, which is now lazy;
wenzelm
parents:
37148
diff
changeset
|
231 |
NONE => NONE |
79fe8e753e84
define_state/new_state: provide state immediately, which is now lazy;
wenzelm
parents:
37148
diff
changeset
|
232 |
| 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
|
233 |
val _ = define_state state_id' state'; |
79fe8e753e84
define_state/new_state: provide state immediately, which is now lazy;
wenzelm
parents:
37148
diff
changeset
|
234 |
in (state_id', (id, state_id') :: updates) end; |
29468 | 235 |
|
34285
218fa4267718
always report updates -- required has "handshake";
wenzelm
parents:
34242
diff
changeset
|
236 |
fun report_updates updates = |
218fa4267718
always report updates -- required has "handshake";
wenzelm
parents:
34242
diff
changeset
|
237 |
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
|
238 |
|> Markup.markup Markup.assign |
218fa4267718
always report updates -- required has "handshake";
wenzelm
parents:
34242
diff
changeset
|
239 |
|> Output.status; |
29489
5dfe03f423c4
edit_document: proper edits/edit markup, including the document id;
wenzelm
parents:
29487
diff
changeset
|
240 |
|
29507 | 241 |
in |
242 |
||
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
243 |
fun edit_document (old_id: Document.version_id) (new_id: Document.version_id) edits = |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
244 |
NAMED_CRITICAL "Isar" (fn () => exception_trace (fn () => |
34207
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
245 |
let |
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
246 |
val old_document = the_document old_id; |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
247 |
val new_document = fold edit_nodes edits old_document; |
29520 | 248 |
|
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
249 |
fun update_node name node = |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
250 |
(case first_entry (is_changed (the_node old_document name)) node of |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
251 |
NONE => ([], node) |
34207
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
252 |
| SOME (prev, id, _) => |
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
253 |
let |
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
254 |
val prev_state_id = the (#state (the_entry node (the prev))); |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
255 |
val (_, updates) = fold_entries id (new_state name o #1) node (prev_state_id, []); |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
256 |
val node' = fold set_entry_state updates node; |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
257 |
in (rev updates, node') end); |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
258 |
|
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
259 |
(* FIXME proper node deps *) |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
260 |
val (updatess, new_document') = |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
261 |
(Graph.keys new_document, new_document) |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
262 |
|-> fold_map (fn name => Graph.map_node_yield name (update_node name)); |
29520 | 263 |
|
34207
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
264 |
val _ = define_document new_id new_document'; |
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
265 |
val _ = report_updates (flat updatess); |
37184
79fe8e753e84
define_state/new_state: provide state immediately, which is now lazy;
wenzelm
parents:
37148
diff
changeset
|
266 |
val _ = execute new_document'; |
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
267 |
in () end)); |
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
268 |
|
29507 | 269 |
end; |
270 |
||
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
271 |
|
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
272 |
|
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
273 |
(** concrete syntax **) |
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 |
val _ = |
36953
2af1ad9aa1a3
renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents:
36951
diff
changeset
|
276 |
Outer_Syntax.internal_command "Isar.define_command" |
36950 | 277 |
(Parse.string -- Parse.string >> (fn (id, text) => |
32573 | 278 |
Toplevel.position (Position.id_only id) o |
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
279 |
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
|
280 |
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
|
281 |
|
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
282 |
val _ = |
36953
2af1ad9aa1a3
renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents:
36951
diff
changeset
|
283 |
Outer_Syntax.internal_command "Isar.edit_document" |
36950 | 284 |
(Parse.string -- Parse.string -- |
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
285 |
Parse_Value.list |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
286 |
(Parse.string -- Scan.option (Parse_Value.list (Parse.string -- Scan.option Parse.string))) |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
287 |
>> (fn ((old_id, new_id), edits) => |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
288 |
Toplevel.position (Position.id_only new_id) o |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
289 |
Toplevel.imperative (fn () => edit_document old_id new_id edits))); |
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
290 |
|
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
291 |
end; |
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
292 |