# HG changeset patch
# User wenzelm
# Date 1377546836 -7200
# Node ID 753b9fbe18be991ecb8fa1c0bbfced9978a0dd6a
# Parent  7219c61796c04048e6529a59405aa64441533d30
allow NUL characters in ML string passed to C library;

diff -r 7219c61796c0 -r 753b9fbe18be src/Pure/General/sha1_polyml.ML
--- a/src/Pure/General/sha1_polyml.ML	Mon Aug 26 18:08:54 2013 +0200
+++ b/src/Pure/General/sha1_polyml.ML	Mon Aug 26 21:53:56 2013 +0200
@@ -21,12 +21,16 @@
   ("$ML_HOME/" ^ (if ML_System.platform_is_cygwin then "sha1.dll" else "libsha1.so"))
   |> Path.explode;
 
+val STRING_INPUT_BYTES =
+  CInterface.mkConversion undefined (CInterface.toCbytes o Byte.stringToBytes)
+    (CInterface.Cpointer CInterface.Cchar);
+
 fun digest_external str =
   let
     val digest = CInterface.alloc 20 CInterface.Cchar;
     val _ =
       CInterface.call3 (CInterface.get_sym (File.platform_path lib_path) "sha1_buffer")
-        (CInterface.STRING, CInterface.LONG, CInterface.POINTER)
+        (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;