author | wenzelm |
Mon, 15 Aug 2011 19:27:55 +0200 | |
changeset 44198 | a41ea419de68 |
parent 44197 | 458573968568 |
child 44199 | e38885e3ea60 |
permissions | -rw-r--r-- |
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/PIDE/document.ML |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset
|
3 |
|
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset
|
4 |
Document as collection of named nodes, each consisting of an editable |
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
5 |
list of commands, associated with asynchronous execution process. |
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset
|
6 |
*) |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset
|
7 |
|
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset
|
8 |
signature DOCUMENT = |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset
|
9 |
sig |
38363
af7f41a8a0a8
clarified "state" (accumulated data) vs. "exec" (execution that produces data);
wenzelm
parents:
38355
diff
changeset
|
10 |
type id = int |
38373 | 11 |
type version_id = id |
38363
af7f41a8a0a8
clarified "state" (accumulated data) vs. "exec" (execution that produces data);
wenzelm
parents:
38355
diff
changeset
|
12 |
type command_id = id |
38373 | 13 |
type exec_id = id |
38363
af7f41a8a0a8
clarified "state" (accumulated data) vs. "exec" (execution that produces data);
wenzelm
parents:
38355
diff
changeset
|
14 |
val no_id: id |
38419 | 15 |
val new_id: unit -> id |
38363
af7f41a8a0a8
clarified "state" (accumulated data) vs. "exec" (execution that produces data);
wenzelm
parents:
38355
diff
changeset
|
16 |
val parse_id: string -> id |
af7f41a8a0a8
clarified "state" (accumulated data) vs. "exec" (execution that produces data);
wenzelm
parents:
38355
diff
changeset
|
17 |
val print_id: id -> string |
44185 | 18 |
type node_header = (string * string list * (string * bool) list) Exn.result |
44157
a21d3e1e64fd
uniform treatment of header edits as document edits;
wenzelm
parents:
44156
diff
changeset
|
19 |
datatype node_edit = |
44185 | 20 |
Clear | |
44157
a21d3e1e64fd
uniform treatment of header edits as document edits;
wenzelm
parents:
44156
diff
changeset
|
21 |
Edits of (command_id option * command_id option) list | |
44182 | 22 |
Header of node_header |
44156 | 23 |
type edit = string * node_edit |
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
24 |
type state |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
25 |
val init_state: state |
44197
458573968568
refined Document.edit: less stateful update via Graph.schedule;
wenzelm
parents:
44196
diff
changeset
|
26 |
val join_commands: state -> unit |
43666 | 27 |
val cancel_execution: state -> unit -> unit |
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
28 |
val define_command: command_id -> string -> state -> state |
44157
a21d3e1e64fd
uniform treatment of header edits as document edits;
wenzelm
parents:
44156
diff
changeset
|
29 |
val edit: version_id -> version_id -> edit list -> state -> (command_id * exec_id) list * state |
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
30 |
val execute: version_id -> state -> state |
43713
1ba5331b4623
moved global state to structure Document (again);
wenzelm
parents:
43668
diff
changeset
|
31 |
val state: unit -> state |
1ba5331b4623
moved global state to structure Document (again);
wenzelm
parents:
43668
diff
changeset
|
32 |
val change_state: (state -> state) -> unit |
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset
|
33 |
end; |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset
|
34 |
|
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset
|
35 |
structure Document: DOCUMENT = |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset
|
36 |
struct |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset
|
37 |
|
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset
|
38 |
(* unique identifiers *) |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset
|
39 |
|
38363
af7f41a8a0a8
clarified "state" (accumulated data) vs. "exec" (execution that produces data);
wenzelm
parents:
38355
diff
changeset
|
40 |
type id = int; |
38373 | 41 |
type version_id = id; |
38363
af7f41a8a0a8
clarified "state" (accumulated data) vs. "exec" (execution that produces data);
wenzelm
parents:
38355
diff
changeset
|
42 |
type command_id = id; |
38373 | 43 |
type exec_id = id; |
38355
8cb265fb12fe
represent document ids by (long) int, to benefit from the somewhat faster Inttab in ML (LinearSet in Scala is invariably indexed by native object ids);
wenzelm
parents:
38150
diff
changeset
|
44 |
|
8cb265fb12fe
represent document ids by (long) int, to benefit from the somewhat faster Inttab in ML (LinearSet in Scala is invariably indexed by native object ids);
wenzelm
parents:
38150
diff
changeset
|
45 |
val no_id = 0; |
40449 | 46 |
val new_id = Synchronized.counter (); |
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
47 |
|
38414
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38373
diff
changeset
|
48 |
val parse_id = Markup.parse_int; |
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38373
diff
changeset
|
49 |
val print_id = Markup.print_int; |
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset
|
50 |
|
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
51 |
fun err_dup kind id = error ("Duplicate " ^ kind ^ ": " ^ print_id id); |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
52 |
fun err_undef kind id = error ("Undefined " ^ kind ^ ": " ^ print_id id); |
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset
|
53 |
|
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
54 |
|
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
55 |
|
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
56 |
(** document structure **) |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
57 |
|
44185 | 58 |
type node_header = (string * string list * (string * bool) list) Exn.result; |
38448
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38421
diff
changeset
|
59 |
structure Entries = Linear_Set(type key = command_id val ord = int_ord); |
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38421
diff
changeset
|
60 |
|
43668 | 61 |
abstype node = Node of |
44182 | 62 |
{header: node_header, |
44180 | 63 |
entries: exec_id option Entries.T, (*command entries with excecutions*) |
44197
458573968568
refined Document.edit: less stateful update via Graph.schedule;
wenzelm
parents:
44196
diff
changeset
|
64 |
result: Toplevel.state lazy} |
43668 | 65 |
and version = Version of node Graph.T (*development graph wrt. static imports*) |
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
66 |
with |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
67 |
|
44197
458573968568
refined Document.edit: less stateful update via Graph.schedule;
wenzelm
parents:
44196
diff
changeset
|
68 |
fun make_node (header, entries, result) = |
458573968568
refined Document.edit: less stateful update via Graph.schedule;
wenzelm
parents:
44196
diff
changeset
|
69 |
Node {header = header, entries = entries, result = result}; |
43668 | 70 |
|
44197
458573968568
refined Document.edit: less stateful update via Graph.schedule;
wenzelm
parents:
44196
diff
changeset
|
71 |
fun map_node f (Node {header, entries, result}) = |
458573968568
refined Document.edit: less stateful update via Graph.schedule;
wenzelm
parents:
44196
diff
changeset
|
72 |
make_node (f (header, entries, result)); |
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
73 |
|
44180 | 74 |
fun get_header (Node {header, ...}) = header; |
44197
458573968568
refined Document.edit: less stateful update via Graph.schedule;
wenzelm
parents:
44196
diff
changeset
|
75 |
fun set_header header = map_node (fn (_, entries, result) => (header, entries, result)); |
44180 | 76 |
|
44197
458573968568
refined Document.edit: less stateful update via Graph.schedule;
wenzelm
parents:
44196
diff
changeset
|
77 |
fun map_entries f (Node {header, entries, result}) = make_node (header, f entries, result); |
43668 | 78 |
fun fold_entries start f (Node {entries, ...}) = Entries.fold start f entries; |
79 |
fun first_entry start P (Node {entries, ...}) = Entries.get_first start P entries; |
|
80 |
||
44198 | 81 |
fun get_theory pos (Node {result, ...}) = Toplevel.end_theory pos (Lazy.get_finished result); |
44197
458573968568
refined Document.edit: less stateful update via Graph.schedule;
wenzelm
parents:
44196
diff
changeset
|
82 |
fun set_result result = map_node (fn (header, entries, _) => (header, entries, result)); |
44180 | 83 |
|
44197
458573968568
refined Document.edit: less stateful update via Graph.schedule;
wenzelm
parents:
44196
diff
changeset
|
84 |
val empty_exec = Lazy.value Toplevel.toplevel; |
458573968568
refined Document.edit: less stateful update via Graph.schedule;
wenzelm
parents:
44196
diff
changeset
|
85 |
val empty_node = make_node (Exn.Exn (ERROR "Bad theory header"), Entries.empty, empty_exec); |
458573968568
refined Document.edit: less stateful update via Graph.schedule;
wenzelm
parents:
44196
diff
changeset
|
86 |
val clear_node = map_node (fn (header, _, _) => (header, Entries.empty, empty_exec)); |
44185 | 87 |
|
88 |
fun get_node nodes name = Graph.get_node nodes name handle Graph.UNDEF _ => empty_node; |
|
89 |
fun remove_node name nodes = Graph.del_node name nodes handle Graph.UNDEF _ => nodes; |
|
90 |
fun update_node name f = Graph.default_node (name, empty_node) #> Graph.map_node name f; |
|
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
91 |
|
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
92 |
|
38448
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38421
diff
changeset
|
93 |
(* node edits and associated executions *) |
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset
|
94 |
|
44157
a21d3e1e64fd
uniform treatment of header edits as document edits;
wenzelm
parents:
44156
diff
changeset
|
95 |
datatype node_edit = |
44185 | 96 |
Clear | |
44157
a21d3e1e64fd
uniform treatment of header edits as document edits;
wenzelm
parents:
44156
diff
changeset
|
97 |
Edits of (command_id option * command_id option) list | |
44182 | 98 |
Header of node_header; |
44157
a21d3e1e64fd
uniform treatment of header edits as document edits;
wenzelm
parents:
44156
diff
changeset
|
99 |
|
44156 | 100 |
type edit = string * node_edit; |
38448
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38421
diff
changeset
|
101 |
|
43668 | 102 |
fun the_entry (Node {entries, ...}) id = |
38448
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38421
diff
changeset
|
103 |
(case Entries.lookup entries id of |
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38421
diff
changeset
|
104 |
NONE => err_undef "command entry" id |
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38421
diff
changeset
|
105 |
| SOME entry => entry); |
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset
|
106 |
|
43668 | 107 |
fun update_entry (id, exec_id) = |
108 |
map_entries (Entries.update (id, SOME exec_id)); |
|
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
109 |
|
38448
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38421
diff
changeset
|
110 |
fun reset_after id entries = |
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38421
diff
changeset
|
111 |
(case Entries.get_after entries id of |
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38421
diff
changeset
|
112 |
NONE => entries |
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38421
diff
changeset
|
113 |
| SOME next => Entries.update (next, NONE) entries); |
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38421
diff
changeset
|
114 |
|
43668 | 115 |
val edit_node = map_entries o fold |
116 |
(fn (id, SOME id2) => Entries.insert_after id (id2, NONE) |
|
117 |
| (id, NONE) => Entries.delete_after id #> reset_after id); |
|
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
118 |
|
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
119 |
|
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
120 |
(* version operations *) |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
121 |
|
44185 | 122 |
val empty_version = Version Graph.empty; |
123 |
||
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
124 |
fun nodes_of (Version nodes) = nodes; |
44185 | 125 |
val node_of = get_node o nodes_of; |
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
126 |
val node_names_of = Graph.keys o nodes_of; |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
127 |
|
44185 | 128 |
fun cycle_msg names = "Cyclic dependency of " ^ space_implode " via " (map quote names); |
44180 | 129 |
|
44157
a21d3e1e64fd
uniform treatment of header edits as document edits;
wenzelm
parents:
44156
diff
changeset
|
130 |
fun edit_nodes (name, node_edit) (Version nodes) = |
a21d3e1e64fd
uniform treatment of header edits as document edits;
wenzelm
parents:
44156
diff
changeset
|
131 |
Version |
a21d3e1e64fd
uniform treatment of header edits as document edits;
wenzelm
parents:
44156
diff
changeset
|
132 |
(case node_edit of |
44185 | 133 |
Clear => update_node name clear_node nodes |
44180 | 134 |
| Edits edits => update_node name (edit_node edits) nodes |
44185 | 135 |
| Header header => |
136 |
let |
|
137 |
val node = get_node nodes name; |
|
138 |
val nodes' = Graph.new_node (name, node) (remove_node name nodes); |
|
139 |
val parents = |
|
140 |
(case header of Exn.Res (_, parents, _) => parents | _ => []) |
|
141 |
|> filter (can (Graph.get_node nodes')); |
|
142 |
val (header', nodes'') = |
|
143 |
(header, Graph.add_deps_acyclic (name, parents) nodes') |
|
144 |
handle Graph.CYCLES cs => (Exn.Exn (ERROR (cat_lines (map cycle_msg cs))), nodes'); |
|
145 |
in Graph.map_node name (set_header header') nodes'' end); |
|
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
146 |
|
44197
458573968568
refined Document.edit: less stateful update via Graph.schedule;
wenzelm
parents:
44196
diff
changeset
|
147 |
fun put_node (name, node) (Version nodes) = |
40481 | 148 |
Version (nodes |
149 |
|> Graph.default_node (name, empty_node) |
|
150 |
|> Graph.map_node name (K node)); |
|
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
151 |
|
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset
|
152 |
end; |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset
|
153 |
|
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
154 |
|
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
155 |
|
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
156 |
(** global state -- document structure and execution process **) |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
157 |
|
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
158 |
abstype state = State of |
40398 | 159 |
{versions: version Inttab.table, (*version_id -> document content*) |
38421
6cfc6fce7bfb
document commands: maintain transition as future (wrt. potentially slow Outer_Syntax.prepare_command), refrain from second Toplevel.put_id;
wenzelm
parents:
38419
diff
changeset
|
160 |
commands: Toplevel.transition future Inttab.table, (*command_id -> transition (future parsing)*) |
44196 | 161 |
execs: Toplevel.state lazy Inttab.table, (*exec_id -> execution process*) |
40398 | 162 |
execution: unit future list} (*global execution process*) |
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
163 |
with |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
164 |
|
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
165 |
fun make_state (versions, commands, execs, execution) = |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
166 |
State {versions = versions, commands = commands, execs = execs, execution = execution}; |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
167 |
|
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
168 |
fun map_state f (State {versions, commands, execs, execution}) = |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
169 |
make_state (f (versions, commands, execs, execution)); |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
170 |
|
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
171 |
val init_state = |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
172 |
make_state (Inttab.make [(no_id, empty_version)], |
38449 | 173 |
Inttab.make [(no_id, Future.value Toplevel.empty)], |
44197
458573968568
refined Document.edit: less stateful update via Graph.schedule;
wenzelm
parents:
44196
diff
changeset
|
174 |
Inttab.make [(no_id, empty_exec)], |
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
175 |
[]); |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
176 |
|
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
177 |
|
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
178 |
(* document versions *) |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
179 |
|
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
180 |
fun define_version (id: version_id) version = |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
181 |
map_state (fn (versions, commands, execs, execution) => |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
182 |
let val versions' = Inttab.update_new (id, version) versions |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
183 |
handle Inttab.DUP dup => err_dup "document version" dup |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
184 |
in (versions', commands, execs, execution) end); |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
185 |
|
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
186 |
fun the_version (State {versions, ...}) (id: version_id) = |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
187 |
(case Inttab.lookup versions id of |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
188 |
NONE => err_undef "document version" id |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
189 |
| SOME version => version); |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
190 |
|
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
191 |
|
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
192 |
(* commands *) |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
193 |
|
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
194 |
fun define_command (id: command_id) text = |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
195 |
map_state (fn (versions, commands, execs, execution) => |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
196 |
let |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
197 |
val id_string = print_id id; |
38421
6cfc6fce7bfb
document commands: maintain transition as future (wrt. potentially slow Outer_Syntax.prepare_command), refrain from second Toplevel.put_id;
wenzelm
parents:
38419
diff
changeset
|
198 |
val tr = Future.fork_pri 2 (fn () => |
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
199 |
Position.setmp_thread_data (Position.id_only id_string) |
38421
6cfc6fce7bfb
document commands: maintain transition as future (wrt. potentially slow Outer_Syntax.prepare_command), refrain from second Toplevel.put_id;
wenzelm
parents:
38419
diff
changeset
|
200 |
(fn () => Outer_Syntax.prepare_command (Position.id id_string) text) ()); |
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
201 |
val commands' = |
38421
6cfc6fce7bfb
document commands: maintain transition as future (wrt. potentially slow Outer_Syntax.prepare_command), refrain from second Toplevel.put_id;
wenzelm
parents:
38419
diff
changeset
|
202 |
Inttab.update_new (id, tr) commands |
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
203 |
handle Inttab.DUP dup => err_dup "command" dup; |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
204 |
in (versions, commands', execs, execution) end); |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
205 |
|
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
206 |
fun the_command (State {commands, ...}) (id: command_id) = |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
207 |
(case Inttab.lookup commands id of |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
208 |
NONE => err_undef "command" id |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
209 |
| SOME tr => tr); |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
210 |
|
38421
6cfc6fce7bfb
document commands: maintain transition as future (wrt. potentially slow Outer_Syntax.prepare_command), refrain from second Toplevel.put_id;
wenzelm
parents:
38419
diff
changeset
|
211 |
fun join_commands (State {commands, ...}) = |
6cfc6fce7bfb
document commands: maintain transition as future (wrt. potentially slow Outer_Syntax.prepare_command), refrain from second Toplevel.put_id;
wenzelm
parents:
38419
diff
changeset
|
212 |
Inttab.fold (fn (_, tr) => fn () => ignore (Future.join_result tr)) commands (); |
6cfc6fce7bfb
document commands: maintain transition as future (wrt. potentially slow Outer_Syntax.prepare_command), refrain from second Toplevel.put_id;
wenzelm
parents:
38419
diff
changeset
|
213 |
|
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
214 |
|
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
215 |
(* command executions *) |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
216 |
|
44197
458573968568
refined Document.edit: less stateful update via Graph.schedule;
wenzelm
parents:
44196
diff
changeset
|
217 |
fun define_exec (exec_id, exec) = |
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
218 |
map_state (fn (versions, commands, execs, execution) => |
44197
458573968568
refined Document.edit: less stateful update via Graph.schedule;
wenzelm
parents:
44196
diff
changeset
|
219 |
let val execs' = Inttab.update_new (exec_id, exec) execs |
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
220 |
handle Inttab.DUP dup => err_dup "command execution" dup |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
221 |
in (versions, commands, execs', execution) end); |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
222 |
|
44197
458573968568
refined Document.edit: less stateful update via Graph.schedule;
wenzelm
parents:
44196
diff
changeset
|
223 |
fun the_exec (State {execs, ...}) exec_id = |
458573968568
refined Document.edit: less stateful update via Graph.schedule;
wenzelm
parents:
44196
diff
changeset
|
224 |
(case Inttab.lookup execs exec_id of |
458573968568
refined Document.edit: less stateful update via Graph.schedule;
wenzelm
parents:
44196
diff
changeset
|
225 |
NONE => err_undef "command execution" exec_id |
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
226 |
| SOME exec => exec); |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
227 |
|
41634
28d94383249c
cancel document execution before editing, to improve reactivity on systems with few cores;
wenzelm
parents:
41630
diff
changeset
|
228 |
|
28d94383249c
cancel document execution before editing, to improve reactivity on systems with few cores;
wenzelm
parents:
41630
diff
changeset
|
229 |
(* document execution *) |
28d94383249c
cancel document execution before editing, to improve reactivity on systems with few cores;
wenzelm
parents:
41630
diff
changeset
|
230 |
|
43666 | 231 |
fun cancel_execution (State {execution, ...}) = |
232 |
(List.app Future.cancel execution; |
|
233 |
fn () => ignore (Future.join_results execution)); |
|
41634
28d94383249c
cancel document execution before editing, to improve reactivity on systems with few cores;
wenzelm
parents:
41630
diff
changeset
|
234 |
|
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
235 |
end; |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
236 |
|
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
237 |
|
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
238 |
|
38888
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38873
diff
changeset
|
239 |
(* toplevel transactions *) |
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38873
diff
changeset
|
240 |
|
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38873
diff
changeset
|
241 |
local |
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38873
diff
changeset
|
242 |
|
40391
b0dafbfc05b7
explicit "timing" status for toplevel transactions;
wenzelm
parents:
40390
diff
changeset
|
243 |
fun timing tr t = Toplevel.status tr (Markup.timing t); |
b0dafbfc05b7
explicit "timing" status for toplevel transactions;
wenzelm
parents:
40390
diff
changeset
|
244 |
|
38888
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38873
diff
changeset
|
245 |
fun proof_status tr st = |
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38873
diff
changeset
|
246 |
(case try Toplevel.proof_of st of |
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38873
diff
changeset
|
247 |
SOME prf => Toplevel.status tr (Proof.status_markup prf) |
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38873
diff
changeset
|
248 |
| NONE => ()); |
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38873
diff
changeset
|
249 |
|
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38873
diff
changeset
|
250 |
fun async_state tr st = |
40534
9e196062bf88
clarified interact/print state: proof commands are treated as in TTY mode to get full response;
wenzelm
parents:
40532
diff
changeset
|
251 |
ignore |
41673 | 252 |
(singleton |
41674 | 253 |
(Future.forks {name = "Document.async_state", |
44113 | 254 |
group = SOME (Task_Queue.new_group NONE), deps = [], pri = 0, interrupts = true}) |
40534
9e196062bf88
clarified interact/print state: proof commands are treated as in TTY mode to get full response;
wenzelm
parents:
40532
diff
changeset
|
255 |
(fn () => |
9e196062bf88
clarified interact/print state: proof commands are treated as in TTY mode to get full response;
wenzelm
parents:
40532
diff
changeset
|
256 |
Toplevel.setmp_thread_position tr |
9e196062bf88
clarified interact/print state: proof commands are treated as in TTY mode to get full response;
wenzelm
parents:
40532
diff
changeset
|
257 |
(fn () => Toplevel.print_state false st) ())); |
38888
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38873
diff
changeset
|
258 |
|
40390 | 259 |
fun run int tr st = |
260 |
(case Toplevel.transition int tr st of |
|
261 |
SOME (st', NONE) => ([], SOME st') |
|
262 |
| SOME (_, SOME exn_info) => |
|
263 |
(case ML_Compiler.exn_messages (Runtime.EXCURSION_FAIL exn_info) of |
|
264 |
[] => Exn.interrupt () |
|
265 |
| errs => (errs, NONE)) |
|
266 |
| NONE => ([ML_Compiler.exn_message Runtime.TERMINATE], NONE)); |
|
267 |
||
38888
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38873
diff
changeset
|
268 |
in |
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38873
diff
changeset
|
269 |
|
44185 | 270 |
fun run_command (node_name, node_header) raw_tr st = |
271 |
let |
|
272 |
val is_init = Toplevel.is_init raw_tr; |
|
273 |
val tr = |
|
274 |
if is_init then |
|
44186
806f0ec1a43d
simplified Toplevel.init_theory: discontinued special master argument;
wenzelm
parents:
44185
diff
changeset
|
275 |
raw_tr |> Toplevel.modify_init (fn () => |
44185 | 276 |
let |
277 |
(* FIXME get theories from document state *) |
|
278 |
(* FIXME provide files via Scala layer *) |
|
279 |
val (name, imports, uses) = Exn.release node_header; |
|
44186
806f0ec1a43d
simplified Toplevel.init_theory: discontinued special master argument;
wenzelm
parents:
44185
diff
changeset
|
280 |
val master = Path.dir (Path.explode node_name); |
44185 | 281 |
in Thy_Info.toplevel_begin_theory master name imports (map (apfst Path.explode) uses) end) |
282 |
else raw_tr; |
|
40534
9e196062bf88
clarified interact/print state: proof commands are treated as in TTY mode to get full response;
wenzelm
parents:
40532
diff
changeset
|
283 |
|
44185 | 284 |
val is_proof = Keyword.is_proof (Toplevel.name_of tr); |
285 |
val do_print = not is_init andalso (Toplevel.print_of tr orelse is_proof); |
|
286 |
||
287 |
val start = Timing.start (); |
|
288 |
val (errs, result) = |
|
289 |
if Toplevel.is_toplevel st andalso not is_init then ([], SOME st) |
|
290 |
else run (is_init orelse is_proof) (Toplevel.set_print false tr) st; |
|
291 |
val _ = timing tr (Timing.result start); |
|
292 |
val _ = List.app (Toplevel.error_msg tr) errs; |
|
293 |
in |
|
294 |
(case result of |
|
44196 | 295 |
NONE => (Toplevel.status tr Markup.failed; st) |
44185 | 296 |
| SOME st' => |
297 |
(Toplevel.status tr Markup.finished; |
|
298 |
proof_status tr st'; |
|
299 |
if do_print then async_state tr st' else (); |
|
44196 | 300 |
st')) |
44185 | 301 |
end; |
38888
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38873
diff
changeset
|
302 |
|
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38873
diff
changeset
|
303 |
end; |
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38873
diff
changeset
|
304 |
|
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38873
diff
changeset
|
305 |
|
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38873
diff
changeset
|
306 |
|
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38873
diff
changeset
|
307 |
|
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
308 |
(** editing **) |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
309 |
|
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
310 |
(* edit *) |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
311 |
|
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
312 |
local |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
313 |
|
38448
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38421
diff
changeset
|
314 |
fun is_changed node' ((_, id), exec) = |
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
315 |
(case try (the_entry node') id of |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
316 |
NONE => true |
38448
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38421
diff
changeset
|
317 |
| SOME exec' => exec' <> exec); |
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
318 |
|
44197
458573968568
refined Document.edit: less stateful update via Graph.schedule;
wenzelm
parents:
44196
diff
changeset
|
319 |
fun new_exec node_info (command, command_id) (assigns, execs, exec) = |
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
320 |
let |
38419 | 321 |
val exec_id' = new_id (); |
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
322 |
val exec' = |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
323 |
Lazy.lazy (fn () => |
40398 | 324 |
let |
44198 | 325 |
val tr = Toplevel.put_id (print_id exec_id') (Future.get_finished command); |
326 |
val st = Lazy.get_finished exec; |
|
44197
458573968568
refined Document.edit: less stateful update via Graph.schedule;
wenzelm
parents:
44196
diff
changeset
|
327 |
in run_command node_info tr st end); |
458573968568
refined Document.edit: less stateful update via Graph.schedule;
wenzelm
parents:
44196
diff
changeset
|
328 |
in ((command_id, exec_id') :: assigns, (exec_id', exec') :: execs, exec') end; |
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
329 |
|
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
330 |
in |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
331 |
|
44157
a21d3e1e64fd
uniform treatment of header edits as document edits;
wenzelm
parents:
44156
diff
changeset
|
332 |
fun edit (old_id: version_id) (new_id: version_id) edits state = |
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
333 |
let |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
334 |
val old_version = the_version state old_id; |
44180 | 335 |
val _ = Time.now (); (* FIXME odd workaround for polyml-5.4.0/x86_64 *) |
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
336 |
val new_version = fold edit_nodes edits old_version; |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
337 |
|
44197
458573968568
refined Document.edit: less stateful update via Graph.schedule;
wenzelm
parents:
44196
diff
changeset
|
338 |
(* FIXME futures *) |
458573968568
refined Document.edit: less stateful update via Graph.schedule;
wenzelm
parents:
44196
diff
changeset
|
339 |
val updates = |
458573968568
refined Document.edit: less stateful update via Graph.schedule;
wenzelm
parents:
44196
diff
changeset
|
340 |
nodes_of new_version |> Graph.schedule |
458573968568
refined Document.edit: less stateful update via Graph.schedule;
wenzelm
parents:
44196
diff
changeset
|
341 |
(fn _ => fn (name, node) => |
458573968568
refined Document.edit: less stateful update via Graph.schedule;
wenzelm
parents:
44196
diff
changeset
|
342 |
(case first_entry NONE (is_changed (node_of old_version name)) node of |
458573968568
refined Document.edit: less stateful update via Graph.schedule;
wenzelm
parents:
44196
diff
changeset
|
343 |
NONE => (([], [], []), node) |
458573968568
refined Document.edit: less stateful update via Graph.schedule;
wenzelm
parents:
44196
diff
changeset
|
344 |
| SOME ((prev, id), _) => |
458573968568
refined Document.edit: less stateful update via Graph.schedule;
wenzelm
parents:
44196
diff
changeset
|
345 |
let |
458573968568
refined Document.edit: less stateful update via Graph.schedule;
wenzelm
parents:
44196
diff
changeset
|
346 |
val prev_exec = |
458573968568
refined Document.edit: less stateful update via Graph.schedule;
wenzelm
parents:
44196
diff
changeset
|
347 |
(case prev of |
458573968568
refined Document.edit: less stateful update via Graph.schedule;
wenzelm
parents:
44196
diff
changeset
|
348 |
NONE => no_id |
458573968568
refined Document.edit: less stateful update via Graph.schedule;
wenzelm
parents:
44196
diff
changeset
|
349 |
| SOME prev_id => the_default no_id (the_entry node prev_id)); |
458573968568
refined Document.edit: less stateful update via Graph.schedule;
wenzelm
parents:
44196
diff
changeset
|
350 |
val (assigns, execs, result) = |
458573968568
refined Document.edit: less stateful update via Graph.schedule;
wenzelm
parents:
44196
diff
changeset
|
351 |
fold_entries (SOME id) |
458573968568
refined Document.edit: less stateful update via Graph.schedule;
wenzelm
parents:
44196
diff
changeset
|
352 |
(new_exec (name, get_header node) o `(the_command state) o #2 o #1) |
458573968568
refined Document.edit: less stateful update via Graph.schedule;
wenzelm
parents:
44196
diff
changeset
|
353 |
node ([], [], the_exec state prev_exec); |
458573968568
refined Document.edit: less stateful update via Graph.schedule;
wenzelm
parents:
44196
diff
changeset
|
354 |
val node' = node |> fold update_entry assigns |> set_result result; |
458573968568
refined Document.edit: less stateful update via Graph.schedule;
wenzelm
parents:
44196
diff
changeset
|
355 |
in ((assigns, execs, [(name, node')]), node') end)) |
458573968568
refined Document.edit: less stateful update via Graph.schedule;
wenzelm
parents:
44196
diff
changeset
|
356 |
|> map #1; |
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
357 |
|
44197
458573968568
refined Document.edit: less stateful update via Graph.schedule;
wenzelm
parents:
44196
diff
changeset
|
358 |
val state' = state |
458573968568
refined Document.edit: less stateful update via Graph.schedule;
wenzelm
parents:
44196
diff
changeset
|
359 |
|> fold (fold define_exec o #2) updates |
458573968568
refined Document.edit: less stateful update via Graph.schedule;
wenzelm
parents:
44196
diff
changeset
|
360 |
|> define_version new_id (fold (fold put_node o #3) updates new_version); |
38421
6cfc6fce7bfb
document commands: maintain transition as future (wrt. potentially slow Outer_Syntax.prepare_command), refrain from second Toplevel.put_id;
wenzelm
parents:
38419
diff
changeset
|
361 |
|
44197
458573968568
refined Document.edit: less stateful update via Graph.schedule;
wenzelm
parents:
44196
diff
changeset
|
362 |
in (maps #1 (rev updates), state') end; |
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
363 |
|
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
364 |
end; |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
365 |
|
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
366 |
|
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
367 |
(* execute *) |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
368 |
|
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
369 |
fun execute version_id state = |
41673 | 370 |
state |> map_state (fn (versions, commands, execs, _) => |
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
371 |
let |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
372 |
val version = the_version state version_id; |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
373 |
|
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
374 |
fun force_exec NONE = () |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
375 |
| force_exec (SOME exec_id) = ignore (Lazy.force (the_exec state exec_id)); |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
376 |
|
44180 | 377 |
val execution' = (* FIXME Graph.schedule *) |
44113 | 378 |
Future.forks |
379 |
{name = "Document.execute", group = NONE, deps = [], pri = 1, interrupts = true} |
|
41673 | 380 |
[fn () => |
43666 | 381 |
node_names_of version |> List.app (fn name => |
382 |
fold_entries NONE (fn (_, exec) => fn () => force_exec exec) |
|
44185 | 383 |
(node_of version name) ())]; |
40520
77a7b0a7d4b1
await_cancellation in the main thread, independently of the execution futures, which might get interrupted or be absent after node deletetion;
wenzelm
parents:
40481
diff
changeset
|
384 |
|
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
385 |
in (versions, commands, execs, execution') end); |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
386 |
|
43713
1ba5331b4623
moved global state to structure Document (again);
wenzelm
parents:
43668
diff
changeset
|
387 |
|
1ba5331b4623
moved global state to structure Document (again);
wenzelm
parents:
43668
diff
changeset
|
388 |
|
1ba5331b4623
moved global state to structure Document (again);
wenzelm
parents:
43668
diff
changeset
|
389 |
(** global state **) |
1ba5331b4623
moved global state to structure Document (again);
wenzelm
parents:
43668
diff
changeset
|
390 |
|
1ba5331b4623
moved global state to structure Document (again);
wenzelm
parents:
43668
diff
changeset
|
391 |
val global_state = Synchronized.var "Document" init_state; |
1ba5331b4623
moved global state to structure Document (again);
wenzelm
parents:
43668
diff
changeset
|
392 |
|
1ba5331b4623
moved global state to structure Document (again);
wenzelm
parents:
43668
diff
changeset
|
393 |
fun state () = Synchronized.value global_state; |
1ba5331b4623
moved global state to structure Document (again);
wenzelm
parents:
43668
diff
changeset
|
394 |
val change_state = Synchronized.change global_state; |
1ba5331b4623
moved global state to structure Document (again);
wenzelm
parents:
43668
diff
changeset
|
395 |
|
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
396 |
end; |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset
|
397 |