# HG changeset patch
# User Andreas Lochbihler
# Date 1375971005 -7200
# Node ID 7bfe0df532a9d11f26d2353583b355b721b74af3
# Parent  66cc4ed9a1f2d7259fd405930f0722fba42bd12f
abort execution of generated code with explicit exception message

diff -r 66cc4ed9a1f2 -r 7bfe0df532a9 src/HOL/String.thy
--- a/src/HOL/String.thy	Thu Aug 08 14:55:01 2013 +0200
+++ b/src/HOL/String.thy	Thu Aug 08 16:10:05 2013 +0200
@@ -420,6 +420,19 @@
     and (Haskell) infix 4 "=="
     and (Scala) infixl 5 "=="
 
+setup {* Sign.map_naming (Name_Space.mandatory_path "Code") *}
+
+definition abort :: "literal \<Rightarrow> (unit \<Rightarrow> 'a) \<Rightarrow> 'a"
+where [simp, code del]: "abort _ f = f ()"
+
+setup {* Sign.map_naming Name_Space.parent_path *}
+
+code_printing constant Code.abort \<rightharpoonup>
+    (SML) "!(raise/ Fail/ _)"
+    and (OCaml) "failwith"
+    and (Haskell) "error"
+    and (Scala) "!{/ sys.error((_));/  ((_)).apply(())/ }"
+
 hide_type (open) literal
 
 end