--- a/src/Pure/General/sha1_polyml.ML Tue Aug 18 11:14:39 2015 +0200
+++ b/src/Pure/General/sha1_polyml.ML Tue Aug 18 11:43:24 2015 +0200
@@ -18,7 +18,9 @@
in (op ^) (apply2 hex_digit (Integer.div_mod (Char.ord c) 16)) end
val lib_path =
- ("$ML_HOME/" ^ (if ML_System.platform_is_cygwin then "sha1.dll" else "libsha1.so"))
+ ("$ML_HOME/" ^
+ (if ML_System.platform_is_cygwin orelse ML_System.platform_is_windows
+ then "sha1.dll" else "libsha1.so"))
|> Path.explode;
val STRING_INPUT_BYTES =
@@ -29,7 +31,8 @@
let
val digest = CInterface.alloc 20 CInterface.Cchar;
val _ =
- CInterface.call3 (CInterface.get_sym (File.platform_path lib_path) "sha1_buffer")
+ CInterface.call3
+ (CInterface.get_sym (ml_platform_path (File.platform_path lib_path)) "sha1_buffer")
(STRING_INPUT_BYTES, CInterface.LONG, CInterface.POINTER)
CInterface.POINTER (str, size str, CInterface.address digest);
in fold (suffix o hex_string digest) (0 upto 19) "" end;
--- a/src/Pure/ML-Systems/polyml.ML Tue Aug 18 11:14:39 2015 +0200
+++ b/src/Pure/ML-Systems/polyml.ML Tue Aug 18 11:43:24 2015 +0200
@@ -31,6 +31,7 @@
then use "ML-Systems/share_common_data_polyml-5.3.0.ML"
else ();
+fun ml_platform_path (s: string) = s;
if ML_System.platform_is_windows then use "ML-Systems/windows_polyml.ML" else ();
structure ML_System =
--- a/src/Pure/ML-Systems/smlnj.ML Tue Aug 18 11:14:39 2015 +0200
+++ b/src/Pure/ML-Systems/smlnj.ML Tue Aug 18 11:43:24 2015 +0200
@@ -168,6 +168,8 @@
(* ML system operations *)
+fun ml_platform_path (s: string) = s;
+
use "ML-Systems/ml_system.ML";
structure ML_System =
--- a/src/Pure/ML-Systems/windows_polyml.ML Tue Aug 18 11:14:39 2015 +0200
+++ b/src/Pure/ML-Systems/windows_polyml.ML Tue Aug 18 11:43:24 2015 +0200
@@ -75,13 +75,6 @@
val openAppend = openAppend o OS.windows;
end;
-structure CInterfaces =
-struct
- open CInterface;
- val get_sym_windows = get_sym;
- val get_sym = get_sym_windows o OS.windows;
-end;
-
structure PolyML =
struct
open PolyML
@@ -91,4 +84,6 @@
val loadState = loadState o OS.windows;
val saveState = saveState o OS.windows;
end;
-end;
\ No newline at end of file
+end;
+
+val ml_platform_path = OS.windows;