tuned protocol -- resolve command positions in ML;
authorwenzelm
Mon Mar 16 11:30:54 2015 +0100 (2015-03-16)
changeset 59714ae322325adbb
parent 59713 6da3efec20ca
child 59715 4f0d0e4ad68d
tuned protocol -- resolve command positions in ML;
src/Pure/PIDE/protocol.ML
src/Pure/PIDE/protocol.scala
src/Pure/PIDE/protocol_message.ML
src/Pure/ROOT
src/Pure/ROOT.ML
     1.1 --- a/src/Pure/PIDE/protocol.ML	Mon Mar 16 11:07:56 2015 +0100
     1.2 +++ b/src/Pure/PIDE/protocol.ML	Mon Mar 16 11:30:54 2015 +0100
     1.3 @@ -32,11 +32,15 @@
     1.4        let
     1.5          val (blobs, blobs_index) =
     1.6            YXML.parse_body blobs_yxml |>
     1.7 -            let open XML.Decode in
     1.8 +            let
     1.9 +              val message =
    1.10 +                YXML.string_of_body o Protocol_Message.command_positions id;
    1.11 +              open XML.Decode;
    1.12 +            in
    1.13                pair
    1.14                  (list (variant
    1.15                   [fn ([], a) => Exn.Res (pair string (option string) a),
    1.16 -                  fn ([], a) => Exn.Exn (ERROR (YXML.string_of_body a))]))
    1.17 +                  fn ([], a) => Exn.Exn (ERROR (message a))]))
    1.18                  int
    1.19              end;
    1.20          val toks =
     2.1 --- a/src/Pure/PIDE/protocol.scala	Mon Mar 16 11:07:56 2015 +0100
     2.2 +++ b/src/Pure/PIDE/protocol.scala	Mon Mar 16 11:30:54 2015 +0100
     2.3 @@ -307,29 +307,6 @@
     2.4    def define_blob(digest: SHA1.Digest, bytes: Bytes): Unit =
     2.5      protocol_command_bytes("Document.define_blob", Bytes(digest.toString), bytes)
     2.6  
     2.7 -  private def resolve_id(id: String, body: XML.Body): XML.Body =
     2.8 -  {
     2.9 -    def resolve_property(p: (String, String)): (String, String) =
    2.10 -      if (p._1 == Markup.ID && p._2 == Markup.COMMAND) (Markup.ID, id) else p
    2.11 -
    2.12 -    def resolve_markup(markup: Markup): Markup =
    2.13 -      Markup(markup.name, markup.properties.map(resolve_property))
    2.14 -
    2.15 -    def resolve_tree(t: XML.Tree): XML.Tree =
    2.16 -      t match {
    2.17 -        case XML.Wrapped_Elem(markup, ts1, ts2) =>
    2.18 -          XML.Wrapped_Elem(resolve_markup(markup), ts1.map(resolve_tree _), ts2.map(resolve_tree _))
    2.19 -        case XML.Elem(markup, ts) =>
    2.20 -          XML.Elem(resolve_markup(markup), ts.map(resolve_tree _))
    2.21 -        case text => text
    2.22 -      }
    2.23 -    body.map(resolve_tree _)
    2.24 -  }
    2.25 -
    2.26 -  private def resolve_id(id: String, s: String): XML.Body =
    2.27 -    try { resolve_id(id, YXML.parse_body(s)) }
    2.28 -    catch { case ERROR(_) => XML.Encode.string(s) }
    2.29 -
    2.30    def define_command(command: Command)
    2.31    {
    2.32      val blobs_yxml =
    2.33 @@ -338,7 +315,7 @@
    2.34          variant(List(
    2.35            { case Exn.Res((a, b)) =>
    2.36                (Nil, pair(string, option(string))((a.node, b.map(p => p._1.toString)))) },
    2.37 -          { case Exn.Exn(e) => (Nil, resolve_id(command.id.toString, Exn.message(e))) }))
    2.38 +          { case Exn.Exn(e) => (Nil, string(Exn.message(e))) }))
    2.39  
    2.40        YXML.string_of_body(pair(list(encode_blob), int)(command.blobs, command.blobs_index))
    2.41      }
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Pure/PIDE/protocol_message.ML	Mon Mar 16 11:30:54 2015 +0100
     3.3 @@ -0,0 +1,27 @@
     3.4 +(*  Title:      Pure/PIDE/protocol_message.ML
     3.5 +    Author:     Makarius
     3.6 +
     3.7 +Auxiliary operations on protocol messages.
     3.8 +*)
     3.9 +
    3.10 +signature PROTOCOL_MESSAGE =
    3.11 +sig
    3.12 +  val command_positions: string -> XML.body -> XML.body
    3.13 +  val command_positions_yxml: string -> string -> string
    3.14 +end;
    3.15 +
    3.16 +structure Protocol_Message: PROTOCOL_MESSAGE =
    3.17 +struct
    3.18 +
    3.19 +fun command_positions id =
    3.20 +  let
    3.21 +    fun attribute (a, b) =
    3.22 +      if a = Markup.idN andalso b = Markup.commandN then (a, id) else (a, b);
    3.23 +    fun tree (XML.Elem ((a, atts), ts)) = XML.Elem ((a, map attribute atts), map tree ts)
    3.24 +      | tree text = text;
    3.25 +  in map tree end;
    3.26 +
    3.27 +fun command_positions_yxml id =
    3.28 +  YXML.string_of_body o command_positions id o YXML.parse_body;
    3.29 +
    3.30 +end;
     4.1 --- a/src/Pure/ROOT	Mon Mar 16 11:07:56 2015 +0100
     4.2 +++ b/src/Pure/ROOT	Mon Mar 16 11:30:54 2015 +0100
     4.3 @@ -172,6 +172,7 @@
     4.4      "PIDE/execution.ML"
     4.5      "PIDE/markup.ML"
     4.6      "PIDE/protocol.ML"
     4.7 +    "PIDE/protocol_message.ML"
     4.8      "PIDE/query_operation.ML"
     4.9      "PIDE/resources.ML"
    4.10      "PIDE/session.ML"
     5.1 --- a/src/Pure/ROOT.ML	Mon Mar 16 11:07:56 2015 +0100
     5.2 +++ b/src/Pure/ROOT.ML	Mon Mar 16 11:30:54 2015 +0100
     5.3 @@ -310,6 +310,7 @@
     5.4  use "PIDE/resources.ML";
     5.5  use "Thy/thy_info.ML";
     5.6  use "PIDE/session.ML";
     5.7 +use "PIDE/protocol_message.ML";
     5.8  use "PIDE/document.ML";
     5.9  
    5.10  (*theory and proof operations*)