86 val prefix = |
86 val prefix = |
87 Export.explode_name(args.name) match { |
87 Export.explode_name(args.name) match { |
88 case List("mirabelle", action, "initialize") => action + " initialize " |
88 case List("mirabelle", action, "initialize") => action + " initialize " |
89 case List("mirabelle", action, "finalize") => action + " finalize " |
89 case List("mirabelle", action, "finalize") => action + " finalize " |
90 case List("mirabelle", action, "goal", goal_name, line, offset, cpu_ms) => |
90 case List("mirabelle", action, "goal", goal_name, line, offset, cpu_ms) => |
91 action + " goal." + String.format("%-5s", goal_name) + " " + String.format("%5sms", cpu_ms) + " " + |
91 action + " goal." + String.format("%-9s", goal_name) + " " + String.format("%5sms", cpu_ms) + " " + |
92 args.theory_name + " " + line + ":" + offset + " " |
92 args.theory_name + " " + line + ":" + offset + " " |
93 case _ => "" |
93 case _ => "" |
94 } |
94 } |
95 val body = (if (lines == "") prefix else Library.prefix_lines(prefix, lines)) + "\n" |
95 val body = (if (lines == "") prefix else Library.prefix_lines(prefix, lines)) + "\n" |
96 val log_file = output_dir + Path.basic("mirabelle.log") |
96 val log_file = output_dir + Path.basic("mirabelle.log") |