Changed AnnoMaLy build process from CVS to tarball sources.
Moved annomaly.ML from the official sources to the isatest directory.
1 use "ML-Systems/smlnj.ML";
5 val smlnj_use_text = use_text
7 fun strip ([], name, _) = name
8 | strip (["Distribution"], name, _) = name
9 | strip (h1 :: t1, h2 :: t2, def) =
10 if h1 = h2 then strip (t1, t2, def) else def
12 fun rewrite (NONE, name) = "use_text" :: name
13 | rewrite (SOME home, name) =
14 strip (#arcs (OS.Path.fromString home), name, "use_text" :: name)
18 fun use_text name p v t =
19 let val name = case name of "" => "unnamed" | name => name
20 val arcs = rewrite (OS.Process.getEnv "ISABELLE_HOME",
21 #arcs (OS.Path.fromString name))
22 val _ = AnnoMaLy.nameNextStream ("isabelle" :: arcs)
23 in smlnj_use_text name p v t