author  blanchet 
Wed, 08 Dec 2010 22:18:37 +0100  
changeset 41093  dfbc8759415f 
parent 32449  696d64ed85da 
permissions  rwrr 
23207  1 
(* Title: Admin/isatest/annomaly.ML 
2 
Author: Martin von Gagern <martin@vongagern.net> 

3 
*) 

4 

5 
use "MLSystems/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  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  36 
val rel = OS.Path.mkRelative { path = abs, relativeTo = isabelleHome } 
37 
val exists = (OS.FileSys.access(abs, nil) 

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  40 
then isabellePath (toArcs rel) 
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  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  52 
*) 
53 
val arcs = if t = "structure Isabelle =\nstruct\nend;" 

54 
andalso name = "ML" 

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; 