equal
deleted
inserted
replaced
67 val has_junk = |
67 val has_junk = |
68 exists (fn s => not (Symbol.is_digit s) andalso s <> ".") o raw_explode (* FIXME Symbol.explode (?) *) |
68 exists (fn s => not (Symbol.is_digit s) andalso s <> ".") o raw_explode (* FIXME Symbol.explode (?) *) |
69 |
69 |
70 fun parse_time name s = |
70 fun parse_time name s = |
71 let val secs = if has_junk s then NONE else Real.fromString s in |
71 let val secs = if has_junk s then NONE else Real.fromString s in |
72 if is_none secs orelse Real.< (the secs, 0.0) then |
72 if is_none secs orelse the secs < 0.0 then |
73 error ("Parameter " ^ quote name ^ " must be assigned a nonnegative number of seconds \ |
73 error ("Parameter " ^ quote name ^ " must be assigned a nonnegative number of seconds \ |
74 \(e.g., \"60\", \"0.5\") or \"none\".") |
74 \(e.g., \"60\", \"0.5\") or \"none\".") |
75 else |
75 else |
76 seconds (the secs) |
76 seconds (the secs) |
77 end |
77 end |