# HG changeset patch
# User wenzelm
# Date 1601113405 -7200
# Node ID aa14f630d8ef841fe3135c38d3d7d214f5268c50
# Parent  b82347da780b5b25f3f7766083c3f6082562845f
clarified errors;

diff -r b82347da780b -r aa14f630d8ef src/HOL/Library/code_test.ML
--- a/src/HOL/Library/code_test.ML	Sat Sep 26 11:30:26 2020 +0200
+++ b/src/HOL/Library/code_test.ML	Sat Sep 26 11:43:25 2020 +0200
@@ -322,6 +322,7 @@
         (ML_Lex.read_text (code, Path.position code_path) @
          ML_Lex.read_text (driver, Path.position driver_path) @
          ML_Lex.read "main ()")
+      handle ERROR msg => error ("Evaluation for " ^ polymlN ^ " failed:\n" ^ msg)
   in File.read out_path end
 
 
@@ -509,6 +510,7 @@
     val _ = File.write code_path code
     val _ = File.write driver_path driver
     val _ = Scala_Compiler.toplevel true (code ^ driver)
+      handle ERROR msg => error ("Evaluation for " ^ scalaN ^ " failed:\n" ^ msg)
   in File.read out_path end