# HG changeset patch
# User wenzelm
# Date 1604237409 -3600
# Node ID e0c6522d5d437b4c021c20d17934cca2e8f8ed37
# Parent  63ec86626ec3add8bf7b7288e187f9722e8c9b73
prefer static library_call, following recent changes to structure Foreign;

diff -r 63ec86626ec3 -r e0c6522d5d43 src/Pure/General/sha1.ML
--- a/src/Pure/General/sha1.ML	Sun Nov 01 14:04:52 2020 +0100
+++ b/src/Pure/General/sha1.ML	Sun Nov 01 14:30:09 2020 +0100
@@ -148,6 +148,11 @@
 val library_path =
   Path.explode ("$ML_HOME/" ^ (if ML_System.platform_is_windows then "sha1.dll" else "libsha1.so"));
 
+val library_call =
+  Foreign.buildCall3
+    (Foreign.getSymbol (Foreign.loadLibrary (File.platform_path library_path)) "sha1_buffer",
+      (Foreign.cByteArray, Foreign.cUlong, Foreign.cPointer), Foreign.cPointer);
+
 fun with_memory n =
   Thread_Attributes.uninterruptible (fn restore_attributes => fn f =>
     let
@@ -166,12 +171,8 @@
 fun digest_string_external str =
   with_memory 20 (fn mem =>
     let
-      val library = Foreign.loadLibrary (File.platform_path library_path);
       val bytes = Byte.stringToBytes str;
-      val _ =
-        Foreign.buildCall3 (Foreign.getSymbol library "sha1_buffer",
-          (Foreign.cByteArray, Foreign.cUlong, Foreign.cPointer), Foreign.cPointer)
-          (bytes, Word8Vector.length bytes, mem);
+      val _ = library_call (bytes, Word8Vector.length bytes, mem);
       fun get i = hex_string (Foreign.Memory.get8 (mem, Word.fromInt i));
     in implode (map get (0 upto 19)) end);