src/Pure/PIDE/protocol.scala
changeset 59085 08a6901eb035
parent 58015 2777096e0adf
child 59184 830bb7ddb3ab
     1.1 --- a/src/Pure/PIDE/protocol.scala	Wed Dec 03 15:22:27 2014 +0100
     1.2 +++ b/src/Pure/PIDE/protocol.scala	Wed Dec 03 20:45:20 2014 +0100
     1.3 @@ -392,10 +392,21 @@
     1.4            { case Exn.Res((a, b)) =>
     1.5                (Nil, pair(string, option(string))((a.node, b.map(p => p._1.toString)))) },
     1.6            { case Exn.Exn(e) => (Nil, string(Exn.message(e))) }))
     1.7 +
     1.8        YXML.string_of_body(list(encode_blob)(command.blobs))
     1.9      }
    1.10 +
    1.11 +    val toks = command.span.content
    1.12 +    val toks_yxml =
    1.13 +    { import XML.Encode._
    1.14 +      val encode_tok: T[Token] =
    1.15 +        (tok => pair(int, int)((tok.kind.id, Symbol.iterator(tok.source).length)))
    1.16 +      YXML.string_of_body(list(encode_tok)(toks))
    1.17 +    }
    1.18 +
    1.19      protocol_command("Document.define_command",
    1.20 -      Document_ID(command.id), encode(command.name), blobs_yxml, encode(command.source))
    1.21 +      (Document_ID(command.id) :: encode(command.name) :: blobs_yxml :: toks_yxml ::
    1.22 +        toks.map(tok => encode(tok.source))): _*)
    1.23    }
    1.24  
    1.25