84 "Mirabelle export " + quote(args.compound_name) + " (in " + session_name + ")") |
84 "Mirabelle export " + quote(args.compound_name) + " (in " + session_name + ")") |
85 } |
85 } |
86 using(store.open_database_context())(db_context => |
86 using(store.open_database_context())(db_context => |
87 { |
87 { |
88 for (entry <- db_context.read_export(session_hierarchy, args.theory_name, args.name)) { |
88 for (entry <- db_context.read_export(session_hierarchy, args.theory_name, args.name)) { |
89 val prefix = args.name.split('/') match { |
89 val prefix = |
90 case Array("mirabelle", action, "finalize") => |
90 Export.explode_name(args.name) match { |
91 s"${action} finalize " |
91 case List("mirabelle", action, "finalize") => action + " finalize " |
92 case Array("mirabelle", action, "goal", goal_name, line, offset) => |
92 case List("mirabelle", action, "goal", goal_name, line, offset) => |
93 s"${action} goal.${goal_name} ${args.theory_name} ${line}:${offset} " |
93 action + " goal." + goal_name + " " + args.theory_name + " " + |
94 case _ => "" |
94 line + ":" + offset + " " |
95 } |
95 case _ => "" |
|
96 } |
96 val lines = Pretty.string_of(entry.uncompressed_yxml).trim() |
97 val lines = Pretty.string_of(entry.uncompressed_yxml).trim() |
97 val body = Library.prefix_lines(prefix, lines) + "\n" |
98 val body = Library.prefix_lines(prefix, lines) + "\n" |
98 val log_file = output_dir + Path.basic("mirabelle.log") |
99 val log_file = output_dir + Path.basic("mirabelle.log") |
99 File.append(log_file, body) |
100 File.append(log_file, body) |
100 } |
101 } |