src/Pure/proof_general.ML
changeset 16896 db2defb39f4c
parent 16824 c889f499911c
child 16958 1b4a3110c64a
equal deleted inserted replaced
16895:df67fc190e06 16896:db2defb39f4c
   174   fun assemble_pgips pgips =
   174   fun assemble_pgips pgips =
   175     XML.element
   175     XML.element
   176       "pgip"
   176       "pgip"
   177       ([("tag",    pgip_tag),
   177       ([("tag",    pgip_tag),
   178         ("class",  pgip_class),
   178         ("class",  pgip_class),
       
   179 	("seq",    string_of_int (pgip_serial())),
   179         ("id",     !pgip_id)] @
   180         ("id",     !pgip_id)] @
   180        if_none (Option.map (single o (pair "destid")) (! pgip_refid)) [] @
   181        if_none (Option.map (single o (pair "destid")) (! pgip_refid)) [] @
   181        (* destid=refid since Isabelle only communicates back to sender,
   182        (* destid=refid since Isabelle only communicates back to sender,
   182           so we may omit refid from attributes.
   183           so we may omit refid from attributes.
   183        if_none (Option.map (single o (pair "refid"))  (! pgip_refid)) [] @
   184        if_none (Option.map (single o (pair "refid"))  (! pgip_refid)) [] @