--- a/src/HOL/HOL.thy Tue Jun 05 07:05:56 2012 +0200
+++ b/src/HOL/HOL.thy Tue Jun 05 07:10:51 2012 +0200
@@ -1903,7 +1903,7 @@
(SML "!(raise/ Fail/ \"undefined\")")
(OCaml "failwith/ \"undefined\"")
(Haskell "error/ \"undefined\"")
- (Scala "!error(\"undefined\")")
+ (Scala "!sys.error(\"undefined\")")
subsubsection {* Evaluation and normalization by evaluation *}
--- a/src/HOL/Imperative_HOL/Array.thy Tue Jun 05 07:05:56 2012 +0200
+++ b/src/HOL/Imperative_HOL/Array.thy Tue Jun 05 07:10:51 2012 +0200
@@ -491,7 +491,7 @@
text {* Scala *}
code_type array (Scala "!collection.mutable.ArraySeq[_]")
-code_const Array (Scala "!error(\"bare Array\")")
+code_const Array (Scala "!sys.error(\"bare Array\")")
code_const Array.new' (Scala "('_: Unit)/ => / Array.alloc((_))((_))")
code_const Array.make' (Scala "('_: Unit)/ =>/ Array.make((_))((_))")
code_const Array.len' (Scala "('_: Unit)/ =>/ Array.len((_))")
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy Tue Jun 05 07:05:56 2012 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Tue Jun 05 07:10:51 2012 +0200
@@ -610,7 +610,7 @@
code_type Heap (Scala "Unit/ =>/ _")
code_const bind (Scala "Heap.bind")
code_const return (Scala "('_: Unit)/ =>/ _")
-code_const Heap_Monad.raise' (Scala "!error((_))")
+code_const Heap_Monad.raise' (Scala "!sys.error((_))")
subsubsection {* Target variants with less units *}
--- a/src/HOL/Imperative_HOL/Ref.thy Tue Jun 05 07:05:56 2012 +0200
+++ b/src/HOL/Imperative_HOL/Ref.thy Tue Jun 05 07:10:51 2012 +0200
@@ -313,7 +313,7 @@
text {* Scala *}
code_type ref (Scala "!Ref[_]")
-code_const Ref (Scala "!error(\"bare Ref\")")
+code_const Ref (Scala "!sys.error(\"bare Ref\")")
code_const ref' (Scala "('_: Unit)/ =>/ Ref((_))")
code_const Ref.lookup (Scala "('_: Unit)/ =>/ Ref.lookup((_))")
code_const Ref.update (Scala "('_: Unit)/ =>/ Ref.update((_), (_))")
--- a/src/HOL/Library/Code_Integer.thy Tue Jun 05 07:05:56 2012 +0200
+++ b/src/HOL/Library/Code_Integer.thy Tue Jun 05 07:10:51 2012 +0200
@@ -111,7 +111,7 @@
(SML "!(raise/ Fail/ \"sub\")")
(OCaml "failwith/ \"sub\"")
(Haskell "error/ \"sub\"")
- (Scala "!error(\"sub\")")
+ (Scala "!sys.error(\"sub\")")
code_const "op * \<Colon> int \<Rightarrow> int \<Rightarrow> int"
(SML "IntInf.* ((_), (_))")
--- a/src/HOL/Library/Efficient_Nat.thy Tue Jun 05 07:05:56 2012 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy Tue Jun 05 07:10:51 2012 +0200
@@ -228,7 +228,7 @@
(SML "!(raise/ Fail/ \"sub\")")
(OCaml "failwith/ \"sub\"")
(Haskell "error/ \"sub\"")
- (Scala "!error(\"sub\")")
+ (Scala "!sys.error(\"sub\")")
code_const "times \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"
(SML "IntInf.*/ ((_),/ (_))")
@@ -269,7 +269,7 @@
(SML "!(raise/ Fail/ \"num'_of'_nat\")")
(OCaml "failwith/ \"num'_of'_nat\"")
(Haskell "error/ \"num'_of'_nat\"")
- (Scala "!error(\"num'_of'_nat\")")
+ (Scala "!sys.error(\"num'_of'_nat\")")
subsection {* Evaluation *}
--- a/src/HOL/Library/Target_Numeral.thy Tue Jun 05 07:05:56 2012 +0200
+++ b/src/HOL/Library/Target_Numeral.thy Tue Jun 05 07:10:51 2012 +0200
@@ -465,7 +465,7 @@
(SML "!(raise/ Fail/ \"sub\")")
(OCaml "failwith/ \"sub\"")
(Haskell "error/ \"sub\"")
- (Scala "!error(\"sub\")")
+ (Scala "!sys.error(\"sub\")")
code_const "times :: Target_Numeral.int \<Rightarrow> _ \<Rightarrow> _"
(SML "IntInf.* ((_), (_))")
--- a/src/Tools/Code/code_scala.ML Tue Jun 05 07:05:56 2012 +0200
+++ b/src/Tools/Code/code_scala.ML Tue Jun 05 07:10:51 2012 +0200
@@ -101,7 +101,7 @@
and print_bind tyvars some_thm fxy p =
gen_print_bind (print_term tyvars true) some_thm fxy p
and print_case tyvars some_thm vars fxy { clauses = [], ... } =
- (brackify fxy o Pretty.breaks o map str) ["error(\"empty case\")"]
+ (brackify fxy o Pretty.breaks o map str) ["sys.error(\"empty case\")"]
| print_case tyvars some_thm vars fxy (case_expr as { clauses = [_], ... }) =
let
val (bind :: binds, body) = Code_Thingol.unfold_let (ICase case_expr);
@@ -155,7 +155,7 @@
val vars = intro_vars params reserved;
in
concat [print_defhead tyvars vars name vs params tys ty',
- str ("error(\"" ^ name ^ "\")")]
+ str ("sys.error(\"" ^ name ^ "\")")]
end
| print_def name (vs, ty) eqs =
let
@@ -439,7 +439,7 @@
"true", "type", "val", "var", "while", "with", "yield"
]
#> fold (Code_Target.add_reserved target) [
- "apply", "error", "scala", "BigInt", "Nil", "List"
+ "apply", "sys", "scala", "BigInt", "Nil", "List"
];
end; (*struct*)