# HG changeset patch
# User haftmann
# Date 1263487658 -3600
# Node ID 62d70417f8ce16b3a2f3813a0b54e42121a6b20a
# Parent  19fd499cddff39affb8f42abb7c05fdae46dfde0
allow individual printing of numerals during code serialization

diff -r 19fd499cddff -r 62d70417f8ce src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Wed Jan 13 12:20:37 2010 +0100
+++ b/src/HOL/Code_Numeral.thy	Thu Jan 14 17:47:38 2010 +0100
@@ -296,8 +296,11 @@
 
 setup {*
   fold (Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
-    false false) ["SML", "Haskell", "Scala"]
-  #> Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral} false true "OCaml"
+    false false Code_Printer.str) ["SML", "Haskell"]
+  #> Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
+    false true Code_Printer.str "OCaml"
+  #> Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
+    false false Code_Printer.str "Scala"
 *}
 
 code_reserved SML Int int
@@ -323,9 +326,10 @@
   (Scala infixl 8 "*")
 
 code_const div_mod_code_numeral
-  (SML "(fn n => fn m =>/ if m = 0/ then (0, n) else/ (n div m, n mod m))")
-  (OCaml "(fun k -> fun l ->/ Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int k)/ (Big'_int.abs'_big'_int l))")
+  (SML "!(fn n => fn m =>/ if m = 0/ then (0, n) else/ (n div m, n mod m))")
+  (OCaml "Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int _)/ (Big'_int.abs'_big'_int _)")
   (Haskell "divMod")
+  (Scala "!((n: Int) => (m: Int) =>/ if (m == 0)/ (0, n) else/ (n '/ m, n % m))")
 
 code_const "eq_class.eq \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
   (SML "!((_ : Int.int) = _)")
@@ -337,12 +341,12 @@
   (SML "Int.<=/ ((_),/ (_))")
   (OCaml "Big'_int.le'_big'_int")
   (Haskell infix 4 "<=")
-  (Scala infix 4 "<=")
+  (Scala infixl 4 "<=")
 
 code_const "op < \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
   (SML "Int.</ ((_),/ (_))")
   (OCaml "Big'_int.lt'_big'_int")
   (Haskell infix 4 "<")
-  (Scala infix 4 "<")
+  (Scala infixl 4 "<")
 
 end
diff -r 19fd499cddff -r 62d70417f8ce src/HOL/Tools/numeral.ML
--- a/src/HOL/Tools/numeral.ML	Wed Jan 13 12:20:37 2010 +0100
+++ b/src/HOL/Tools/numeral.ML	Thu Jan 14 17:47:38 2010 +0100
@@ -8,7 +8,7 @@
 sig
   val mk_cnumeral: int -> cterm
   val mk_cnumber: ctyp -> int -> cterm
-  val add_code: string -> bool -> bool -> string -> theory -> theory
+  val add_code: string -> bool -> bool -> (string -> Pretty.T) -> string -> theory -> theory
 end;
 
 structure Numeral: NUMERAL =
@@ -56,7 +56,7 @@
 
 local open Basic_Code_Thingol in
 
-fun add_code number_of negative unbounded target thy =
+fun add_code number_of negative unbounded print target thy =
   let
     fun dest_numeral pls' min' bit0' bit1' thm =
       let
@@ -74,11 +74,12 @@
           | dest_num _ = Code_Printer.eqn_error thm "Illegal numeral expression: illegal term";
       in dest_num end;
     fun pretty literals [pls', min', bit0', bit1'] _ thm _ _ [(t, _)] =
-      (Code_Printer.str o Code_Printer.literal_numeral literals unbounded
+      (print o Code_Printer.literal_numeral literals unbounded
         o the_default 0 o dest_numeral pls' min' bit0' bit1' thm) t;
   in
     thy |> Code_Target.add_syntax_const target number_of
-      (SOME (1, ([@{const_name Int.Pls}, @{const_name Int.Min}, @{const_name Int.Bit0}, @{const_name Int.Bit1}], pretty)))
+      (SOME (1, ([@{const_name Int.Pls}, @{const_name Int.Min},
+        @{const_name Int.Bit0}, @{const_name Int.Bit1}], pretty)))
   end;
 
 end; (*local*)