1structure GraphExtra :> GraphExtra =
2struct
3
4open Holmake_tools
5open hm_target
6type t = {holheap : dep option}
7
8fun extra_deps {holheap = SOME d} = [d]
9  | extra_deps {holheap = NONE} = []
10
11fun get_extra0 {master_dir,master_cline : HM_Cline.t, envlist} =
12    case envlist "HOLHEAP" of
13        [] =>
14        if #poly_not_hol master_cline then NONE
15        else (
16          case #holstate master_cline of
17              NONE => SOME (filestr_to_tgt
18                              (fullPath[Systeml.HOLDIR, "bin",
19                                        "hol.state"]))
20            | SOME s =>
21              let
22                val fp = hmdir.extendp {base = master_dir, extension = s}
23                val {dir,file} = OS.Path.splitDirFile (hmdir.toAbsPath fp)
24              in
25                SOME (mk(hmdir.fromPath{origin="", path = dir}, toFile file))
26              end
27        )
28      | [s] => SOME (filestr_to_tgt s)
29      | _ => die_with ("Can't interpret HOLHEAP spec. in " ^
30                       OS.FileSys.getDir())
31
32fun get_extra i = {holheap = get_extra0 i}
33
34fun toString {holheap = SOME d} = "heap="^tgt_toString d
35  | toString {holheap = NONE} = "heap=*"
36
37fun canIgnore d {holheap=SOME d'} = hm_target.compare(d,d') = EQUAL
38  | canIgnore d _ = false
39
40end
41