added SHA1 library integrity test, which is invoked at compile time and Isabelle_Process run-time;

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/sha1_samples.ML	Mon Aug 26 21:56:08 2013 +0200
@@ -0,0 +1,35 @@
+(*  Title:      Pure/General/sha1_samples.ML
+    Author:     Makarius
+
+Some SHA1 samples found in the wild.
+*)
+
+signature SHA1_SAMPLES =
+sig
+  val test: unit -> unit
+end;
+
+structure SHA1_Samples: SHA1_SAMPLES =
+struct
+
+fun check (msg, key) =
+  let val key' = SHA1.rep (SHA1.digest msg) in
+    if key = key' then ()
+    else
+      raise Fail ("SHA1 library integrity test failed on " ^ quote msg ^ ":\n" ^
+        key ^ " expected, but\n" ^ key' ^ " was found")
+  end;
+
+fun test () =
+  List.app check
+   [("", "da39a3ee5e6b4b0d3255bfef95601890afd80709"),
+    ("a", "86f7e437faa5a7fce15d1ddcb9eaeaea377667b8"),
+    ("abc", "a9993e364706816aba3e25717850c26c9cd0d89d"),
+    ("abcdefghijklmnopqrstuvwxyz", "32d10c7b8cf96570ca04ce37f2a19d84240d3a89"),
+    ("The quick brown fox jumps over the lazy dog", "2fd4e1c67a2d28fced849ee1bb76e7391b93eb12"),
+    (replicate_string 100 "\000", "ed4a77d1b56a118938788fc53037759b6c501e3d"),
+    ("a\000b", "4a3dec2d1f8245280855c42db0ee4239f917fdb8")];
+
+val _ = test ();
+
+end;

--- a/src/Pure/ROOT	Mon Aug 26 21:53:56 2013 +0200
+++ b/src/Pure/ROOT	Mon Aug 26 21:56:08 2013 +0200
@@ -91,6 +91,7 @@
     "General/seq.ML"
     "General/sha1.ML"
     "General/sha1_polyml.ML"
+    "General/sha1_samples.ML"
     "General/socket_io.ML"
     "General/source.ML"
     "General/stack.ML"

--- a/src/Pure/ROOT.ML	Mon Aug 26 21:53:56 2013 +0200
+++ b/src/Pure/ROOT.ML	Mon Aug 26 21:56:08 2013 +0200
@@ -59,6 +59,7 @@
 
 use "General/sha1.ML";
 if ML_System.is_polyml then use "General/sha1_polyml.ML" else ();
+use "General/sha1_samples.ML";
 
 use "PIDE/xml.ML";
 use "PIDE/yxml.ML";

--- a/src/Pure/System/isabelle_process.ML	Mon Aug 26 21:53:56 2013 +0200
+++ b/src/Pure/System/isabelle_process.ML	Mon Aug 26 21:56:08 2013 +0200
@@ -187,6 +187,8 @@
 
 val init = uninterruptible (fn _ => fn rendezvous =>
   let
+    val _ = SHA1_Samples.test ()
+      handle exn as Fail msg => (Output.physical_stderr (msg ^ "\n"); reraise exn);
     val _ = Output.physical_stderr Symbol.STX;
 
     val _ = Printer.show_markup_default := true;

--- a/src/Pure/Tools/build.ML	Mon Aug 26 21:53:56 2013 +0200
+++ b/src/Pure/Tools/build.ML	Mon Aug 26 21:56:08 2013 +0200
@@ -127,6 +127,8 @@
 
 fun build args_file = Command_Line.tool (fn () =>
     let
+      val _ = SHA1_Samples.test ();
+
       val (command_timings, (do_output, (options, (verbose, (browser_info,
           (parent_name, (chapter, (name, theories)))))))) =
         File.read (Path.explode args_file) |> YXML.parse_body |>