clarified errors;
authorwenzelm
Sat, 26 Sep 2020 11:43:25 +0200
changeset 72308 aa14f630d8ef
parent 72307 b82347da780b
child 72309 564012e31db1
clarified errors;
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