Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
proper platform_path;
authorwenzelm
Tue, 18 Aug 2015 16:49:32 +0200
changeset 60971 6dfe08f5834e
parent 60970 e08d868ceca9
child 60972 4fc468197040
proper platform_path;
src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Tue Aug 18 16:08:47 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Tue Aug 18 16:49:32 2015 +0200
@@ -653,7 +653,7 @@
 
 fun load_state ctxt (time_state as (memory_time, _)) =
   let val path = state_file () in
-    (case try OS.FileSys.modTime (Path.implode path) of
+    (case try OS.FileSys.modTime (File.platform_path path) of
       NONE => time_state
     | SOME disk_time =>
       if Time.>= (memory_time, disk_time) then
@@ -699,7 +699,7 @@
 
       val path = state_file ()
       val dirty_facts' =
-        (case try OS.FileSys.modTime (Path.implode path) of
+        (case try OS.FileSys.modTime (File.platform_path path) of
           NONE => NONE
         | SOME disk_time => if Time.<= (disk_time, memory_time) then dirty_facts else NONE)
       val (banner, entries) =
isabelle