equal
deleted
inserted
replaced
78 | NONE => state)); |
78 | NONE => state)); |
79 |
79 |
80 |
80 |
81 (* main manager thread -- only one may exist *) |
81 (* main manager thread -- only one may exist *) |
82 |
82 |
83 val min_wait_time = Time.fromMilliseconds 300; |
83 val min_wait_time = seconds 0.3; |
84 val max_wait_time = Time.fromSeconds 10; |
84 val max_wait_time = seconds 10.0; |
85 |
85 |
86 fun replace_all bef aft = |
86 fun replace_all bef aft = |
87 let |
87 let |
88 fun aux seen "" = String.implode (rev seen) |
88 fun aux seen "" = String.implode (rev seen) |
89 | aux seen s = |
89 | aux seen s = |