1.1 --- a/Admin/isatest/annomaly.ML	Mon Jul 23 18:52:10 2012 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,69 +0,0 @@
     1.4 -(*  Title:      Admin/isatest/annomaly.ML
     1.5 -    Author:     Martin von Gagern <martin@von-gagern.net>
     1.6 -*)
     1.7 -
     1.8 -use "ML-Systems/smlnj.ML";
     1.9 -
    1.10 -local
    1.11 -
    1.12 -  val smlnj_use_text = use_text
    1.13 -
    1.14 -  val smlnj_use_file = use_file
    1.15 -
    1.16 -  val smlnj_forget_structure = forget_structure
    1.17 -
    1.18 -  fun mkAbsolute path =
    1.19 -      OS.Path.mkAbsolute { path = path, relativeTo = OS.FileSys.getDir () }
    1.20 -
    1.21 -  fun toArcs path = #arcs (OS.Path.fromString path)
    1.22 -
    1.23 -  val isabelleHome =
    1.24 -      case OS.Process.getEnv "ISABELLE_HOME"
    1.25 -       of  NONE => OS.FileSys.getDir ()
    1.26 -         | SOME home => mkAbsolute home
    1.27 -
    1.28 -  fun noparent [] = []
    1.29 -    | noparent (n :: ns) =
    1.30 -      if n = OS.Path.parentArc then noparent ns else n :: noparent ns
    1.31 -
    1.32 -  fun isabellePath [] = []
    1.33 -    | isabellePath ("src" :: name) = "Isabelle" :: name
    1.34 -    | isabellePath (name as (n :: ns)) =
    1.35 -      if n = OS.Path.parentArc then noparent ns else "Isabelle" :: name
    1.36 -
    1.37 -  fun rewrite defPrefix name =
    1.38 -      let val abs = mkAbsolute name
    1.39 -          val rel = OS.Path.mkRelative { path = abs, relativeTo = isabelleHome }
    1.40 -          val exists = (OS.FileSys.access(abs, nil)
    1.41 -                        handle OS.SysErr _ => false)
    1.42 -      in  if exists andalso rel <> ""
    1.43 -          then isabellePath (toArcs rel)
    1.44 -          else defPrefix @ noparent (toArcs name)
    1.45 -      end handle OS.Path.Path => defPrefix @ noparent (toArcs name)
    1.46 -
    1.47 -in
    1.48 -
    1.49 -  fun use_text tune str_of_pos name_space (line, name) p v t =
    1.50 -    let val name = case name of "" => "unnamed" | name => name
    1.51 -        val arcs = rewrite ["use_text"] name
    1.52 -        (* should we have different files for different line numbers? *
    1.53 -        val arcs = if line <= 1 then arcs
    1.54 -                   else arcs @ [ "l." ^ Int.toString line ]
    1.55 -        *)
    1.56 -        val arcs = if t = "structure Isabelle =\nstruct\nend;"
    1.57 -                      andalso name = "ML"
    1.58 -                   then ["empty_Isabelle", "empty" ] else arcs
    1.59 -        val _    = AnnoMaLy.nameNextStream arcs
    1.60 -    in  smlnj_use_text tune str_of_pos name_space (line, name) p v t  end;
    1.61 -
    1.62 -  fun use_file tune str_of_pos name_space output verbose name =
    1.63 -      let val arcs = rewrite ["use_file"] name
    1.64 -          val _    = AnnoMaLy.nameNextStream arcs
    1.65 -      in  smlnj_use_file tune str_of_pos name_space output verbose name  end;
    1.66 -
    1.67 -  fun forget_structure name =
    1.68 -      let val arcs = [ "forget_structure", name ]
    1.69 -          val _    = AnnoMaLy.nameNextStream arcs
    1.70 -      in  smlnj_forget_structure name  end;
    1.71 -
    1.72 -end;