src/Pure/PIDE/protocol_message.ML
author wenzelm
Tue, 07 Mar 2017 17:56:57 +0100
changeset 65144 b5782e996651
parent 59714 ae322325adbb
child 70907 7e3f25a0cee4
permissions -rw-r--r--
more generic colors;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
59714
ae322325adbb tuned protocol -- resolve command positions in ML;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/PIDE/protocol_message.ML
ae322325adbb tuned protocol -- resolve command positions in ML;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
ae322325adbb tuned protocol -- resolve command positions in ML;
wenzelm
parents:
diff changeset
     3
ae322325adbb tuned protocol -- resolve command positions in ML;
wenzelm
parents:
diff changeset
     4
Auxiliary operations on protocol messages.
ae322325adbb tuned protocol -- resolve command positions in ML;
wenzelm
parents:
diff changeset
     5
*)
ae322325adbb tuned protocol -- resolve command positions in ML;
wenzelm
parents:
diff changeset
     6
ae322325adbb tuned protocol -- resolve command positions in ML;
wenzelm
parents:
diff changeset
     7
signature PROTOCOL_MESSAGE =
ae322325adbb tuned protocol -- resolve command positions in ML;
wenzelm
parents:
diff changeset
     8
sig
ae322325adbb tuned protocol -- resolve command positions in ML;
wenzelm
parents:
diff changeset
     9
  val command_positions: string -> XML.body -> XML.body
ae322325adbb tuned protocol -- resolve command positions in ML;
wenzelm
parents:
diff changeset
    10
  val command_positions_yxml: string -> string -> string
ae322325adbb tuned protocol -- resolve command positions in ML;
wenzelm
parents:
diff changeset
    11
end;
ae322325adbb tuned protocol -- resolve command positions in ML;
wenzelm
parents:
diff changeset
    12
ae322325adbb tuned protocol -- resolve command positions in ML;
wenzelm
parents:
diff changeset
    13
structure Protocol_Message: PROTOCOL_MESSAGE =
ae322325adbb tuned protocol -- resolve command positions in ML;
wenzelm
parents:
diff changeset
    14
struct
ae322325adbb tuned protocol -- resolve command positions in ML;
wenzelm
parents:
diff changeset
    15
ae322325adbb tuned protocol -- resolve command positions in ML;
wenzelm
parents:
diff changeset
    16
fun command_positions id =
ae322325adbb tuned protocol -- resolve command positions in ML;
wenzelm
parents:
diff changeset
    17
  let
ae322325adbb tuned protocol -- resolve command positions in ML;
wenzelm
parents:
diff changeset
    18
    fun attribute (a, b) =
ae322325adbb tuned protocol -- resolve command positions in ML;
wenzelm
parents:
diff changeset
    19
      if a = Markup.idN andalso b = Markup.commandN then (a, id) else (a, b);
ae322325adbb tuned protocol -- resolve command positions in ML;
wenzelm
parents:
diff changeset
    20
    fun tree (XML.Elem ((a, atts), ts)) = XML.Elem ((a, map attribute atts), map tree ts)
ae322325adbb tuned protocol -- resolve command positions in ML;
wenzelm
parents:
diff changeset
    21
      | tree text = text;
ae322325adbb tuned protocol -- resolve command positions in ML;
wenzelm
parents:
diff changeset
    22
  in map tree end;
ae322325adbb tuned protocol -- resolve command positions in ML;
wenzelm
parents:
diff changeset
    23
ae322325adbb tuned protocol -- resolve command positions in ML;
wenzelm
parents:
diff changeset
    24
fun command_positions_yxml id =
ae322325adbb tuned protocol -- resolve command positions in ML;
wenzelm
parents:
diff changeset
    25
  YXML.string_of_body o command_positions id o YXML.parse_body;
ae322325adbb tuned protocol -- resolve command positions in ML;
wenzelm
parents:
diff changeset
    26
ae322325adbb tuned protocol -- resolve command positions in ML;
wenzelm
parents:
diff changeset
    27
end;