author | wenzelm |
Thu, 06 Jun 2024 11:53:52 +0200 | |
changeset 80266 | d52be75ae60b |
parent 72771 | 72976a6bd2ba |
child 80820 | db114ec720cb |
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 |
|
71622 | 9 |
val marker_text: string -> string -> unit |
10 |
val marker: 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 |
||
72771 | 18 |
(* message markers *) |
19 |
||
71622 | 20 |
fun marker_text a text = |
71619
e33f6e5f86b6
clarified protocol messages: explicitly use physical_writeln, always encode_lines;
wenzelm
parents:
70907
diff
changeset
|
21 |
Output.physical_writeln ("\f" ^ a ^ " = " ^ encode_lines text); |
e33f6e5f86b6
clarified protocol messages: explicitly use physical_writeln, always encode_lines;
wenzelm
parents:
70907
diff
changeset
|
22 |
|
71622 | 23 |
fun marker a props = |
24 |
marker_text a (YXML.string_of_body (XML.Encode.properties props)); |
|
70907 | 25 |
|
26 |
||
72771 | 27 |
(* inlined messages *) |
28 |
||
59714 | 29 |
fun command_positions id = |
30 |
let |
|
31 |
fun attribute (a, b) = |
|
32 |
if a = Markup.idN andalso b = Markup.commandN then (a, id) else (a, b); |
|
33 |
fun tree (XML.Elem ((a, atts), ts)) = XML.Elem ((a, map attribute atts), map tree ts) |
|
34 |
| tree text = text; |
|
35 |
in map tree end; |
|
36 |
||
37 |
fun command_positions_yxml id = |
|
38 |
YXML.string_of_body o command_positions id o YXML.parse_body; |
|
39 |
||
40 |
end; |