equal
deleted
inserted
replaced
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)) [] @ |