651 | _ => NONE) |
651 | _ => NONE) |
652 | _ => NONE) |
652 | _ => NONE) |
653 |
653 |
654 fun load_state ctxt (time_state as (memory_time, _)) = |
654 fun load_state ctxt (time_state as (memory_time, _)) = |
655 let val path = state_file () in |
655 let val path = state_file () in |
656 (case try OS.FileSys.modTime (Path.implode path) of |
656 (case try OS.FileSys.modTime (File.platform_path path) of |
657 NONE => time_state |
657 NONE => time_state |
658 | SOME disk_time => |
658 | SOME disk_time => |
659 if Time.>= (memory_time, disk_time) then |
659 if Time.>= (memory_time, disk_time) then |
660 time_state |
660 time_state |
661 else |
661 else |
697 fun append_entry (name, ((kind, feats, deps), (parents, _))) = |
697 fun append_entry (name, ((kind, feats, deps), (parents, _))) = |
698 cons (kind, name, Graph.Keys.dest parents, feats, deps) |
698 cons (kind, name, Graph.Keys.dest parents, feats, deps) |
699 |
699 |
700 val path = state_file () |
700 val path = state_file () |
701 val dirty_facts' = |
701 val dirty_facts' = |
702 (case try OS.FileSys.modTime (Path.implode path) of |
702 (case try OS.FileSys.modTime (File.platform_path path) of |
703 NONE => NONE |
703 NONE => NONE |
704 | SOME disk_time => if Time.<= (disk_time, memory_time) then dirty_facts else NONE) |
704 | SOME disk_time => if Time.<= (disk_time, memory_time) then dirty_facts else NONE) |
705 val (banner, entries) = |
705 val (banner, entries) = |
706 (case dirty_facts' of |
706 (case dirty_facts' of |
707 SOME names => (NONE, fold (append_entry o Graph.get_entry access_G) names []) |
707 SOME names => (NONE, fold (append_entry o Graph.get_entry access_G) names []) |