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.
fixed file_info;
authorwenzelm
Thu, 04 Feb 1999 18:15:20 +0100
changeset 6227 3198f547f8af
parent 6226 42c94393d39e
child 6228 64f18b89d5d5
fixed file_info;
src/Pure/ML-Systems/mlworks.ML file | annotate | diff | comparison | revisions
src/Pure/ML-Systems/polyml.ML file | annotate | diff | comparison | revisions
src/Pure/ML-Systems/smlnj-0.93.ML file | annotate | diff | comparison | revisions
src/Pure/ML-Systems/smlnj.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/ML-Systems/mlworks.ML	Thu Feb 04 18:15:01 1999 +0100
+++ b/src/Pure/ML-Systems/mlworks.ML	Thu Feb 04 18:15:20 1999 +0100
@@ -124,9 +124,8 @@
 
 (* file handling *)
 
-(*get time of last modification; if file doesn't exist return an empty string*)
-fun file_info "" = ""		(* FIXME !? *)
-  | file_info name = Time.toString (OS.FileSys.modTime name) handle _ => "";
+(*get time of last modification*)
+fun file_info name = Time.toString (OS.FileSys.modTime name) handle _ => "";
 
 
 (* getenv *)
--- a/src/Pure/ML-Systems/polyml.ML	Thu Feb 04 18:15:01 1999 +0100
+++ b/src/Pure/ML-Systems/polyml.ML	Thu Feb 04 18:15:20 1999 +0100
@@ -109,9 +109,8 @@
 
 (* file handling *)
 
-(*get time of last modification; if file doesn't exist return an empty string*)
-fun file_info "" = ""           (* FIXME !? *)
-  | file_info name = Int.toString (System.filedate name) handle _ => "";
+(*get time of last modification*)
+fun file_info name = Int.toString (System.filedate name) handle _ => "";
 
 structure OS =
 struct
--- a/src/Pure/ML-Systems/smlnj-0.93.ML	Thu Feb 04 18:15:01 1999 +0100
+++ b/src/Pure/ML-Systems/smlnj-0.93.ML	Thu Feb 04 18:15:20 1999 +0100
@@ -174,12 +174,11 @@
 
 (* file handling *)
 
-(*Get time of last modification; if file doesn't exist return an empty string*)
+(*get time of last modification*)
 local
   open System.Timer System.Unsafe.SysIO;
 in
-  fun file_info "" = ""
-    | file_info name = makestring (mtime (PATH name)) handle _ => "";
+  fun file_info name = makestring (mtime (PATH name)) handle _ => "";
 end;
 
 structure OS =
--- a/src/Pure/ML-Systems/smlnj.ML	Thu Feb 04 18:15:01 1999 +0100
+++ b/src/Pure/ML-Systems/smlnj.ML	Thu Feb 04 18:15:20 1999 +0100
@@ -192,9 +192,8 @@
 
 (* file handling *)
 
-(*get time of last modification; if file doesn't exist return an empty string*)
-fun file_info "" = ""           (* FIXME !? *)
-  | file_info name = Time.toString (OS.FileSys.modTime name) handle _ => "";
+(*get time of last modification*)
+fun file_info name = Time.toString (OS.FileSys.modTime name) handle _ => "";
 
 
 (* getenv *)
isabelle