wenzelm@38453
|
1 |
(* Title: Pure/PIDE/document.ML
|
wenzelm@38453
|
2 |
Author: Makarius
|
wenzelm@38453
|
3 |
|
wenzelm@38453
|
4 |
Document as collection of named nodes, each consisting of an editable
|
wenzelm@38677
|
5 |
list of commands, associated with asynchronous execution process.
|
wenzelm@38453
|
6 |
*)
|
wenzelm@38453
|
7 |
|
wenzelm@38453
|
8 |
signature DOCUMENT =
|
wenzelm@38453
|
9 |
sig
|
wenzelm@38645
|
10 |
type id = int
|
wenzelm@38655
|
11 |
type version_id = id
|
wenzelm@38655
|
12 |
type command_id = id
|
wenzelm@38645
|
13 |
type exec_id = id
|
wenzelm@38645
|
14 |
val no_id: id
|
wenzelm@38678
|
15 |
val new_id: unit -> id
|
wenzelm@38645
|
16 |
val parse_id: string -> id
|
wenzelm@38645
|
17 |
val print_id: id -> string
|
wenzelm@38708
|
18 |
type edit = string * ((command_id option * command_id option) list) option
|
wenzelm@38677
|
19 |
type state
|
wenzelm@38677
|
20 |
val init_state: state
|
wenzelm@41882
|
21 |
val cancel: state -> unit
|
wenzelm@38677
|
22 |
val define_command: command_id -> string -> state -> state
|
wenzelm@38677
|
23 |
val edit: version_id -> version_id -> edit list -> state -> (command_id * exec_id) list * state
|
wenzelm@38677
|
24 |
val execute: version_id -> state -> state
|
wenzelm@38453
|
25 |
end;
|
wenzelm@38453
|
26 |
|
wenzelm@38453
|
27 |
structure Document: DOCUMENT =
|
wenzelm@38453
|
28 |
struct
|
wenzelm@38453
|
29 |
|
wenzelm@38453
|
30 |
(* unique identifiers *)
|
wenzelm@38453
|
31 |
|
wenzelm@38645
|
32 |
type id = int;
|
wenzelm@38655
|
33 |
type version_id = id;
|
wenzelm@38655
|
34 |
type command_id = id;
|
wenzelm@38645
|
35 |
type exec_id = id;
|
wenzelm@38453
|
36 |
|
wenzelm@38637
|
37 |
val no_id = 0;
|
wenzelm@40706
|
38 |
val new_id = Synchronized.counter ();
|
wenzelm@38677
|
39 |
|
wenzelm@38660
|
40 |
val parse_id = Markup.parse_int;
|
wenzelm@38660
|
41 |
val print_id = Markup.print_int;
|
wenzelm@38453
|
42 |
|
wenzelm@38677
|
43 |
fun err_dup kind id = error ("Duplicate " ^ kind ^ ": " ^ print_id id);
|
wenzelm@38677
|
44 |
fun err_undef kind id = error ("Undefined " ^ kind ^ ": " ^ print_id id);
|
wenzelm@38453
|
45 |
|
wenzelm@38677
|
46 |
|
wenzelm@38677
|
47 |
|
wenzelm@38677
|
48 |
(** document structure **)
|
wenzelm@38677
|
49 |
|
wenzelm@38708
|
50 |
structure Entries = Linear_Set(type key = command_id val ord = int_ord);
|
wenzelm@38708
|
51 |
|
wenzelm@38708
|
52 |
abstype node = Node of exec_id option Entries.T (*command entries with excecutions*)
|
wenzelm@38677
|
53 |
and version = Version of node Graph.T (*development graph wrt. static imports*)
|
wenzelm@38677
|
54 |
with
|
wenzelm@38677
|
55 |
|
wenzelm@38708
|
56 |
val empty_node = Node Entries.empty;
|
wenzelm@38708
|
57 |
val empty_version = Version Graph.empty;
|
wenzelm@38677
|
58 |
|
wenzelm@38708
|
59 |
fun fold_entries start f (Node entries) = Entries.fold start f entries;
|
wenzelm@38708
|
60 |
fun first_entry start P (Node entries) = Entries.get_first start P entries;
|
wenzelm@38677
|
61 |
|
wenzelm@38677
|
62 |
|
wenzelm@38708
|
63 |
(* node edits and associated executions *)
|
wenzelm@38453
|
64 |
|
wenzelm@38453
|
65 |
type edit =
|
wenzelm@38708
|
66 |
string *
|
wenzelm@38708
|
67 |
(*NONE: remove node, SOME: insert/remove commands*)
|
wenzelm@38708
|
68 |
((command_id option * command_id option) list) option;
|
wenzelm@38453
|
69 |
|
wenzelm@38708
|
70 |
fun the_entry (Node entries) id =
|
wenzelm@38708
|
71 |
(case Entries.lookup entries id of
|
wenzelm@38708
|
72 |
NONE => err_undef "command entry" id
|
wenzelm@38708
|
73 |
| SOME entry => entry);
|
wenzelm@38677
|
74 |
|
wenzelm@38708
|
75 |
fun update_entry (id, exec_id) (Node entries) =
|
wenzelm@38708
|
76 |
Node (Entries.update (id, SOME exec_id) entries);
|
wenzelm@38708
|
77 |
|
wenzelm@38708
|
78 |
fun reset_after id entries =
|
wenzelm@38708
|
79 |
(case Entries.get_after entries id of
|
wenzelm@38708
|
80 |
NONE => entries
|
wenzelm@38708
|
81 |
| SOME next => Entries.update (next, NONE) entries);
|
wenzelm@38708
|
82 |
|
wenzelm@38708
|
83 |
fun edit_node (hook, SOME id2) (Node entries) =
|
wenzelm@38708
|
84 |
Node (Entries.insert_after hook (id2, NONE) entries)
|
wenzelm@38708
|
85 |
| edit_node (hook, NONE) (Node entries) =
|
wenzelm@38708
|
86 |
Node (entries |> Entries.delete_after hook |> reset_after hook);
|
wenzelm@38677
|
87 |
|
wenzelm@38677
|
88 |
|
wenzelm@38677
|
89 |
(* version operations *)
|
wenzelm@38677
|
90 |
|
wenzelm@38677
|
91 |
fun nodes_of (Version nodes) = nodes;
|
wenzelm@38677
|
92 |
val node_names_of = Graph.keys o nodes_of;
|
wenzelm@38677
|
93 |
|
wenzelm@38708
|
94 |
fun get_node version name = Graph.get_node (nodes_of version) name
|
wenzelm@38708
|
95 |
handle Graph.UNDEF _ => empty_node;
|
wenzelm@38708
|
96 |
|
wenzelm@38677
|
97 |
fun edit_nodes (name, SOME edits) (Version nodes) =
|
wenzelm@38677
|
98 |
Version (nodes
|
wenzelm@38677
|
99 |
|> Graph.default_node (name, empty_node)
|
wenzelm@38677
|
100 |
|> Graph.map_node name (fold edit_node edits))
|
wenzelm@38708
|
101 |
| edit_nodes (name, NONE) (Version nodes) =
|
wenzelm@40750
|
102 |
Version (perhaps (try (Graph.del_node name)) nodes);
|
wenzelm@38677
|
103 |
|
wenzelm@38677
|
104 |
fun put_node name node (Version nodes) =
|
wenzelm@40750
|
105 |
Version (nodes
|
wenzelm@40750
|
106 |
|> Graph.default_node (name, empty_node)
|
wenzelm@40750
|
107 |
|> Graph.map_node name (K node));
|
wenzelm@38677
|
108 |
|
wenzelm@38453
|
109 |
end;
|
wenzelm@38453
|
110 |
|
wenzelm@38677
|
111 |
|
wenzelm@38677
|
112 |
|
wenzelm@38677
|
113 |
(** global state -- document structure and execution process **)
|
wenzelm@38677
|
114 |
|
wenzelm@38677
|
115 |
abstype state = State of
|
wenzelm@40677
|
116 |
{versions: version Inttab.table, (*version_id -> document content*)
|
wenzelm@38680
|
117 |
commands: Toplevel.transition future Inttab.table, (*command_id -> transition (future parsing)*)
|
wenzelm@40677
|
118 |
execs: (bool * Toplevel.state) lazy Inttab.table, (*exec_id -> execution process*)
|
wenzelm@40677
|
119 |
execution: unit future list} (*global execution process*)
|
wenzelm@38677
|
120 |
with
|
wenzelm@38677
|
121 |
|
wenzelm@38677
|
122 |
fun make_state (versions, commands, execs, execution) =
|
wenzelm@38677
|
123 |
State {versions = versions, commands = commands, execs = execs, execution = execution};
|
wenzelm@38677
|
124 |
|
wenzelm@38677
|
125 |
fun map_state f (State {versions, commands, execs, execution}) =
|
wenzelm@38677
|
126 |
make_state (f (versions, commands, execs, execution));
|
wenzelm@38677
|
127 |
|
wenzelm@38677
|
128 |
val init_state =
|
wenzelm@38677
|
129 |
make_state (Inttab.make [(no_id, empty_version)],
|
wenzelm@38709
|
130 |
Inttab.make [(no_id, Future.value Toplevel.empty)],
|
wenzelm@40677
|
131 |
Inttab.make [(no_id, Lazy.value (true, Toplevel.toplevel))],
|
wenzelm@38677
|
132 |
[]);
|
wenzelm@38677
|
133 |
|
wenzelm@38677
|
134 |
|
wenzelm@38677
|
135 |
(* document versions *)
|
wenzelm@38677
|
136 |
|
wenzelm@38677
|
137 |
fun define_version (id: version_id) version =
|
wenzelm@38677
|
138 |
map_state (fn (versions, commands, execs, execution) =>
|
wenzelm@38677
|
139 |
let val versions' = Inttab.update_new (id, version) versions
|
wenzelm@38677
|
140 |
handle Inttab.DUP dup => err_dup "document version" dup
|
wenzelm@38677
|
141 |
in (versions', commands, execs, execution) end);
|
wenzelm@38677
|
142 |
|
wenzelm@38677
|
143 |
fun the_version (State {versions, ...}) (id: version_id) =
|
wenzelm@38677
|
144 |
(case Inttab.lookup versions id of
|
wenzelm@38677
|
145 |
NONE => err_undef "document version" id
|
wenzelm@38677
|
146 |
| SOME version => version);
|
wenzelm@38677
|
147 |
|
wenzelm@38677
|
148 |
|
wenzelm@38677
|
149 |
(* commands *)
|
wenzelm@38677
|
150 |
|
wenzelm@38677
|
151 |
fun define_command (id: command_id) text =
|
wenzelm@38677
|
152 |
map_state (fn (versions, commands, execs, execution) =>
|
wenzelm@38677
|
153 |
let
|
wenzelm@38677
|
154 |
val id_string = print_id id;
|
wenzelm@38680
|
155 |
val tr = Future.fork_pri 2 (fn () =>
|
wenzelm@38677
|
156 |
Position.setmp_thread_data (Position.id_only id_string)
|
wenzelm@38680
|
157 |
(fn () => Outer_Syntax.prepare_command (Position.id id_string) text) ());
|
wenzelm@38677
|
158 |
val commands' =
|
wenzelm@38680
|
159 |
Inttab.update_new (id, tr) commands
|
wenzelm@38677
|
160 |
handle Inttab.DUP dup => err_dup "command" dup;
|
wenzelm@38677
|
161 |
in (versions, commands', execs, execution) end);
|
wenzelm@38677
|
162 |
|
wenzelm@38677
|
163 |
fun the_command (State {commands, ...}) (id: command_id) =
|
wenzelm@38677
|
164 |
(case Inttab.lookup commands id of
|
wenzelm@38677
|
165 |
NONE => err_undef "command" id
|
wenzelm@38677
|
166 |
| SOME tr => tr);
|
wenzelm@38677
|
167 |
|
wenzelm@38680
|
168 |
fun join_commands (State {commands, ...}) =
|
wenzelm@38680
|
169 |
Inttab.fold (fn (_, tr) => fn () => ignore (Future.join_result tr)) commands ();
|
wenzelm@38680
|
170 |
|
wenzelm@38677
|
171 |
|
wenzelm@38677
|
172 |
(* command executions *)
|
wenzelm@38677
|
173 |
|
wenzelm@38677
|
174 |
fun define_exec (id: exec_id) exec =
|
wenzelm@38677
|
175 |
map_state (fn (versions, commands, execs, execution) =>
|
wenzelm@38677
|
176 |
let val execs' = Inttab.update_new (id, exec) execs
|
wenzelm@38677
|
177 |
handle Inttab.DUP dup => err_dup "command execution" dup
|
wenzelm@38677
|
178 |
in (versions, commands, execs', execution) end);
|
wenzelm@38677
|
179 |
|
wenzelm@38677
|
180 |
fun the_exec (State {execs, ...}) (id: exec_id) =
|
wenzelm@38677
|
181 |
(case Inttab.lookup execs id of
|
wenzelm@38677
|
182 |
NONE => err_undef "command execution" id
|
wenzelm@38677
|
183 |
| SOME exec => exec);
|
wenzelm@38677
|
184 |
|
wenzelm@41882
|
185 |
|
wenzelm@41882
|
186 |
(* document execution *)
|
wenzelm@41882
|
187 |
|
wenzelm@41882
|
188 |
fun cancel (State {execution, ...}) =
|
wenzelm@41882
|
189 |
List.app Future.cancel execution;
|
wenzelm@41882
|
190 |
|
wenzelm@41882
|
191 |
fun await_cancellation (State {execution, ...}) =
|
wenzelm@41882
|
192 |
ignore (Future.join_results execution);
|
wenzelm@41882
|
193 |
|
wenzelm@38677
|
194 |
end;
|
wenzelm@38677
|
195 |
|
wenzelm@38677
|
196 |
|
wenzelm@38677
|
197 |
|
wenzelm@39214
|
198 |
(* toplevel transactions *)
|
wenzelm@39214
|
199 |
|
wenzelm@39214
|
200 |
local
|
wenzelm@39214
|
201 |
|
wenzelm@40670
|
202 |
fun timing tr t = Toplevel.status tr (Markup.timing t);
|
wenzelm@40670
|
203 |
|
wenzelm@39214
|
204 |
fun proof_status tr st =
|
wenzelm@39214
|
205 |
(case try Toplevel.proof_of st of
|
wenzelm@39214
|
206 |
SOME prf => Toplevel.status tr (Proof.status_markup prf)
|
wenzelm@39214
|
207 |
| NONE => ());
|
wenzelm@39214
|
208 |
|
wenzelm@39214
|
209 |
fun async_state tr st =
|
wenzelm@40780
|
210 |
ignore
|
wenzelm@42543
|
211 |
(singleton (Future.bulk {group = SOME (Task_Queue.new_group NONE), deps = [], pri = 0})
|
wenzelm@40780
|
212 |
(fn () =>
|
wenzelm@40780
|
213 |
Toplevel.setmp_thread_position tr
|
wenzelm@40780
|
214 |
(fn () => Toplevel.print_state false st) ()));
|
wenzelm@39214
|
215 |
|
wenzelm@40669
|
216 |
fun run int tr st =
|
wenzelm@40669
|
217 |
(case Toplevel.transition int tr st of
|
wenzelm@40669
|
218 |
SOME (st', NONE) => ([], SOME st')
|
wenzelm@40669
|
219 |
| SOME (_, SOME exn_info) =>
|
wenzelm@40669
|
220 |
(case ML_Compiler.exn_messages (Runtime.EXCURSION_FAIL exn_info) of
|
wenzelm@40669
|
221 |
[] => Exn.interrupt ()
|
wenzelm@40669
|
222 |
| errs => (errs, NONE))
|
wenzelm@40669
|
223 |
| NONE => ([ML_Compiler.exn_message Runtime.TERMINATE], NONE));
|
wenzelm@40669
|
224 |
|
wenzelm@39214
|
225 |
in
|
wenzelm@39214
|
226 |
|
wenzelm@41785
|
227 |
fun run_command thy_name raw_tr st =
|
wenzelm@39214
|
228 |
(case
|
wenzelm@41785
|
229 |
(case Toplevel.init_of raw_tr of
|
wenzelm@41785
|
230 |
SOME name => Exn.capture (fn () =>
|
wenzelm@41785
|
231 |
let
|
wenzelm@41785
|
232 |
val path = Path.explode thy_name;
|
wenzelm@41785
|
233 |
val _ = Thy_Header.consistent_name (Path.implode (Path.base path)) name;
|
wenzelm@41785
|
234 |
in Toplevel.modify_master (SOME (Path.dir path)) raw_tr end) ()
|
wenzelm@41785
|
235 |
| NONE => Exn.Result raw_tr) of
|
wenzelm@41785
|
236 |
Exn.Result tr =>
|
wenzelm@39214
|
237 |
let
|
wenzelm@40780
|
238 |
val is_init = is_some (Toplevel.init_of tr);
|
wenzelm@40780
|
239 |
val is_proof = Keyword.is_proof (Toplevel.name_of tr);
|
wenzelm@40780
|
240 |
val do_print = not is_init andalso (Toplevel.print_of tr orelse is_proof);
|
wenzelm@40780
|
241 |
|
wenzelm@40670
|
242 |
val start = start_timing ();
|
wenzelm@40780
|
243 |
val (errs, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
|
wenzelm@40670
|
244 |
val _ = timing tr (end_timing start);
|
wenzelm@39214
|
245 |
val _ = List.app (Toplevel.error_msg tr) errs;
|
wenzelm@40677
|
246 |
val res =
|
wenzelm@39214
|
247 |
(case result of
|
wenzelm@40677
|
248 |
NONE => (Toplevel.status tr Markup.failed; (false, st))
|
wenzelm@39214
|
249 |
| SOME st' =>
|
wenzelm@39214
|
250 |
(Toplevel.status tr Markup.finished;
|
wenzelm@39214
|
251 |
proof_status tr st';
|
wenzelm@40780
|
252 |
if do_print then async_state tr st' else ();
|
wenzelm@40677
|
253 |
(true, st')));
|
wenzelm@40677
|
254 |
in res end
|
wenzelm@39214
|
255 |
| Exn.Exn exn =>
|
wenzelm@39515
|
256 |
if Exn.is_interrupt exn then reraise exn
|
wenzelm@39515
|
257 |
else
|
wenzelm@41785
|
258 |
(Toplevel.error_msg raw_tr (ML_Compiler.exn_message exn);
|
wenzelm@41785
|
259 |
Toplevel.status raw_tr Markup.failed;
|
wenzelm@40677
|
260 |
(false, Toplevel.toplevel)));
|
wenzelm@39214
|
261 |
|
wenzelm@39214
|
262 |
end;
|
wenzelm@39214
|
263 |
|
wenzelm@39214
|
264 |
|
wenzelm@39214
|
265 |
|
wenzelm@39214
|
266 |
|
wenzelm@38677
|
267 |
(** editing **)
|
wenzelm@38677
|
268 |
|
wenzelm@38677
|
269 |
(* edit *)
|
wenzelm@38677
|
270 |
|
wenzelm@38677
|
271 |
local
|
wenzelm@38677
|
272 |
|
wenzelm@38708
|
273 |
fun is_changed node' ((_, id), exec) =
|
wenzelm@38677
|
274 |
(case try (the_entry node') id of
|
wenzelm@38677
|
275 |
NONE => true
|
wenzelm@38708
|
276 |
| SOME exec' => exec' <> exec);
|
wenzelm@38677
|
277 |
|
wenzelm@38677
|
278 |
fun new_exec name (id: command_id) (exec_id, updates, state) =
|
wenzelm@38677
|
279 |
let
|
wenzelm@38677
|
280 |
val exec = the_exec state exec_id;
|
wenzelm@38678
|
281 |
val exec_id' = new_id ();
|
wenzelm@38709
|
282 |
val future_tr = the_command state id;
|
wenzelm@38677
|
283 |
val exec' =
|
wenzelm@38677
|
284 |
Lazy.lazy (fn () =>
|
wenzelm@40677
|
285 |
let
|
wenzelm@40677
|
286 |
val st = #2 (Lazy.force exec);
|
wenzelm@40677
|
287 |
val exec_tr = Toplevel.put_id (print_id exec_id') (Future.join future_tr);
|
wenzelm@40677
|
288 |
in run_command name exec_tr st end);
|
wenzelm@38677
|
289 |
val state' = define_exec exec_id' exec' state;
|
wenzelm@38677
|
290 |
in (exec_id', (id, exec_id') :: updates, state') end;
|
wenzelm@38677
|
291 |
|
wenzelm@38677
|
292 |
in
|
wenzelm@38677
|
293 |
|
wenzelm@38677
|
294 |
fun edit (old_id: version_id) (new_id: version_id) edits state =
|
wenzelm@38677
|
295 |
let
|
wenzelm@38677
|
296 |
val old_version = the_version state old_id;
|
wenzelm@41878
|
297 |
val _ = Time.now (); (* FIXME odd workaround *)
|
wenzelm@38677
|
298 |
val new_version = fold edit_nodes edits old_version;
|
wenzelm@38677
|
299 |
|
wenzelm@38677
|
300 |
fun update_node name (rev_updates, version, st) =
|
wenzelm@38708
|
301 |
let val node = get_node version name in
|
wenzelm@38708
|
302 |
(case first_entry NONE (is_changed (get_node old_version name)) node of
|
wenzelm@38677
|
303 |
NONE => (rev_updates, version, st)
|
wenzelm@38708
|
304 |
| SOME ((prev, id), _) =>
|
wenzelm@38677
|
305 |
let
|
wenzelm@38708
|
306 |
val prev_exec =
|
wenzelm@38708
|
307 |
(case prev of
|
wenzelm@38708
|
308 |
NONE => no_id
|
wenzelm@38708
|
309 |
| SOME prev_id => the_default no_id (the_entry node prev_id));
|
wenzelm@38677
|
310 |
val (_, rev_upds, st') =
|
wenzelm@38708
|
311 |
fold_entries (SOME id) (new_exec name o #2 o #1) node (prev_exec, [], st);
|
wenzelm@38708
|
312 |
val node' = fold update_entry rev_upds node;
|
wenzelm@38677
|
313 |
in (rev_upds @ rev_updates, put_node name node' version, st') end)
|
wenzelm@38677
|
314 |
end;
|
wenzelm@38677
|
315 |
|
wenzelm@38677
|
316 |
(* FIXME proper node deps *)
|
wenzelm@38677
|
317 |
val (rev_updates, new_version', state') =
|
wenzelm@38677
|
318 |
fold update_node (node_names_of new_version) ([], new_version, state);
|
wenzelm@38677
|
319 |
val state'' = define_version new_id new_version' state';
|
wenzelm@38680
|
320 |
|
wenzelm@38680
|
321 |
val _ = join_commands state''; (* FIXME async!? *)
|
wenzelm@38677
|
322 |
in (rev rev_updates, state'') end;
|
wenzelm@38677
|
323 |
|
wenzelm@38677
|
324 |
end;
|
wenzelm@38677
|
325 |
|
wenzelm@38677
|
326 |
|
wenzelm@38677
|
327 |
(* execute *)
|
wenzelm@38677
|
328 |
|
wenzelm@38677
|
329 |
fun execute version_id state =
|
wenzelm@38677
|
330 |
state |> map_state (fn (versions, commands, execs, execution) =>
|
wenzelm@38677
|
331 |
let
|
wenzelm@38677
|
332 |
val version = the_version state version_id;
|
wenzelm@38677
|
333 |
|
wenzelm@38677
|
334 |
fun force_exec NONE = ()
|
wenzelm@38677
|
335 |
| force_exec (SOME exec_id) = ignore (Lazy.force (the_exec state exec_id));
|
wenzelm@38677
|
336 |
|
wenzelm@41882
|
337 |
val _ = cancel state;
|
wenzelm@38677
|
338 |
|
wenzelm@38677
|
339 |
val execution' = (* FIXME proper node deps *)
|
wenzelm@42543
|
340 |
Future.bulk {group = NONE, deps = [], pri = 1} [fn () =>
|
wenzelm@41879
|
341 |
let
|
wenzelm@41882
|
342 |
val _ = await_cancellation state;
|
wenzelm@41879
|
343 |
val _ =
|
wenzelm@41879
|
344 |
node_names_of version |> List.app (fn name =>
|
wenzelm@41879
|
345 |
fold_entries NONE (fn (_, exec) => fn () => force_exec exec)
|
wenzelm@41879
|
346 |
(get_node version name) ());
|
wenzelm@42543
|
347 |
in () end];
|
wenzelm@40766
|
348 |
|
wenzelm@41882
|
349 |
val _ = await_cancellation state; (* FIXME async!? *)
|
wenzelm@40766
|
350 |
|
wenzelm@38677
|
351 |
in (versions, commands, execs, execution') end);
|
wenzelm@38677
|
352 |
|
wenzelm@38677
|
353 |
end;
|
wenzelm@38677
|
354 |
|