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