changeset 40627 | becf5d5187cc |
parent 40564 | 6827505e96e1 |
child 40721 | e5089e903e39 |
child 40731 | 4e60c7348096 |
40626:d86540f6ea0d | 40627:becf5d5187cc |
---|---|
667 else (num, c :: cs); |
667 else (num, c :: cs); |
668 in scan (0, cs) end; |
668 in scan (0, cs) end; |
669 |
669 |
670 val read_int = read_radix_int 10; |
670 val read_int = read_radix_int 10; |
671 |
671 |
672 fun oct_char s = chr (#1 (read_radix_int 8 (explode s))); |
672 fun oct_char s = chr (#1 (read_radix_int 8 (raw_explode s))); |
673 |
673 |
674 |
674 |
675 |
675 |
676 (** reals **) |
676 (** reals **) |
677 |
677 |