equal
deleted
inserted
replaced
67 val exists: ('a -> bool) -> 'a list -> bool |
67 val exists: ('a -> bool) -> 'a list -> bool |
68 val forall: ('a -> bool) -> 'a list -> bool |
68 val forall: ('a -> bool) -> 'a list -> bool |
69 val set: bool ref -> bool |
69 val set: bool ref -> bool |
70 val reset: bool ref -> bool |
70 val reset: bool ref -> bool |
71 val toggle: bool ref -> bool |
71 val toggle: bool ref -> bool |
|
72 val change: 'a ref -> ('a -> 'a) -> unit |
72 val setmp: 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c |
73 val setmp: 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c |
73 |
74 |
74 (*lists*) |
75 (*lists*) |
75 exception LIST of string |
76 exception LIST of string |
76 val null: 'a list -> bool |
77 val null: 'a list -> bool |
390 |
391 |
391 fun set flag = (flag := true; true); |
392 fun set flag = (flag := true; true); |
392 fun reset flag = (flag := false; false); |
393 fun reset flag = (flag := false; false); |
393 fun toggle flag = (flag := not (! flag); ! flag); |
394 fun toggle flag = (flag := not (! flag); ! flag); |
394 |
395 |
|
396 fun change r f = r := f (! r); |
|
397 |
395 (*temporarily set flag, handling errors*) |
398 (*temporarily set flag, handling errors*) |
396 fun setmp flag value f x = |
399 fun setmp flag value f x = |
397 let |
400 let |
398 val orig_value = ! flag; |
401 val orig_value = ! flag; |
399 fun return y = (flag := orig_value; y); |
402 fun return y = (flag := orig_value; y); |
723 fun untabify chs = |
726 fun untabify chs = |
724 let |
727 let |
725 val tab_width = 8; |
728 val tab_width = 8; |
726 |
729 |
727 fun untab (_, "\n") = (0, ["\n"]) |
730 fun untab (_, "\n") = (0, ["\n"]) |
728 | untab (pos, "\t") = let val d = tab_width - (pos mod tab_width) in (pos + d, replicate d " ") end |
731 | untab (pos, "\t") = |
|
732 let val d = tab_width - (pos mod tab_width) in (pos + d, replicate d " ") end |
729 | untab (pos, c) = (pos + 1, [c]); |
733 | untab (pos, c) = (pos + 1, [c]); |
730 in |
734 in |
731 if not (exists (equal "\t") chs) then chs |
735 if not (exists (equal "\t") chs) then chs |
732 else flat (#2 (foldl_map untab (0, chs))) |
736 else flat (#2 (foldl_map untab (0, chs))) |
733 end; |
737 end; |