wenzelm@38483
|
1 |
(* Title: Pure/PIDE/isar_document.ML
|
wenzelm@38412
|
2 |
Author: Makarius
|
wenzelm@38412
|
3 |
|
wenzelm@38567
|
4 |
Protocol message formats for interactive Isar documents.
|
wenzelm@38412
|
5 |
*)
|
wenzelm@38412
|
6 |
|
wenzelm@43713
|
7 |
structure Isar_Document: sig end =
|
wenzelm@38412
|
8 |
struct
|
wenzelm@38412
|
9 |
|
wenzelm@38418
|
10 |
val _ =
|
wenzelm@38418
|
11 |
Isabelle_Process.add_command "Isar_Document.define_command"
|
wenzelm@44644
|
12 |
(fn [id, name, text] =>
|
wenzelm@44644
|
13 |
Document.change_state (Document.define_command (Document.parse_id id) name text));
|
wenzelm@38412
|
14 |
|
wenzelm@38418
|
15 |
val _ =
|
wenzelm@44612
|
16 |
Isabelle_Process.add_command "Isar_Document.cancel_execution"
|
wenzelm@44612
|
17 |
(fn [] => ignore (Document.cancel_execution (Document.state ())));
|
wenzelm@44612
|
18 |
|
wenzelm@44612
|
19 |
val _ =
|
wenzelm@44436
|
20 |
Isabelle_Process.add_command "Isar_Document.update_perspective"
|
wenzelm@44436
|
21 |
(fn [old_id_string, new_id_string, name, ids_yxml] => Document.change_state (fn state =>
|
wenzelm@44436
|
22 |
let
|
wenzelm@44436
|
23 |
val old_id = Document.parse_id old_id_string;
|
wenzelm@44436
|
24 |
val new_id = Document.parse_id new_id_string;
|
wenzelm@44436
|
25 |
val ids = YXML.parse_body ids_yxml
|
wenzelm@44436
|
26 |
|> let open XML.Decode in list int end;
|
wenzelm@44436
|
27 |
|
wenzelm@44436
|
28 |
val _ = Future.join_tasks (Document.cancel_execution state);
|
wenzelm@44436
|
29 |
in
|
wenzelm@44436
|
30 |
state
|
wenzelm@44436
|
31 |
|> Document.update_perspective old_id new_id name ids
|
wenzelm@44436
|
32 |
|> Document.execute new_id
|
wenzelm@44436
|
33 |
end));
|
wenzelm@44436
|
34 |
|
wenzelm@44436
|
35 |
val _ =
|
wenzelm@44481
|
36 |
Isabelle_Process.add_command "Isar_Document.update"
|
wenzelm@44157
|
37 |
(fn [old_id_string, new_id_string, edits_yxml] => Document.change_state (fn state =>
|
wenzelm@38418
|
38 |
let
|
wenzelm@38418
|
39 |
val old_id = Document.parse_id old_id_string;
|
wenzelm@38418
|
40 |
val new_id = Document.parse_id new_id_string;
|
wenzelm@44157
|
41 |
val edits =
|
wenzelm@44157
|
42 |
YXML.parse_body edits_yxml |>
|
wenzelm@44157
|
43 |
let open XML.Decode in
|
wenzelm@44157
|
44 |
list (pair string
|
wenzelm@44157
|
45 |
(variant
|
wenzelm@44185
|
46 |
[fn ([], []) => Document.Clear,
|
wenzelm@44157
|
47 |
fn ([], a) => Document.Edits (list (pair (option int) (option int)) a),
|
wenzelm@44157
|
48 |
fn ([], a) =>
|
wenzelm@44185
|
49 |
Document.Header
|
wenzelm@44185
|
50 |
(Exn.Res (triple string (list string) (list (pair string bool)) a)),
|
wenzelm@44384
|
51 |
fn ([a], []) => Document.Header (Exn.Exn (ERROR a)),
|
wenzelm@44384
|
52 |
fn (a, []) => Document.Perspective (map int_atom a)]))
|
wenzelm@44157
|
53 |
end;
|
wenzelm@38412
|
54 |
|
wenzelm@44436
|
55 |
val running = Document.cancel_execution state;
|
wenzelm@44610
|
56 |
val (assignment, state1) = Document.update old_id new_id edits state;
|
wenzelm@44436
|
57 |
val _ = Future.join_tasks running;
|
wenzelm@44610
|
58 |
val state2 = Document.join_commands state1;
|
wenzelm@44436
|
59 |
val _ =
|
wenzelm@44436
|
60 |
Output.status (Markup.markup (Markup.assign new_id)
|
wenzelm@44476
|
61 |
(assignment |>
|
wenzelm@44476
|
62 |
let open XML.Encode
|
wenzelm@44479
|
63 |
in pair (list (pair int (option int))) (list (pair string (option int))) end
|
wenzelm@44476
|
64 |
|> YXML.string_of_body));
|
wenzelm@44610
|
65 |
val state3 = Document.execute new_id state2;
|
wenzelm@44610
|
66 |
in state3 end));
|
wenzelm@38412
|
67 |
|
wenzelm@43748
|
68 |
val _ =
|
wenzelm@43748
|
69 |
Isabelle_Process.add_command "Isar_Document.invoke_scala"
|
wenzelm@43748
|
70 |
(fn [id, tag, res] => Invoke_Scala.fulfill_method id tag res);
|
wenzelm@43748
|
71 |
|
wenzelm@38412
|
72 |
end;
|
wenzelm@38412
|
73 |
|