src/Tools/Code/code_scala.ML
changeset 38968 e55deaa22fff
parent 38966 68853347ba37
child 38971 5d49165a192e
equal deleted inserted replaced
38967:b912278b719f 38968:e55deaa22fff
   475           snd (Graph.get_node nodes name)))
   475           snd (Graph.get_node nodes name)))
   476             ((rev o flat o Graph.strong_conn) nodes);
   476             ((rev o flat o Graph.strong_conn) nodes);
   477       in if null ps then NONE else SOME (Pretty.chunks2 ps) end;
   477       in if null ps then NONE else SOME (Pretty.chunks2 ps) end;
   478 
   478 
   479     (* serialization *)
   479     (* serialization *)
   480     val p_includes = if null presentation_names
   480     val p_includes = if null presentation_names then map snd includes else [];
   481       then map (fn (base, p) => print_module base [] p) includes else [];
       
   482     val p = Pretty.chunks2 (p_includes @ the_list (print_nodes [] sca_program));
   481     val p = Pretty.chunks2 (p_includes @ the_list (print_nodes [] sca_program));
   483     fun write width NONE = writeln_pretty width
   482     fun write width NONE = writeln_pretty width
   484       | write width (SOME p) = File.write p o string_of_pretty width;
   483       | write width (SOME p) = File.write p o string_of_pretty width;
   485   in
   484   in
   486     Code_Target.serialization write (rpair [] oo string_of_pretty) p
   485     Code_Target.serialization write (rpair [] oo string_of_pretty) p
   504       else quote (string_of_int k)
   503       else quote (string_of_int k)
   505 in Literals {
   504 in Literals {
   506   literal_char = Library.enclose "'" "'" o char_scala,
   505   literal_char = Library.enclose "'" "'" o char_scala,
   507   literal_string = quote o translate_string char_scala,
   506   literal_string = quote o translate_string char_scala,
   508   literal_numeral = fn k => "BigInt(" ^ numeral_scala k ^ ")",
   507   literal_numeral = fn k => "BigInt(" ^ numeral_scala k ^ ")",
   509   literal_positive_numeral = fn k => "Nat.Nat(" ^ numeral_scala k ^ ")",
   508   literal_positive_numeral = fn k => "Nat(" ^ numeral_scala k ^ ")",
   510   literal_alternative_numeral = fn k => "Natural.Nat(" ^ numeral_scala k ^ ")",
   509   literal_alternative_numeral = fn k => "Natural(" ^ numeral_scala k ^ ")",
   511   literal_naive_numeral = fn k => "BigInt(" ^ numeral_scala k ^ ")",
   510   literal_naive_numeral = fn k => "BigInt(" ^ numeral_scala k ^ ")",
   512   literal_list = fn [] => str "Nil" | ps => Pretty.block [str "List", enum "," "(" ")" ps],
   511   literal_list = fn [] => str "Nil" | ps => Pretty.block [str "List", enum "," "(" ")" ps],
   513   infix_cons = (6, "::")
   512   infix_cons = (6, "::")
   514 } end;
   513 } end;
   515 
   514