1.1 --- a/Admin/isatest/annomaly.ML Sat Aug 29 10:50:04 2009 +0200
1.2 +++ b/Admin/isatest/annomaly.ML Sat Aug 29 12:01:25 2009 +0200
1.3 @@ -20,7 +20,7 @@
1.4 val isabelleHome =
1.5 case OS.Process.getEnv "ISABELLE_HOME"
1.6 of NONE => OS.FileSys.getDir ()
1.7 - | SOME home => mkAbsolute home
1.8 + | SOME home => mkAbsolute home
1.9
1.10 fun noparent [] = []
1.11 | noparent (n :: ns) =
1.12 @@ -33,12 +33,12 @@
1.13
1.14 fun rewrite defPrefix name =
1.15 let val abs = mkAbsolute name
1.16 - val rel = OS.Path.mkRelative { path = abs, relativeTo = isabelleHome }
1.17 - val exists = (OS.FileSys.access(abs, nil)
1.18 - handle OS.SysErr _ => false)
1.19 + val rel = OS.Path.mkRelative { path = abs, relativeTo = isabelleHome }
1.20 + val exists = (OS.FileSys.access(abs, nil)
1.21 + handle OS.SysErr _ => false)
1.22 in if exists andalso rel <> ""
1.23 - then isabellePath (toArcs rel)
1.24 - else defPrefix @ noparent (toArcs name)
1.25 + then isabellePath (toArcs rel)
1.26 + else defPrefix @ noparent (toArcs name)
1.27 end handle OS.Path.Path => defPrefix @ noparent (toArcs name)
1.28
1.29 in
1.30 @@ -49,10 +49,10 @@
1.31 (* should we have different files for different line numbers? *
1.32 val arcs = if line <= 1 then arcs
1.33 else arcs @ [ "l." ^ Int.toString line ]
1.34 - *)
1.35 - val arcs = if t = "structure Isabelle =\nstruct\nend;"
1.36 - andalso name = "ML"
1.37 - then ["empty_Isabelle", "empty" ] else arcs
1.38 + *)
1.39 + val arcs = if t = "structure Isabelle =\nstruct\nend;"
1.40 + andalso name = "ML"
1.41 + then ["empty_Isabelle", "empty" ] else arcs
1.42 val _ = AnnoMaLy.nameNextStream arcs
1.43 in smlnj_use_text tune str_of_pos name_space (line, name) p v t end;
1.44