Admin/isatest/annomaly.ML
author haftmann
Thu, 18 Nov 2010 17:01:15 +0100
changeset 40602 91e583511113
parent 32449 696d64ed85da
permissions -rw-r--r--
map_fun combinator in theory Fun
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
    Author:     Martin von Gagern <martin@von-gagern.net>
769f7762f531 cosmetic
webertj
parents: 22489
diff changeset
     3
*)
769f7762f531 cosmetic
webertj
parents: 22489
diff changeset
     4
769f7762f531 cosmetic
webertj
parents: 22489
diff changeset
     5
use "ML-Systems/smlnj.ML";
22488
415098eece94 Changed AnnoMaLy build process from CVS to tarball sources.
gagern
parents:
diff changeset
     6
415098eece94 Changed AnnoMaLy build process from CVS to tarball sources.
gagern
parents:
diff changeset
     7
local
415098eece94 Changed AnnoMaLy build process from CVS to tarball sources.
gagern
parents:
diff changeset
     8
415098eece94 Changed AnnoMaLy build process from CVS to tarball sources.
gagern
parents:
diff changeset
     9
  val smlnj_use_text = use_text
415098eece94 Changed AnnoMaLy build process from CVS to tarball sources.
gagern
parents:
diff changeset
    10
26505
49967f8b1068 Catching up with smlnj.ML 1.47 (use_file), 1.52 (line numbers), 1.53
gagern
parents: 24611
diff changeset
    11
  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
    12
49967f8b1068 Catching up with smlnj.ML 1.47 (use_file), 1.52 (line numbers), 1.53
gagern
parents: 24611
diff changeset
    13
  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
    14
49967f8b1068 Catching up with smlnj.ML 1.47 (use_file), 1.52 (line numbers), 1.53
gagern
parents: 24611
diff changeset
    15
  fun mkAbsolute path =
49967f8b1068 Catching up with smlnj.ML 1.47 (use_file), 1.52 (line numbers), 1.53
gagern
parents: 24611
diff changeset
    16
      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
    17
49967f8b1068 Catching up with smlnj.ML 1.47 (use_file), 1.52 (line numbers), 1.53
gagern
parents: 24611
diff changeset
    18
  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
    19
49967f8b1068 Catching up with smlnj.ML 1.47 (use_file), 1.52 (line numbers), 1.53
gagern
parents: 24611
diff changeset
    20
  val isabelleHome =
49967f8b1068 Catching up with smlnj.ML 1.47 (use_file), 1.52 (line numbers), 1.53
gagern
parents: 24611
diff changeset
    21
      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
    22
       of  NONE => OS.FileSys.getDir ()
32449
696d64ed85da eliminated hard tabs;
wenzelm
parents: 31582
diff changeset
    23
         | SOME home => mkAbsolute home
22488
415098eece94 Changed AnnoMaLy build process from CVS to tarball sources.
gagern
parents:
diff changeset
    24
26505
49967f8b1068 Catching up with smlnj.ML 1.47 (use_file), 1.52 (line numbers), 1.53
gagern
parents: 24611
diff changeset
    25
  fun noparent [] = []
49967f8b1068 Catching up with smlnj.ML 1.47 (use_file), 1.52 (line numbers), 1.53
gagern
parents: 24611
diff changeset
    26
    | noparent (n :: ns) =
49967f8b1068 Catching up with smlnj.ML 1.47 (use_file), 1.52 (line numbers), 1.53
gagern
parents: 24611
diff changeset
    27
      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
    28
49967f8b1068 Catching up with smlnj.ML 1.47 (use_file), 1.52 (line numbers), 1.53
gagern
parents: 24611
diff changeset
    29
  fun isabellePath [] = []
49967f8b1068 Catching up with smlnj.ML 1.47 (use_file), 1.52 (line numbers), 1.53
gagern
parents: 24611
diff changeset
    30
    | 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
    31
    | 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
    32
      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
    33
49967f8b1068 Catching up with smlnj.ML 1.47 (use_file), 1.52 (line numbers), 1.53
gagern
parents: 24611
diff changeset
    34
  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
    35
      let val abs = mkAbsolute name
32449
696d64ed85da eliminated hard tabs;
wenzelm
parents: 31582
diff changeset
    36
          val rel = OS.Path.mkRelative { path = abs, relativeTo = isabelleHome }
696d64ed85da eliminated hard tabs;
wenzelm
parents: 31582
diff changeset
    37
          val exists = (OS.FileSys.access(abs, nil)
696d64ed85da eliminated hard tabs;
wenzelm
parents: 31582
diff changeset
    38
                        handle OS.SysErr _ => false)
26505
49967f8b1068 Catching up with smlnj.ML 1.47 (use_file), 1.52 (line numbers), 1.53
gagern
parents: 24611
diff changeset
    39
      in  if exists andalso rel <> ""
32449
696d64ed85da eliminated hard tabs;
wenzelm
parents: 31582
diff changeset
    40
          then isabellePath (toArcs rel)
696d64ed85da eliminated hard tabs;
wenzelm
parents: 31582
diff changeset
    41
          else defPrefix @ noparent (toArcs name)
26505
49967f8b1068 Catching up with smlnj.ML 1.47 (use_file), 1.52 (line numbers), 1.53
gagern
parents: 24611
diff changeset
    42
      end handle OS.Path.Path => defPrefix @ noparent (toArcs name)
22488
415098eece94 Changed AnnoMaLy build process from CVS to tarball sources.
gagern
parents:
diff changeset
    43
415098eece94 Changed AnnoMaLy build process from CVS to tarball sources.
gagern
parents:
diff changeset
    44
in
415098eece94 Changed AnnoMaLy build process from CVS to tarball sources.
gagern
parents:
diff changeset
    45
28284
2161665a0a5d use_text/use_file now depend on explicit ML name space;
wenzelm
parents: 26965
diff changeset
    46
  fun use_text tune str_of_pos name_space (line, name) p v t =
23207
769f7762f531 cosmetic
webertj
parents: 22489
diff changeset
    47
    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
    48
        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
    49
        (* 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
    50
        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
    51
                   else arcs @ [ "l." ^ Int.toString line ]
32449
696d64ed85da eliminated hard tabs;
wenzelm
parents: 31582
diff changeset
    52
        *)
696d64ed85da eliminated hard tabs;
wenzelm
parents: 31582
diff changeset
    53
        val arcs = if t = "structure Isabelle =\nstruct\nend;"
696d64ed85da eliminated hard tabs;
wenzelm
parents: 31582
diff changeset
    54
                      andalso name = "ML"
696d64ed85da eliminated hard tabs;
wenzelm
parents: 31582
diff changeset
    55
                   then ["empty_Isabelle", "empty" ] else arcs
26505
49967f8b1068 Catching up with smlnj.ML 1.47 (use_file), 1.52 (line numbers), 1.53
gagern
parents: 24611
diff changeset
    56
        val _    = AnnoMaLy.nameNextStream arcs
28284
2161665a0a5d use_text/use_file now depend on explicit ML name space;
wenzelm
parents: 26965
diff changeset
    57
    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
    58
28284
2161665a0a5d use_text/use_file now depend on explicit ML name space;
wenzelm
parents: 26965
diff changeset
    59
  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
    60
      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
    61
          val _    = AnnoMaLy.nameNextStream arcs
28284
2161665a0a5d use_text/use_file now depend on explicit ML name space;
wenzelm
parents: 26965
diff changeset
    62
      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
    63
49967f8b1068 Catching up with smlnj.ML 1.47 (use_file), 1.52 (line numbers), 1.53
gagern
parents: 24611
diff changeset
    64
  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
    65
      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
    66
          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
    67
      in  smlnj_forget_structure name  end;
22488
415098eece94 Changed AnnoMaLy build process from CVS to tarball sources.
gagern
parents:
diff changeset
    68
415098eece94 Changed AnnoMaLy build process from CVS to tarball sources.
gagern
parents:
diff changeset
    69
end;