Admin/isatest/annomaly.ML
author urbanc
Thu, 13 Sep 2007 23:58:38 +0200
changeset 24571 a6d0428dea8e
parent 23207 769f7762f531
child 24611 1f92518fbabe
permissions -rw-r--r--
some cleaning up to do with contexts
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
23207
769f7762f531 cosmetic
webertj
parents: 22489
diff changeset
     1
(*  Title:      Admin/isatest/annomaly.ML
769f7762f531 cosmetic
webertj
parents: 22489
diff changeset
     2
    ID:         $Id$
769f7762f531 cosmetic
webertj
parents: 22489
diff changeset
     3
    Author:     Martin von Gagern <martin@von-gagern.net>
769f7762f531 cosmetic
webertj
parents: 22489
diff changeset
     4
*)
769f7762f531 cosmetic
webertj
parents: 22489
diff changeset
     5
769f7762f531 cosmetic
webertj
parents: 22489
diff changeset
     6
use "ML-Systems/smlnj.ML";
22488
415098eece94 Changed AnnoMaLy build process from CVS to tarball sources.
gagern
parents:
diff changeset
     7
415098eece94 Changed AnnoMaLy build process from CVS to tarball sources.
gagern
parents:
diff changeset
     8
local
415098eece94 Changed AnnoMaLy build process from CVS to tarball sources.
gagern
parents:
diff changeset
     9
415098eece94 Changed AnnoMaLy build process from CVS to tarball sources.
gagern
parents:
diff changeset
    10
  val smlnj_use_text = use_text
415098eece94 Changed AnnoMaLy build process from CVS to tarball sources.
gagern
parents:
diff changeset
    11
22489
52a5277d0489 Better documentation path rewriting for src dir, used in tarball build.
gagern
parents: 22488
diff changeset
    12
  fun strip ([], "src" :: name, _) = name
22488
415098eece94 Changed AnnoMaLy build process from CVS to tarball sources.
gagern
parents:
diff changeset
    13
    | strip (["Distribution"], name, _) = name
22489
52a5277d0489 Better documentation path rewriting for src dir, used in tarball build.
gagern
parents: 22488
diff changeset
    14
    | strip ([], name, _) = name
22488
415098eece94 Changed AnnoMaLy build process from CVS to tarball sources.
gagern
parents:
diff changeset
    15
    | strip (h1 :: t1, h2 :: t2, def) =
415098eece94 Changed AnnoMaLy build process from CVS to tarball sources.
gagern
parents:
diff changeset
    16
      if h1 = h2 then strip (t1, t2, def) else def
415098eece94 Changed AnnoMaLy build process from CVS to tarball sources.
gagern
parents:
diff changeset
    17
415098eece94 Changed AnnoMaLy build process from CVS to tarball sources.
gagern
parents:
diff changeset
    18
  fun rewrite (NONE, name) = "use_text" :: name
415098eece94 Changed AnnoMaLy build process from CVS to tarball sources.
gagern
parents:
diff changeset
    19
    | rewrite (SOME home, name) =
415098eece94 Changed AnnoMaLy build process from CVS to tarball sources.
gagern
parents:
diff changeset
    20
      strip (#arcs (OS.Path.fromString home), name, "use_text" :: name)
415098eece94 Changed AnnoMaLy build process from CVS to tarball sources.
gagern
parents:
diff changeset
    21
415098eece94 Changed AnnoMaLy build process from CVS to tarball sources.
gagern
parents:
diff changeset
    22
in
415098eece94 Changed AnnoMaLy build process from CVS to tarball sources.
gagern
parents:
diff changeset
    23
23207
769f7762f531 cosmetic
webertj
parents: 22489
diff changeset
    24
  fun use_text name p v t =
769f7762f531 cosmetic
webertj
parents: 22489
diff changeset
    25
    let val name = case name of "" => "unnamed" | name => name
769f7762f531 cosmetic
webertj
parents: 22489
diff changeset
    26
        val arcs = rewrite (OS.Process.getEnv "ISABELLE_HOME",
769f7762f531 cosmetic
webertj
parents: 22489
diff changeset
    27
                            #arcs (OS.Path.fromString name))
769f7762f531 cosmetic
webertj
parents: 22489
diff changeset
    28
        val _    = AnnoMaLy.nameNextStream ("isabelle" :: arcs)
769f7762f531 cosmetic
webertj
parents: 22489
diff changeset
    29
    in  smlnj_use_text name p v t  end
22488
415098eece94 Changed AnnoMaLy build process from CVS to tarball sources.
gagern
parents:
diff changeset
    30
415098eece94 Changed AnnoMaLy build process from CVS to tarball sources.
gagern
parents:
diff changeset
    31
end;