author | wenzelm |
Fri, 06 Sep 2024 20:31:20 +0200 | |
changeset 80820 | db114ec720cb |
parent 72771 | 72976a6bd2ba |
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 |
|
80820
db114ec720cb
more thorough Protocol_Message.clean_output, following Isabelle/Scala;
wenzelm
parents:
72771
diff
changeset
|
13 |
val clean_output: string -> string |
59714 | 14 |
end; |
15 |
||
16 |
structure Protocol_Message: PROTOCOL_MESSAGE = |
|
17 |
struct |
|
18 |
||
72771 | 19 |
(* message markers *) |
20 |
||
71622 | 21 |
fun marker_text a text = |
71619
e33f6e5f86b6
clarified protocol messages: explicitly use physical_writeln, always encode_lines;
wenzelm
parents:
70907
diff
changeset
|
22 |
Output.physical_writeln ("\f" ^ a ^ " = " ^ encode_lines text); |
e33f6e5f86b6
clarified protocol messages: explicitly use physical_writeln, always encode_lines;
wenzelm
parents:
70907
diff
changeset
|
23 |
|
71622 | 24 |
fun marker a props = |
25 |
marker_text a (YXML.string_of_body (XML.Encode.properties props)); |
|
70907 | 26 |
|
27 |
||
72771 | 28 |
(* inlined messages *) |
29 |
||
59714 | 30 |
fun command_positions id = |
31 |
let |
|
32 |
fun attribute (a, b) = |
|
33 |
if a = Markup.idN andalso b = Markup.commandN then (a, id) else (a, b); |
|
34 |
fun tree (XML.Elem ((a, atts), ts)) = XML.Elem ((a, map attribute atts), map tree ts) |
|
35 |
| tree text = text; |
|
36 |
in map tree end; |
|
37 |
||
38 |
fun command_positions_yxml id = |
|
39 |
YXML.string_of_body o command_positions id o YXML.parse_body; |
|
40 |
||
80820
db114ec720cb
more thorough Protocol_Message.clean_output, following Isabelle/Scala;
wenzelm
parents:
72771
diff
changeset
|
41 |
|
db114ec720cb
more thorough Protocol_Message.clean_output, following Isabelle/Scala;
wenzelm
parents:
72771
diff
changeset
|
42 |
(* clean output *) |
db114ec720cb
more thorough Protocol_Message.clean_output, following Isabelle/Scala;
wenzelm
parents:
72771
diff
changeset
|
43 |
|
db114ec720cb
more thorough Protocol_Message.clean_output, following Isabelle/Scala;
wenzelm
parents:
72771
diff
changeset
|
44 |
fun clean_output msg = |
db114ec720cb
more thorough Protocol_Message.clean_output, following Isabelle/Scala;
wenzelm
parents:
72771
diff
changeset
|
45 |
(case try YXML.parse_body msg of |
db114ec720cb
more thorough Protocol_Message.clean_output, following Isabelle/Scala;
wenzelm
parents:
72771
diff
changeset
|
46 |
SOME xml => |
db114ec720cb
more thorough Protocol_Message.clean_output, following Isabelle/Scala;
wenzelm
parents:
72771
diff
changeset
|
47 |
xml |> XML.filter_elements |
db114ec720cb
more thorough Protocol_Message.clean_output, following Isabelle/Scala;
wenzelm
parents:
72771
diff
changeset
|
48 |
{remove = fn a => a = Markup.reportN, |
db114ec720cb
more thorough Protocol_Message.clean_output, following Isabelle/Scala;
wenzelm
parents:
72771
diff
changeset
|
49 |
expose = fn a => a = Markup.no_reportN} |
db114ec720cb
more thorough Protocol_Message.clean_output, following Isabelle/Scala;
wenzelm
parents:
72771
diff
changeset
|
50 |
|> XML.content_of |
db114ec720cb
more thorough Protocol_Message.clean_output, following Isabelle/Scala;
wenzelm
parents:
72771
diff
changeset
|
51 |
| NONE => msg); |
db114ec720cb
more thorough Protocol_Message.clean_output, following Isabelle/Scala;
wenzelm
parents:
72771
diff
changeset
|
52 |
|
59714 | 53 |
end; |