501 |
501 |
502 (** preferences **) |
502 (** preferences **) |
503 |
503 |
504 local |
504 local |
505 |
505 |
|
506 fun signed_string_of_int i = |
|
507 if i < 0 then "-" ^ string_of_int (~ i) else string_of_int i; |
|
508 |
506 val pgipint = XML.element "pgipint" [] []; |
509 val pgipint = XML.element "pgipint" [] []; |
507 val pgipnat = XML.element "pgipint" [("min", "0")] []; |
510 val pgipnat = XML.element "pgipint" [("min", "0")] []; |
508 fun pgipnatmax max = XML.element "pgipint" [("min", "0"), ("max", string_of_int max)] []; |
511 fun pgipnatmax max = XML.element "pgipint" [("min", "0"), ("max", string_of_int max)] []; |
509 val pgipbool = XML.element "pgipbool" [] []; |
512 val pgipbool = XML.element "pgipbool" [] []; |
510 |
513 |
511 fun with_default f = (f (), f); |
514 fun with_default f = (f (), f); |
512 |
515 |
513 in |
516 in |
514 |
517 |
515 fun int_option r = (pgipint, |
518 fun int_option r = (pgipint, |
516 with_default (fn () => string_of_int (! r)), |
519 with_default (fn () => signed_string_of_int (! r)), |
517 (fn s => (case Syntax.read_int s of |
520 (fn s => (case Syntax.read_int s of |
518 NONE => error ("int_option: illegal value: " ^ s) |
521 NONE => error ("int_option: illegal value: " ^ s) |
519 | SOME i => r := i))); |
522 | SOME i => r := i))); |
520 |
523 |
521 fun nat_option r = (pgipnat, |
524 fun nat_option r = (pgipnat, |