equal
deleted
inserted
replaced
439 (make_vars reserved) args_num is_singleton_constr deresolve; |
439 (make_vars reserved) args_num is_singleton_constr deresolve; |
440 |
440 |
441 (* print nodes *) |
441 (* print nodes *) |
442 fun print_implicits [] = NONE |
442 fun print_implicits [] = NONE |
443 | print_implicits implicits = (SOME o Pretty.block) |
443 | print_implicits implicits = (SOME o Pretty.block) |
444 (str "import /*implicits*/" :: Pretty.brk 1 :: Pretty.commas (map (str o deresolve) implicits)); |
444 (str "import /*implicits*/" :: Pretty.brk 1 :: commas (map (str o deresolve) implicits)); |
445 fun print_module base implicits p = Pretty.chunks2 |
445 fun print_module base implicits p = Pretty.chunks2 |
446 ([str ("object " ^ base ^ " {")] @ the_list (print_implicits implicits) |
446 ([str ("object " ^ base ^ " {")] @ the_list (print_implicits implicits) |
447 @ [p, str ("} /* object " ^ base ^ " */")]); |
447 @ [p, str ("} /* object " ^ base ^ " */")]); |
448 fun print_node (_, Dummy) = NONE |
448 fun print_node (_, Dummy) = NONE |
449 | print_node (name, Stmt stmt) = if null presentation_stmt_names |
449 | print_node (name, Stmt stmt) = if null presentation_stmt_names |