# HG changeset patch
# User haftmann
# Date 1338873051 -7200
# Node ID 1b609a7837ef0eecb40023d8fa2c92e76b4ec2d6
# Parent  ace701efe203b4a6420b88a30696cc990fe308b2
prefer sys.error over plain error in Scala to avoid deprecation warning

diff -r ace701efe203 -r 1b609a7837ef src/HOL/HOL.thy
--- 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 *}
 
diff -r ace701efe203 -r 1b609a7837ef src/HOL/Imperative_HOL/Array.thy
--- 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((_))")
diff -r ace701efe203 -r 1b609a7837ef src/HOL/Imperative_HOL/Heap_Monad.thy
--- 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 *}
diff -r ace701efe203 -r 1b609a7837ef src/HOL/Imperative_HOL/Ref.thy
--- 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((_), (_))")
diff -r ace701efe203 -r 1b609a7837ef src/HOL/Library/Code_Integer.thy
--- 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.* ((_), (_))")
diff -r ace701efe203 -r 1b609a7837ef src/HOL/Library/Efficient_Nat.thy
--- 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 *}
diff -r ace701efe203 -r 1b609a7837ef src/HOL/Library/Target_Numeral.thy
--- 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.* ((_), (_))")
diff -r ace701efe203 -r 1b609a7837ef src/Tools/Code/code_scala.ML
--- 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*)