Admin/isatest/annomaly.ML
author nipkow
Sun, 22 Feb 2009 17:25:28 +0100
changeset 30056 0a35bee25c20
parent 28284 2161665a0a5d
child 31582 4753c317d5c1
permissions -rw-r--r--
added lemmas
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
26505
49967f8b1068 Catching up with smlnj.ML 1.47 (use_file), 1.52 (line numbers), 1.53
gagern
parents: 24611
diff changeset
    12
  val smlnj_use_file = use_file
49967f8b1068 Catching up with smlnj.ML 1.47 (use_file), 1.52 (line numbers), 1.53
gagern
parents: 24611
diff changeset
    13
49967f8b1068 Catching up with smlnj.ML 1.47 (use_file), 1.52 (line numbers), 1.53
gagern
parents: 24611
diff changeset
    14
  val smlnj_forget_structure = forget_structure
49967f8b1068 Catching up with smlnj.ML 1.47 (use_file), 1.52 (line numbers), 1.53
gagern
parents: 24611
diff changeset
    15
49967f8b1068 Catching up with smlnj.ML 1.47 (use_file), 1.52 (line numbers), 1.53
gagern
parents: 24611
diff changeset
    16
  fun mkAbsolute path =
49967f8b1068 Catching up with smlnj.ML 1.47 (use_file), 1.52 (line numbers), 1.53
gagern
parents: 24611
diff changeset
    17
      OS.Path.mkAbsolute { path = path, relativeTo = OS.FileSys.getDir () }
49967f8b1068 Catching up with smlnj.ML 1.47 (use_file), 1.52 (line numbers), 1.53
gagern
parents: 24611
diff changeset
    18
49967f8b1068 Catching up with smlnj.ML 1.47 (use_file), 1.52 (line numbers), 1.53
gagern
parents: 24611
diff changeset
    19
  fun toArcs path = #arcs (OS.Path.fromString path)
49967f8b1068 Catching up with smlnj.ML 1.47 (use_file), 1.52 (line numbers), 1.53
gagern
parents: 24611
diff changeset
    20
49967f8b1068 Catching up with smlnj.ML 1.47 (use_file), 1.52 (line numbers), 1.53
gagern
parents: 24611
diff changeset
    21
  val isabelleHome =
49967f8b1068 Catching up with smlnj.ML 1.47 (use_file), 1.52 (line numbers), 1.53
gagern
parents: 24611
diff changeset
    22
      case OS.Process.getEnv "ISABELLE_HOME"
49967f8b1068 Catching up with smlnj.ML 1.47 (use_file), 1.52 (line numbers), 1.53
gagern
parents: 24611
diff changeset
    23
       of  NONE => OS.FileSys.getDir ()
49967f8b1068 Catching up with smlnj.ML 1.47 (use_file), 1.52 (line numbers), 1.53
gagern
parents: 24611
diff changeset
    24
	 | SOME home => mkAbsolute home
22488
415098eece94 Changed AnnoMaLy build process from CVS to tarball sources.
gagern
parents:
diff changeset
    25
26505
49967f8b1068 Catching up with smlnj.ML 1.47 (use_file), 1.52 (line numbers), 1.53
gagern
parents: 24611
diff changeset
    26
  fun noparent [] = []
49967f8b1068 Catching up with smlnj.ML 1.47 (use_file), 1.52 (line numbers), 1.53
gagern
parents: 24611
diff changeset
    27
    | noparent (n :: ns) =
49967f8b1068 Catching up with smlnj.ML 1.47 (use_file), 1.52 (line numbers), 1.53
gagern
parents: 24611
diff changeset
    28
      if n = OS.Path.parentArc then noparent ns else n :: noparent ns
49967f8b1068 Catching up with smlnj.ML 1.47 (use_file), 1.52 (line numbers), 1.53
gagern
parents: 24611
diff changeset
    29
49967f8b1068 Catching up with smlnj.ML 1.47 (use_file), 1.52 (line numbers), 1.53
gagern
parents: 24611
diff changeset
    30
  fun isabellePath [] = []
49967f8b1068 Catching up with smlnj.ML 1.47 (use_file), 1.52 (line numbers), 1.53
gagern
parents: 24611
diff changeset
    31
    | isabellePath ("src" :: name) = "Isabelle" :: name
49967f8b1068 Catching up with smlnj.ML 1.47 (use_file), 1.52 (line numbers), 1.53
gagern
parents: 24611
diff changeset
    32
    | isabellePath (name as (n :: ns)) =
49967f8b1068 Catching up with smlnj.ML 1.47 (use_file), 1.52 (line numbers), 1.53
gagern
parents: 24611
diff changeset
    33
      if n = OS.Path.parentArc then noparent ns else "Isabelle" :: name
49967f8b1068 Catching up with smlnj.ML 1.47 (use_file), 1.52 (line numbers), 1.53
gagern
parents: 24611
diff changeset
    34
49967f8b1068 Catching up with smlnj.ML 1.47 (use_file), 1.52 (line numbers), 1.53
gagern
parents: 24611
diff changeset
    35
  fun rewrite defPrefix name =
49967f8b1068 Catching up with smlnj.ML 1.47 (use_file), 1.52 (line numbers), 1.53
gagern
parents: 24611
diff changeset
    36
      let val abs = mkAbsolute name
49967f8b1068 Catching up with smlnj.ML 1.47 (use_file), 1.52 (line numbers), 1.53
gagern
parents: 24611
diff changeset
    37
	  val rel = OS.Path.mkRelative { path = abs, relativeTo = isabelleHome }
49967f8b1068 Catching up with smlnj.ML 1.47 (use_file), 1.52 (line numbers), 1.53
gagern
parents: 24611
diff changeset
    38
	  val exists = (OS.FileSys.access(abs, nil)
49967f8b1068 Catching up with smlnj.ML 1.47 (use_file), 1.52 (line numbers), 1.53
gagern
parents: 24611
diff changeset
    39
			handle OS.SysErr _ => false)
49967f8b1068 Catching up with smlnj.ML 1.47 (use_file), 1.52 (line numbers), 1.53
gagern
parents: 24611
diff changeset
    40
      in  if exists andalso rel <> ""
49967f8b1068 Catching up with smlnj.ML 1.47 (use_file), 1.52 (line numbers), 1.53
gagern
parents: 24611
diff changeset
    41
	  then isabellePath (toArcs rel)
49967f8b1068 Catching up with smlnj.ML 1.47 (use_file), 1.52 (line numbers), 1.53
gagern
parents: 24611
diff changeset
    42
	  else defPrefix @ noparent (toArcs name)
49967f8b1068 Catching up with smlnj.ML 1.47 (use_file), 1.52 (line numbers), 1.53
gagern
parents: 24611
diff changeset
    43
      end handle OS.Path.Path => defPrefix @ noparent (toArcs name)
22488
415098eece94 Changed AnnoMaLy build process from CVS to tarball sources.
gagern
parents:
diff changeset
    44
415098eece94 Changed AnnoMaLy build process from CVS to tarball sources.
gagern
parents:
diff changeset
    45
in
415098eece94 Changed AnnoMaLy build process from CVS to tarball sources.
gagern
parents:
diff changeset
    46
28284
2161665a0a5d use_text/use_file now depend on explicit ML name space;
wenzelm
parents: 26965
diff changeset
    47
  fun use_text tune str_of_pos name_space (line, name) p v t =
23207
769f7762f531 cosmetic
webertj
parents: 22489
diff changeset
    48
    let val name = case name of "" => "unnamed" | name => name
26505
49967f8b1068 Catching up with smlnj.ML 1.47 (use_file), 1.52 (line numbers), 1.53
gagern
parents: 24611
diff changeset
    49
        val arcs = rewrite ["use_text"] name
49967f8b1068 Catching up with smlnj.ML 1.47 (use_file), 1.52 (line numbers), 1.53
gagern
parents: 24611
diff changeset
    50
        (* should we have different files for different line numbers? *
49967f8b1068 Catching up with smlnj.ML 1.47 (use_file), 1.52 (line numbers), 1.53
gagern
parents: 24611
diff changeset
    51
        val arcs = if line <= 1 then arcs
49967f8b1068 Catching up with smlnj.ML 1.47 (use_file), 1.52 (line numbers), 1.53
gagern
parents: 24611
diff changeset
    52
                   else arcs @ [ "l." ^ Int.toString line ]
49967f8b1068 Catching up with smlnj.ML 1.47 (use_file), 1.52 (line numbers), 1.53
gagern
parents: 24611
diff changeset
    53
	*)
49967f8b1068 Catching up with smlnj.ML 1.47 (use_file), 1.52 (line numbers), 1.53
gagern
parents: 24611
diff changeset
    54
	val arcs = if t = "structure Isabelle =\nstruct\nend;"
49967f8b1068 Catching up with smlnj.ML 1.47 (use_file), 1.52 (line numbers), 1.53
gagern
parents: 24611
diff changeset
    55
		      andalso name = "ML"
49967f8b1068 Catching up with smlnj.ML 1.47 (use_file), 1.52 (line numbers), 1.53
gagern
parents: 24611
diff changeset
    56
		   then ["empty_Isabelle", "empty" ] else arcs
49967f8b1068 Catching up with smlnj.ML 1.47 (use_file), 1.52 (line numbers), 1.53
gagern
parents: 24611
diff changeset
    57
        val _    = AnnoMaLy.nameNextStream arcs
28284
2161665a0a5d use_text/use_file now depend on explicit ML name space;
wenzelm
parents: 26965
diff changeset
    58
    in  smlnj_use_text tune str_of_pos name_space (line, name) p v t  end;
26505
49967f8b1068 Catching up with smlnj.ML 1.47 (use_file), 1.52 (line numbers), 1.53
gagern
parents: 24611
diff changeset
    59
28284
2161665a0a5d use_text/use_file now depend on explicit ML name space;
wenzelm
parents: 26965
diff changeset
    60
  fun use_file tune str_of_pos name_space output verbose name =
26505
49967f8b1068 Catching up with smlnj.ML 1.47 (use_file), 1.52 (line numbers), 1.53
gagern
parents: 24611
diff changeset
    61
      let val arcs = rewrite ["use_file"] name
49967f8b1068 Catching up with smlnj.ML 1.47 (use_file), 1.52 (line numbers), 1.53
gagern
parents: 24611
diff changeset
    62
          val _    = AnnoMaLy.nameNextStream arcs
28284
2161665a0a5d use_text/use_file now depend on explicit ML name space;
wenzelm
parents: 26965
diff changeset
    63
      in  smlnj_use_file tune str_of_pos name_space output verbose name  end;
26505
49967f8b1068 Catching up with smlnj.ML 1.47 (use_file), 1.52 (line numbers), 1.53
gagern
parents: 24611
diff changeset
    64
49967f8b1068 Catching up with smlnj.ML 1.47 (use_file), 1.52 (line numbers), 1.53
gagern
parents: 24611
diff changeset
    65
  fun forget_structure name =
49967f8b1068 Catching up with smlnj.ML 1.47 (use_file), 1.52 (line numbers), 1.53
gagern
parents: 24611
diff changeset
    66
      let val arcs = [ "forget_structure", name ]
49967f8b1068 Catching up with smlnj.ML 1.47 (use_file), 1.52 (line numbers), 1.53
gagern
parents: 24611
diff changeset
    67
          val _    = AnnoMaLy.nameNextStream arcs
49967f8b1068 Catching up with smlnj.ML 1.47 (use_file), 1.52 (line numbers), 1.53
gagern
parents: 24611
diff changeset
    68
      in  smlnj_forget_structure name  end;
22488
415098eece94 Changed AnnoMaLy build process from CVS to tarball sources.
gagern
parents:
diff changeset
    69
415098eece94 Changed AnnoMaLy build process from CVS to tarball sources.
gagern
parents:
diff changeset
    70
end;