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";
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;