author | wenzelm |
Sun, 29 Mar 2020 13:25:59 +0200 | |
changeset 71619 | e33f6e5f86b6 |
parent 70907 | 7e3f25a0cee4 |
child 71622 | ab5009192ebb |
permissions | -rw-r--r-- |
59714 | 1 |
(* Title: Pure/PIDE/protocol_message.ML |
2 |
Author: Makarius |
|
3 |
||
4 |
Auxiliary operations on protocol messages. |
|
5 |
*) |
|
6 |
||
7 |
signature PROTOCOL_MESSAGE = |
|
8 |
sig |
|
71619
e33f6e5f86b6
clarified protocol messages: explicitly use physical_writeln, always encode_lines;
wenzelm
parents:
70907
diff
changeset
|
9 |
val inline_text: string -> string -> unit |
e33f6e5f86b6
clarified protocol messages: explicitly use physical_writeln, always encode_lines;
wenzelm
parents:
70907
diff
changeset
|
10 |
val inline_properties: string -> Properties.T -> unit |
59714 | 11 |
val command_positions: string -> XML.body -> XML.body |
12 |
val command_positions_yxml: string -> string -> string |
|
13 |
end; |
|
14 |
||
15 |
structure Protocol_Message: PROTOCOL_MESSAGE = |
|
16 |
struct |
|
17 |
||
71619
e33f6e5f86b6
clarified protocol messages: explicitly use physical_writeln, always encode_lines;
wenzelm
parents:
70907
diff
changeset
|
18 |
fun inline_text a text = |
e33f6e5f86b6
clarified protocol messages: explicitly use physical_writeln, always encode_lines;
wenzelm
parents:
70907
diff
changeset
|
19 |
Output.physical_writeln ("\f" ^ a ^ " = " ^ encode_lines text); |
e33f6e5f86b6
clarified protocol messages: explicitly use physical_writeln, always encode_lines;
wenzelm
parents:
70907
diff
changeset
|
20 |
|
e33f6e5f86b6
clarified protocol messages: explicitly use physical_writeln, always encode_lines;
wenzelm
parents:
70907
diff
changeset
|
21 |
fun inline_properties a props = |
e33f6e5f86b6
clarified protocol messages: explicitly use physical_writeln, always encode_lines;
wenzelm
parents:
70907
diff
changeset
|
22 |
inline_text a (YXML.string_of_body (XML.Encode.properties props)); |
70907 | 23 |
|
24 |
||
59714 | 25 |
fun command_positions id = |
26 |
let |
|
27 |
fun attribute (a, b) = |
|
28 |
if a = Markup.idN andalso b = Markup.commandN then (a, id) else (a, b); |
|
29 |
fun tree (XML.Elem ((a, atts), ts)) = XML.Elem ((a, map attribute atts), map tree ts) |
|
30 |
| tree text = text; |
|
31 |
in map tree end; |
|
32 |
||
33 |
fun command_positions_yxml id = |
|
34 |
YXML.string_of_body o command_positions id o YXML.parse_body; |
|
35 |
||
36 |
end; |