src/Tools/Code/code_scala.ML
changeset 34900 9b12b0824bfe
parent 34888 460ec1a99aa2
child 34944 970e1466028d
     1.1 --- a/src/Tools/Code/code_scala.ML	Thu Jan 14 17:47:39 2010 +0100
     1.2 +++ b/src/Tools/Code/code_scala.ML	Thu Jan 14 17:47:39 2010 +0100
     1.3 @@ -71,7 +71,7 @@
     1.4                (applify "[" "]" NOBR ((str o deresolve) c) (map (print_typ tyvars NOBR) tys'))
     1.5                  (map (print_term tyvars is_pat thm vars NOBR) ts))
     1.6            | SOME (_, print) => (false, fn ts =>
     1.7 -              print (print_term tyvars is_pat thm) thm vars fxy (ts ~~ take k tys_args));
     1.8 +              print (print_term tyvars is_pat thm) thm vars fxy (ts ~~ take l tys_args));
     1.9        in if k = l then print' ts
    1.10        else if k < l then
    1.11          print_term tyvars is_pat thm vars fxy (Code_Thingol.eta_expand l app)
    1.12 @@ -404,11 +404,17 @@
    1.13      let
    1.14        val s = ML_Syntax.print_char c;
    1.15      in if s = "'" then "\\'" else s end;
    1.16 +  fun bigint_scala k = "(" ^ (if k <= 2147483647
    1.17 +    then string_of_int k else quote (string_of_int k)) ^ ")"
    1.18  in Literals {
    1.19    literal_char = Library.enclose "'" "'" o char_scala,
    1.20    literal_string = quote o translate_string char_scala,
    1.21 -  literal_numeral = fn unbounded => fn k => if k >= 0 then string_of_int k
    1.22 -    else Library.enclose "(" ")" (signed_string_of_int k),
    1.23 +  literal_numeral = fn unbounded => fn k => if k >= 0 then
    1.24 +      if unbounded then bigint_scala k
    1.25 +      else Library.enclose "(" ")" (string_of_int k)
    1.26 +    else
    1.27 +      if unbounded then "(- " ^ bigint_scala (~ k) ^ ")"
    1.28 +      else Library.enclose "(" ")" (signed_string_of_int k),
    1.29    literal_list = fn [] => str "Nil" | ps => Pretty.block [str "List", enum "," "(" ")" ps],
    1.30    infix_cons = (6, "::")
    1.31  } end;
    1.32 @@ -424,7 +430,7 @@
    1.33    Code_Target.add_target (target, (isar_seri_scala, literals))
    1.34    #> Code_Target.add_syntax_tyco target "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
    1.35        brackify_infix (1, R) fxy [
    1.36 -        print_typ (INFX (1, X)) ty1,
    1.37 +        print_typ BR ty1 (*product type vs. tupled arguments!*),
    1.38          str "=>",
    1.39          print_typ (INFX (1, R)) ty2
    1.40        ]))