src/Pure/PIDE/protocol_message.ML
author wenzelm
Mon Mar 13 21:37:35 2017 +0100 (2017-03-13 ago)
changeset 65214 a2ec0db555c7
parent 59714 ae322325adbb
permissions -rw-r--r--
clarified modules;
wenzelm@59714
     1
(*  Title:      Pure/PIDE/protocol_message.ML
wenzelm@59714
     2
    Author:     Makarius
wenzelm@59714
     3
wenzelm@59714
     4
Auxiliary operations on protocol messages.
wenzelm@59714
     5
*)
wenzelm@59714
     6
wenzelm@59714
     7
signature PROTOCOL_MESSAGE =
wenzelm@59714
     8
sig
wenzelm@59714
     9
  val command_positions: string -> XML.body -> XML.body
wenzelm@59714
    10
  val command_positions_yxml: string -> string -> string
wenzelm@59714
    11
end;
wenzelm@59714
    12
wenzelm@59714
    13
structure Protocol_Message: PROTOCOL_MESSAGE =
wenzelm@59714
    14
struct
wenzelm@59714
    15
wenzelm@59714
    16
fun command_positions id =
wenzelm@59714
    17
  let
wenzelm@59714
    18
    fun attribute (a, b) =
wenzelm@59714
    19
      if a = Markup.idN andalso b = Markup.commandN then (a, id) else (a, b);
wenzelm@59714
    20
    fun tree (XML.Elem ((a, atts), ts)) = XML.Elem ((a, map attribute atts), map tree ts)
wenzelm@59714
    21
      | tree text = text;
wenzelm@59714
    22
  in map tree end;
wenzelm@59714
    23
wenzelm@59714
    24
fun command_positions_yxml id =
wenzelm@59714
    25
  YXML.string_of_body o command_positions id o YXML.parse_body;
wenzelm@59714
    26
wenzelm@59714
    27
end;