Commit 82407c0e authored by Stefan Berghofer's avatar Stefan Berghofer
Browse files

Adapted to changes in printer interface

parent 28e07a2f
......@@ -179,6 +179,7 @@ let rec print_term info defs fmt t = match t.t_node with
| Tconst c ->
let number_format = {
Number.long_int_support = true;
Number.extra_leading_zeros_support = true;
Number.dec_int_support = Number.Number_custom
"<num val=\"%s\"><type name=\"Int.int\"/></num>";
Number.hex_int_support = Number.Number_unsupported;
......@@ -402,10 +403,8 @@ let print_decl info fmt d =
let print_decls info fmt dl =
print_list nothing (print_decl info) fmt dl
let print_task env pr thpr _blacklist realize fmt task =
let print_task printer_args realize fmt task =
forget_ids ();
print_prelude fmt pr;
print_th_prelude task fmt thpr;
(* find theories that are both used and realized from metas *)
let realized_theories =
Task.on_meta meta_realized_theory (fun mid args ->
......@@ -414,7 +413,7 @@ let print_task env pr thpr _blacklist realize fmt task =
let f,id =
let l = Strings.rev_split s1 '.' in
List.rev (List.tl l), List.hd l in
let th = Env.find_theory env f id in
let th = Env.find_theory printer_args.env f id in
Mid.add th.Theory.th_name (th, s1) mid
| _ -> assert false
) Mid.empty task in
......@@ -466,11 +465,11 @@ let print_task env pr thpr _blacklist realize fmt task =
((thname, opt_string_of_bool realize),
(Mid.values realized_theories, local_decls))
let print_task_full env pr thpr blacklist ?old fmt task =
print_task env pr thpr blacklist false fmt task
let print_task_full args ?old fmt task =
print_task args false fmt task
let print_task_real env pr thpr blacklist ?old fmt task =
print_task env pr thpr blacklist true fmt task
let print_task_real args ?old fmt task =
print_task args true fmt task
let () = register_printer "isabelle" print_task_full
~desc:"Printer@ for@ the@ Isabelle@ proof@ assistant@ \
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment