equal
deleted
inserted
replaced
2 |
2 |
3 local |
3 local |
4 |
4 |
5 val smlnj_use_text = use_text |
5 val smlnj_use_text = use_text |
6 |
6 |
7 fun strip ([], name, _) = name |
7 fun strip ([], "src" :: name, _) = name |
8 | strip (["Distribution"], name, _) = name |
8 | strip (["Distribution"], name, _) = name |
|
9 | strip ([], name, _) = name |
9 | strip (h1 :: t1, h2 :: t2, def) = |
10 | strip (h1 :: t1, h2 :: t2, def) = |
10 if h1 = h2 then strip (t1, t2, def) else def |
11 if h1 = h2 then strip (t1, t2, def) else def |
11 |
12 |
12 fun rewrite (NONE, name) = "use_text" :: name |
13 fun rewrite (NONE, name) = "use_text" :: name |
13 | rewrite (SOME home, name) = |
14 | rewrite (SOME home, name) = |