18 fun toArcs path = #arcs (OS.Path.fromString path) |
18 fun toArcs path = #arcs (OS.Path.fromString path) |
19 |
19 |
20 val isabelleHome = |
20 val isabelleHome = |
21 case OS.Process.getEnv "ISABELLE_HOME" |
21 case OS.Process.getEnv "ISABELLE_HOME" |
22 of NONE => OS.FileSys.getDir () |
22 of NONE => OS.FileSys.getDir () |
23 | SOME home => mkAbsolute home |
23 | SOME home => mkAbsolute home |
24 |
24 |
25 fun noparent [] = [] |
25 fun noparent [] = [] |
26 | noparent (n :: ns) = |
26 | noparent (n :: ns) = |
27 if n = OS.Path.parentArc then noparent ns else n :: noparent ns |
27 if n = OS.Path.parentArc then noparent ns else n :: noparent ns |
28 |
28 |
31 | isabellePath (name as (n :: ns)) = |
31 | isabellePath (name as (n :: ns)) = |
32 if n = OS.Path.parentArc then noparent ns else "Isabelle" :: name |
32 if n = OS.Path.parentArc then noparent ns else "Isabelle" :: name |
33 |
33 |
34 fun rewrite defPrefix name = |
34 fun rewrite defPrefix name = |
35 let val abs = mkAbsolute name |
35 let val abs = mkAbsolute name |
36 val rel = OS.Path.mkRelative { path = abs, relativeTo = isabelleHome } |
36 val rel = OS.Path.mkRelative { path = abs, relativeTo = isabelleHome } |
37 val exists = (OS.FileSys.access(abs, nil) |
37 val exists = (OS.FileSys.access(abs, nil) |
38 handle OS.SysErr _ => false) |
38 handle OS.SysErr _ => false) |
39 in if exists andalso rel <> "" |
39 in if exists andalso rel <> "" |
40 then isabellePath (toArcs rel) |
40 then isabellePath (toArcs rel) |
41 else defPrefix @ noparent (toArcs name) |
41 else defPrefix @ noparent (toArcs name) |
42 end handle OS.Path.Path => defPrefix @ noparent (toArcs name) |
42 end handle OS.Path.Path => defPrefix @ noparent (toArcs name) |
43 |
43 |
44 in |
44 in |
45 |
45 |
46 fun use_text tune str_of_pos name_space (line, name) p v t = |
46 fun use_text tune str_of_pos name_space (line, name) p v t = |
47 let val name = case name of "" => "unnamed" | name => name |
47 let val name = case name of "" => "unnamed" | name => name |
48 val arcs = rewrite ["use_text"] name |
48 val arcs = rewrite ["use_text"] name |
49 (* should we have different files for different line numbers? * |
49 (* should we have different files for different line numbers? * |
50 val arcs = if line <= 1 then arcs |
50 val arcs = if line <= 1 then arcs |
51 else arcs @ [ "l." ^ Int.toString line ] |
51 else arcs @ [ "l." ^ Int.toString line ] |
52 *) |
52 *) |
53 val arcs = if t = "structure Isabelle =\nstruct\nend;" |
53 val arcs = if t = "structure Isabelle =\nstruct\nend;" |
54 andalso name = "ML" |
54 andalso name = "ML" |
55 then ["empty_Isabelle", "empty" ] else arcs |
55 then ["empty_Isabelle", "empty" ] else arcs |
56 val _ = AnnoMaLy.nameNextStream arcs |
56 val _ = AnnoMaLy.nameNextStream arcs |
57 in smlnj_use_text tune str_of_pos name_space (line, name) p v t end; |
57 in smlnj_use_text tune str_of_pos name_space (line, name) p v t end; |
58 |
58 |
59 fun use_file tune str_of_pos name_space output verbose name = |
59 fun use_file tune str_of_pos name_space output verbose name = |
60 let val arcs = rewrite ["use_file"] name |
60 let val arcs = rewrite ["use_file"] name |