prefer sys.error over plain error in Scala to avoid deprecation warning
authorhaftmann
Tue Jun 05 07:10:51 2012 +0200 (2012-06-05)
changeset 480731b609a7837ef
parent 48072 ace701efe203
child 48074 c6d514717d7b
prefer sys.error over plain error in Scala to avoid deprecation warning
src/HOL/HOL.thy
src/HOL/Imperative_HOL/Array.thy
src/HOL/Imperative_HOL/Heap_Monad.thy
src/HOL/Imperative_HOL/Ref.thy
src/HOL/Library/Code_Integer.thy
src/HOL/Library/Efficient_Nat.thy
src/HOL/Library/Target_Numeral.thy
src/Tools/Code/code_scala.ML
     1.1 --- a/src/HOL/HOL.thy	Tue Jun 05 07:05:56 2012 +0200
     1.2 +++ b/src/HOL/HOL.thy	Tue Jun 05 07:10:51 2012 +0200
     1.3 @@ -1903,7 +1903,7 @@
     1.4    (SML "!(raise/ Fail/ \"undefined\")")
     1.5    (OCaml "failwith/ \"undefined\"")
     1.6    (Haskell "error/ \"undefined\"")
     1.7 -  (Scala "!error(\"undefined\")")
     1.8 +  (Scala "!sys.error(\"undefined\")")
     1.9  
    1.10  subsubsection {* Evaluation and normalization by evaluation *}
    1.11  
     2.1 --- a/src/HOL/Imperative_HOL/Array.thy	Tue Jun 05 07:05:56 2012 +0200
     2.2 +++ b/src/HOL/Imperative_HOL/Array.thy	Tue Jun 05 07:10:51 2012 +0200
     2.3 @@ -491,7 +491,7 @@
     2.4  text {* Scala *}
     2.5  
     2.6  code_type array (Scala "!collection.mutable.ArraySeq[_]")
     2.7 -code_const Array (Scala "!error(\"bare Array\")")
     2.8 +code_const Array (Scala "!sys.error(\"bare Array\")")
     2.9  code_const Array.new' (Scala "('_: Unit)/ => / Array.alloc((_))((_))")
    2.10  code_const Array.make' (Scala "('_: Unit)/ =>/ Array.make((_))((_))")
    2.11  code_const Array.len' (Scala "('_: Unit)/ =>/ Array.len((_))")
     3.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Tue Jun 05 07:05:56 2012 +0200
     3.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Tue Jun 05 07:10:51 2012 +0200
     3.3 @@ -610,7 +610,7 @@
     3.4  code_type Heap (Scala "Unit/ =>/ _")
     3.5  code_const bind (Scala "Heap.bind")
     3.6  code_const return (Scala "('_: Unit)/ =>/ _")
     3.7 -code_const Heap_Monad.raise' (Scala "!error((_))")
     3.8 +code_const Heap_Monad.raise' (Scala "!sys.error((_))")
     3.9  
    3.10  
    3.11  subsubsection {* Target variants with less units *}
     4.1 --- a/src/HOL/Imperative_HOL/Ref.thy	Tue Jun 05 07:05:56 2012 +0200
     4.2 +++ b/src/HOL/Imperative_HOL/Ref.thy	Tue Jun 05 07:10:51 2012 +0200
     4.3 @@ -313,7 +313,7 @@
     4.4  text {* Scala *}
     4.5  
     4.6  code_type ref (Scala "!Ref[_]")
     4.7 -code_const Ref (Scala "!error(\"bare Ref\")")
     4.8 +code_const Ref (Scala "!sys.error(\"bare Ref\")")
     4.9  code_const ref' (Scala "('_: Unit)/ =>/ Ref((_))")
    4.10  code_const Ref.lookup (Scala "('_: Unit)/ =>/ Ref.lookup((_))")
    4.11  code_const Ref.update (Scala "('_: Unit)/ =>/ Ref.update((_), (_))")
     5.1 --- a/src/HOL/Library/Code_Integer.thy	Tue Jun 05 07:05:56 2012 +0200
     5.2 +++ b/src/HOL/Library/Code_Integer.thy	Tue Jun 05 07:10:51 2012 +0200
     5.3 @@ -111,7 +111,7 @@
     5.4    (SML "!(raise/ Fail/ \"sub\")")
     5.5    (OCaml "failwith/ \"sub\"")
     5.6    (Haskell "error/ \"sub\"")
     5.7 -  (Scala "!error(\"sub\")")
     5.8 +  (Scala "!sys.error(\"sub\")")
     5.9  
    5.10  code_const "op * \<Colon> int \<Rightarrow> int \<Rightarrow> int"
    5.11    (SML "IntInf.* ((_), (_))")
     6.1 --- a/src/HOL/Library/Efficient_Nat.thy	Tue Jun 05 07:05:56 2012 +0200
     6.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Tue Jun 05 07:10:51 2012 +0200
     6.3 @@ -228,7 +228,7 @@
     6.4    (SML "!(raise/ Fail/ \"sub\")")
     6.5    (OCaml "failwith/ \"sub\"")
     6.6    (Haskell "error/ \"sub\"")
     6.7 -  (Scala "!error(\"sub\")")
     6.8 +  (Scala "!sys.error(\"sub\")")
     6.9  
    6.10  code_const "times \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"
    6.11    (SML "IntInf.*/ ((_),/ (_))")
    6.12 @@ -269,7 +269,7 @@
    6.13    (SML "!(raise/ Fail/ \"num'_of'_nat\")")
    6.14    (OCaml "failwith/ \"num'_of'_nat\"")
    6.15    (Haskell "error/ \"num'_of'_nat\"")
    6.16 -  (Scala "!error(\"num'_of'_nat\")")
    6.17 +  (Scala "!sys.error(\"num'_of'_nat\")")
    6.18  
    6.19  
    6.20  subsection {* Evaluation *}
     7.1 --- a/src/HOL/Library/Target_Numeral.thy	Tue Jun 05 07:05:56 2012 +0200
     7.2 +++ b/src/HOL/Library/Target_Numeral.thy	Tue Jun 05 07:10:51 2012 +0200
     7.3 @@ -465,7 +465,7 @@
     7.4    (SML "!(raise/ Fail/ \"sub\")")
     7.5    (OCaml "failwith/ \"sub\"")
     7.6    (Haskell "error/ \"sub\"")
     7.7 -  (Scala "!error(\"sub\")")
     7.8 +  (Scala "!sys.error(\"sub\")")
     7.9  
    7.10  code_const "times :: Target_Numeral.int \<Rightarrow> _ \<Rightarrow> _"
    7.11    (SML "IntInf.* ((_), (_))")
     8.1 --- a/src/Tools/Code/code_scala.ML	Tue Jun 05 07:05:56 2012 +0200
     8.2 +++ b/src/Tools/Code/code_scala.ML	Tue Jun 05 07:10:51 2012 +0200
     8.3 @@ -101,7 +101,7 @@
     8.4      and print_bind tyvars some_thm fxy p =
     8.5        gen_print_bind (print_term tyvars true) some_thm fxy p
     8.6      and print_case tyvars some_thm vars fxy { clauses = [], ... } =
     8.7 -          (brackify fxy o Pretty.breaks o map str) ["error(\"empty case\")"]
     8.8 +          (brackify fxy o Pretty.breaks o map str) ["sys.error(\"empty case\")"]
     8.9        | print_case tyvars some_thm vars fxy (case_expr as { clauses = [_], ... }) =
    8.10            let
    8.11              val (bind :: binds, body) = Code_Thingol.unfold_let (ICase case_expr);
    8.12 @@ -155,7 +155,7 @@
    8.13              val vars = intro_vars params reserved;
    8.14            in
    8.15              concat [print_defhead tyvars vars name vs params tys ty',
    8.16 -              str ("error(\"" ^ name ^ "\")")]
    8.17 +              str ("sys.error(\"" ^ name ^ "\")")]
    8.18            end
    8.19        | print_def name (vs, ty) eqs =
    8.20            let
    8.21 @@ -439,7 +439,7 @@
    8.22        "true", "type", "val", "var", "while", "with", "yield"
    8.23      ]
    8.24    #> fold (Code_Target.add_reserved target) [
    8.25 -      "apply", "error", "scala", "BigInt", "Nil", "List"
    8.26 +      "apply", "sys", "scala", "BigInt", "Nil", "List"
    8.27      ];
    8.28  
    8.29  end; (*struct*)