webertj@23207
|
1 |
(* Title: Admin/isatest/annomaly.ML
|
webertj@23207
|
2 |
ID: $Id$
|
webertj@23207
|
3 |
Author: Martin von Gagern <martin@von-gagern.net>
|
webertj@23207
|
4 |
*)
|
webertj@23207
|
5 |
|
webertj@23207
|
6 |
use "ML-Systems/smlnj.ML";
|
gagern@22488
|
7 |
|
gagern@22488
|
8 |
local
|
gagern@22488
|
9 |
|
gagern@22488
|
10 |
val smlnj_use_text = use_text
|
gagern@22488
|
11 |
|
gagern@22489
|
12 |
fun strip ([], "src" :: name, _) = name
|
gagern@22488
|
13 |
| strip (["Distribution"], name, _) = name
|
gagern@22489
|
14 |
| strip ([], name, _) = name
|
gagern@22488
|
15 |
| strip (h1 :: t1, h2 :: t2, def) =
|
gagern@22488
|
16 |
if h1 = h2 then strip (t1, t2, def) else def
|
gagern@22488
|
17 |
|
gagern@22488
|
18 |
fun rewrite (NONE, name) = "use_text" :: name
|
gagern@22488
|
19 |
| rewrite (SOME home, name) =
|
gagern@22488
|
20 |
strip (#arcs (OS.Path.fromString home), name, "use_text" :: name)
|
gagern@22488
|
21 |
|
gagern@22488
|
22 |
in
|
gagern@22488
|
23 |
|
webertj@23207
|
24 |
fun use_text name p v t =
|
webertj@23207
|
25 |
let val name = case name of "" => "unnamed" | name => name
|
webertj@23207
|
26 |
val arcs = rewrite (OS.Process.getEnv "ISABELLE_HOME",
|
webertj@23207
|
27 |
#arcs (OS.Path.fromString name))
|
webertj@23207
|
28 |
val _ = AnnoMaLy.nameNextStream ("isabelle" :: arcs)
|
webertj@23207
|
29 |
in smlnj_use_text name p v t end
|
gagern@22488
|
30 |
|
gagern@22488
|
31 |
end;
|