equal
deleted
inserted
replaced
213 (case XML.parse_string s of |
213 (case XML.parse_string s of |
214 SOME s => s |
214 SOME s => s |
215 | NONE => raise PGIP ("Expected a non-empty string: "^s)) |
215 | NONE => raise PGIP ("Expected a non-empty string: "^s)) |
216 handle _ => raise PGIP ("Invalid XML string syntax: "^s) |
216 handle _ => raise PGIP ("Invalid XML string syntax: "^s) |
217 |
217 |
218 fun int_to_pgstring i = |
218 val int_to_pgstring = signed_string_of_int |
219 if i < 0 then "-" ^ string_of_int (~ i) else string_of_int i |
|
220 |
219 |
221 fun string_to_pgstring s = XML.text s |
220 fun string_to_pgstring s = XML.text s |
222 |
221 |
223 fun bool_to_pgstring b = if b then "true" else "false" |
222 fun bool_to_pgstring b = if b then "true" else "false" |
224 |
223 |