equal
deleted
inserted
replaced
83 } |
83 } |
84 val yxml = YXML.parse_body(UTF8.decode_permissive(msg.chunk), cache = store.cache) |
84 val yxml = YXML.parse_body(UTF8.decode_permissive(msg.chunk), cache = store.cache) |
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, "initialize") => action + " initialize " |
|
89 case List("mirabelle", action, "finalize") => action + " finalize " |
89 case List("mirabelle", action, "goal", goal_name, line, offset) => |
90 case List("mirabelle", action, "goal", goal_name, line, offset) => |
90 action + " goal." + String.format("%-5s", goal_name) + " " + args.theory_name + " " + |
91 action + " goal." + String.format("%-5s", goal_name) + " " + args.theory_name + " " + |
91 line + ":" + offset + " " |
92 line + ":" + offset + " " |
92 case _ => "" |
93 case _ => "" |
93 } |
94 } |