src/Tools/Code/code_scala.ML
changeset 38971 5d49165a192e
parent 38970 53d1ee3d98b8
parent 38968 e55deaa22fff
child 39022 ac7774a35bcf
     1.1 --- a/src/Tools/Code/code_scala.ML	Wed Sep 01 12:01:19 2010 +0200
     1.2 +++ b/src/Tools/Code/code_scala.ML	Wed Sep 01 12:01:44 2010 +0200
     1.3 @@ -388,8 +388,7 @@
     1.4        in if null ps then NONE else SOME (Pretty.chunks2 ps) end;
     1.5  
     1.6      (* serialization *)
     1.7 -    val p_includes = if null presentation_names
     1.8 -      then map (fn (base, p) => print_module base [] p) includes else [];
     1.9 +    val p_includes = if null presentation_names then map snd includes else [];
    1.10      val p = Pretty.chunks2 (p_includes @ the_list (print_nodes [] sca_program));
    1.11      fun write width NONE = writeln_pretty width
    1.12        | write width (SOME p) = File.write p o string_of_pretty width;
    1.13 @@ -415,8 +414,8 @@
    1.14    literal_char = Library.enclose "'" "'" o char_scala,
    1.15    literal_string = quote o translate_string char_scala,
    1.16    literal_numeral = fn k => "BigInt(" ^ numeral_scala k ^ ")",
    1.17 -  literal_positive_numeral = fn k => "Nat.Nat(" ^ numeral_scala k ^ ")",
    1.18 -  literal_alternative_numeral = fn k => "Natural.Nat(" ^ numeral_scala k ^ ")",
    1.19 +  literal_positive_numeral = fn k => "Nat(" ^ numeral_scala k ^ ")",
    1.20 +  literal_alternative_numeral = fn k => "Natural(" ^ numeral_scala k ^ ")",
    1.21    literal_naive_numeral = fn k => "BigInt(" ^ numeral_scala k ^ ")",
    1.22    literal_list = fn [] => str "Nil" | ps => Pretty.block [str "List", enum "," "(" ")" ps],
    1.23    infix_cons = (6, "::")