1.1 --- a/Admin/isatest/annomaly.ML	Mon Mar 31 23:08:55 2008 +0200
     1.2 +++ b/Admin/isatest/annomaly.ML	Mon Mar 31 23:29:36 2008 +0200
     1.3 @@ -9,23 +9,62 @@
     1.4  
     1.5    val smlnj_use_text = use_text
     1.6  
     1.7 -  fun strip ([], "src" :: name, _) = name
     1.8 -    | strip (["Distribution"], name, _) = name
     1.9 -    | strip ([], name, _) = name
    1.10 -    | strip (h1 :: t1, h2 :: t2, def) =
    1.11 -      if h1 = h2 then strip (t1, t2, def) else def
    1.12 +  val smlnj_use_file = use_file
    1.13  
    1.14 -  fun rewrite (NONE, name) = "use_text" :: name
    1.15 -    | rewrite (SOME home, name) =
    1.16 -      strip (#arcs (OS.Path.fromString home), name, "use_text" :: name)
    1.17 +  val smlnj_forget_structure = forget_structure
    1.18 +
    1.19 +  fun mkAbsolute path =
    1.20 +      OS.Path.mkAbsolute { path = path, relativeTo = OS.FileSys.getDir () }
    1.21 +
    1.22 +  fun toArcs path = #arcs (OS.Path.fromString path)
    1.23 +
    1.24 +  val isabelleHome =
    1.25 +      case OS.Process.getEnv "ISABELLE_HOME"
    1.26 +       of  NONE => OS.FileSys.getDir ()
    1.27 +	 | SOME home => mkAbsolute home
    1.28 +
    1.29 +  fun noparent [] = []
    1.30 +    | noparent (n :: ns) =
    1.31 +      if n = OS.Path.parentArc then noparent ns else n :: noparent ns
    1.32 +
    1.33 +  fun isabellePath [] = []
    1.34 +    | isabellePath ("src" :: name) = "Isabelle" :: name
    1.35 +    | isabellePath (name as (n :: ns)) =
    1.36 +      if n = OS.Path.parentArc then noparent ns else "Isabelle" :: name
    1.37 +
    1.38 +  fun rewrite defPrefix name =
    1.39 +      let val abs = mkAbsolute name
    1.40 +	  val rel = OS.Path.mkRelative { path = abs, relativeTo = isabelleHome }
    1.41 +	  val exists = (OS.FileSys.access(abs, nil)
    1.42 +			handle OS.SysErr _ => false)
    1.43 +      in  if exists andalso rel <> ""
    1.44 +	  then isabellePath (toArcs rel)
    1.45 +	  else defPrefix @ noparent (toArcs name)
    1.46 +      end handle OS.Path.Path => defPrefix @ noparent (toArcs name)
    1.47  
    1.48  in
    1.49  
    1.50 -  fun use_text tune name p v t =
    1.51 +  fun use_text tune (line, name) p v t =
    1.52      let val name = case name of "" => "unnamed" | name => name
    1.53 -        val arcs = rewrite (OS.Process.getEnv "ISABELLE_HOME",
    1.54 -                            #arcs (OS.Path.fromString name))
    1.55 -        val _    = AnnoMaLy.nameNextStream ("isabelle" :: arcs)
    1.56 -    in  smlnj_use_text tune name p v t  end
    1.57 +        val arcs = rewrite ["use_text"] name
    1.58 +        (* should we have different files for different line numbers? *
    1.59 +        val arcs = if line <= 1 then arcs
    1.60 +                   else arcs @ [ "l." ^ Int.toString line ]
    1.61 +	*)
    1.62 +	val arcs = if t = "structure Isabelle =\nstruct\nend;"
    1.63 +		      andalso name = "ML"
    1.64 +		   then ["empty_Isabelle", "empty" ] else arcs
    1.65 +        val _    = AnnoMaLy.nameNextStream arcs
    1.66 +    in  smlnj_use_text tune (line, name) p v t  end;
    1.67 +
    1.68 +  fun use_file tune output verbose name =
    1.69 +      let val arcs = rewrite ["use_file"] name
    1.70 +          val _    = AnnoMaLy.nameNextStream arcs
    1.71 +      in  smlnj_use_file tune output verbose name  end;
    1.72 +
    1.73 +  fun forget_structure name =
    1.74 +      let val arcs = [ "forget_structure", name ]
    1.75 +          val _    = AnnoMaLy.nameNextStream arcs
    1.76 +      in  smlnj_forget_structure name  end;
    1.77  
    1.78  end;