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 |