Admin/isatest/annomaly.ML
changeset 32449 696d64ed85da
parent 31582 4753c317d5c1
     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