wenzelm@38801
|
1 |
(* Title: Pure/PIDE/isar_document.ML
|
wenzelm@38658
|
2 |
Author: Makarius
|
wenzelm@38658
|
3 |
|
wenzelm@38861
|
4 |
Protocol message formats for interactive Isar documents.
|
wenzelm@38658
|
5 |
*)
|
wenzelm@38658
|
6 |
|
wenzelm@44584
|
7 |
structure Isar_Document: sig end =
|
wenzelm@38658
|
8 |
struct
|
wenzelm@38658
|
9 |
|
wenzelm@38677
|
10 |
val _ =
|
wenzelm@38677
|
11 |
Isabelle_Process.add_command "Isar_Document.define_command"
|
wenzelm@44584
|
12 |
(fn [id, text] => Document.change_state (Document.define_command (Document.parse_id id) text));
|
wenzelm@38658
|
13 |
|
wenzelm@38677
|
14 |
val _ =
|
wenzelm@38677
|
15 |
Isabelle_Process.add_command "Isar_Document.edit_version"
|
wenzelm@45028
|
16 |
(fn [old_id_string, new_id_string, edits_yxml] => Document.change_state (fn state =>
|
wenzelm@38677
|
17 |
let
|
wenzelm@38677
|
18 |
val old_id = Document.parse_id old_id_string;
|
wenzelm@38677
|
19 |
val new_id = Document.parse_id new_id_string;
|
wenzelm@45028
|
20 |
val edits =
|
wenzelm@45028
|
21 |
YXML.parse_body edits_yxml |>
|
wenzelm@45028
|
22 |
let open XML.Decode in
|
wenzelm@45028
|
23 |
list (pair string
|
wenzelm@45028
|
24 |
(variant
|
wenzelm@45058
|
25 |
[fn ([], []) => Document.Clear,
|
wenzelm@45028
|
26 |
fn ([], a) => Document.Edits (list (pair (option int) (option int)) a),
|
wenzelm@45028
|
27 |
fn ([], a) =>
|
wenzelm@45058
|
28 |
Document.Header
|
wenzelm@45058
|
29 |
(Exn.Res (triple string (list string) (list (pair string bool)) a)),
|
wenzelm@45055
|
30 |
fn ([a], []) => Document.Header (Exn.Exn (ERROR a))]))
|
wenzelm@45028
|
31 |
end;
|
wenzelm@38658
|
32 |
|
wenzelm@45176
|
33 |
val running = Document.cancel_execution state;
|
wenzelm@45028
|
34 |
val (updates, state') = Document.edit old_id new_id edits state;
|
wenzelm@45176
|
35 |
val _ = Future.join_tasks running;
|
wenzelm@45068
|
36 |
val _ = Document.join_commands state';
|
wenzelm@38677
|
37 |
val _ =
|
wenzelm@44540
|
38 |
Output.status (Markup.markup (Markup.assign new_id)
|
wenzelm@44540
|
39 |
(implode (map (Markup.markup_only o Markup.edit) updates)));
|
wenzelm@38677
|
40 |
val state'' = Document.execute new_id state';
|
wenzelm@38677
|
41 |
in state'' end));
|
wenzelm@38658
|
42 |
|
wenzelm@44624
|
43 |
val _ =
|
wenzelm@44624
|
44 |
Isabelle_Process.add_command "Isar_Document.invoke_scala"
|
wenzelm@44624
|
45 |
(fn [id, tag, res] => Invoke_Scala.fulfill_method id tag res);
|
wenzelm@44624
|
46 |
|
wenzelm@38658
|
47 |
end;
|
wenzelm@38658
|
48 |
|