1.1 --- a/src/Pure/General/sha1_polyml.ML	Thu Mar 11 15:33:45 2010 +0100
     1.2 +++ b/src/Pure/General/sha1_polyml.ML	Thu Mar 11 16:56:22 2010 +0100
     1.3 @@ -15,15 +15,21 @@
     1.4    let val c = CInterface.fromCchar (CInterface.offset i CInterface.Cchar arr)
     1.5    in (op ^) (pairself hex_digit (Integer.div_mod (Char.ord c) 16)) end
     1.6  
     1.7 +val lib_path =
     1.8 +  ("$ML_HOME/" ^ (if String.isSuffix "cygwin" ml_system then "sha1.dll" else "libsha1.so"))
     1.9 +  |> Path.explode;
    1.10 +
    1.11  fun digest_external str =
    1.12    let
    1.13      val digest = CInterface.alloc 20 CInterface.Cchar;
    1.14 -    val _ = CInterface.call3 (CInterface.get_sym "sha1" "sha1_buffer")
    1.15 -      (CInterface.STRING, CInterface.INT, CInterface.POINTER)
    1.16 -      CInterface.POINTER (str, size str, CInterface.address digest);
    1.17 +    val _ =
    1.18 +      CInterface.call3 (CInterface.get_sym (File.platform_path lib_path) "sha1_buffer")
    1.19 +        (CInterface.STRING, CInterface.INT, CInterface.POINTER)
    1.20 +        CInterface.POINTER (str, size str, CInterface.address digest);
    1.21    in fold (suffix o hex_string digest) (0 upto 19) "" end;
    1.22  
    1.23  fun digest str = digest_external str
    1.24 -  handle CInterface.Foreign _ => SHA1.digest str;
    1.25 +  handle CInterface.Foreign msg =>
    1.26 +    (warning (msg ^ "\nUsing slow ML implementation of SHA1.digest"); SHA1.digest str);
    1.27  
    1.28  end;