# HG changeset patch
# User wenzelm
# Date 1439891004 -7200
# Node ID fdb82e722f8ac8dea33106277fb47723b8010a36
# Parent  3c6751e2f10adf1479b99334729947cb6d91686d
keep native CInterface to make SHA1 work properly;

diff -r 3c6751e2f10a -r fdb82e722f8a src/Pure/General/sha1_polyml.ML
--- 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;
diff -r 3c6751e2f10a -r fdb82e722f8a src/Pure/ML-Systems/polyml.ML
--- 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 =
diff -r 3c6751e2f10a -r fdb82e722f8a src/Pure/ML-Systems/smlnj.ML
--- 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 =
diff -r 3c6751e2f10a -r fdb82e722f8a src/Pure/ML-Systems/windows_polyml.ML
--- 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;