src/Pure/PIDE/protocol_message.ML
author wenzelm
Sun Mar 10 14:19:30 2019 +0100 (4 months ago ago)
changeset 70070 be04e9a053a7
parent 59714 ae322325adbb
permissions -rw-r--r--
markup and document markers for some meta data from "Dublin Core Metadata Element Set";
     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
     9   val command_positions: string -> XML.body -> XML.body
    10   val command_positions_yxml: string -> string -> string
    11 end;
    12 
    13 structure Protocol_Message: PROTOCOL_MESSAGE =
    14 struct
    15 
    16 fun command_positions id =
    17   let
    18     fun attribute (a, b) =
    19       if a = Markup.idN andalso b = Markup.commandN then (a, id) else (a, b);
    20     fun tree (XML.Elem ((a, atts), ts)) = XML.Elem ((a, map attribute atts), map tree ts)
    21       | tree text = text;
    22   in map tree end;
    23 
    24 fun command_positions_yxml id =
    25   YXML.string_of_body o command_positions id o YXML.parse_body;
    26 
    27 end;