equal
deleted
inserted
replaced
85 val lines = Pretty.string_of(yxml).trim() |
85 val lines = Pretty.string_of(yxml).trim() |
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, "finalize") => action + " finalize " |
88 case List("mirabelle", action, "finalize") => action + " finalize " |
89 case List("mirabelle", action, "goal", goal_name, line, offset) => |
89 case List("mirabelle", action, "goal", goal_name, line, offset) => |
90 action + " goal." + goal_name + " " + args.theory_name + " " + |
90 action + " goal." + String.format("%-5s", goal_name) + " " + args.theory_name + " " + |
91 line + ":" + offset + " " |
91 line + ":" + offset + " " |
92 case _ => "" |
92 case _ => "" |
93 } |
93 } |
94 val body = Library.prefix_lines(prefix, lines) + "\n" |
94 val body = Library.prefix_lines(prefix, lines) + "\n" |
95 val log_file = output_dir + Path.basic("mirabelle.log") |
95 val log_file = output_dir + Path.basic("mirabelle.log") |