simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-07 11:45:41 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

Fix for bad html printing

Browse source
This commit is contained in:
Guillaume Bury 2015-01-29 15:14:24 +01:00
parent 863a49a0a4
commit b6089e67c3
1 changed files with 9 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
solver/mcproof.ml
View file

@ -350,10 +350,15 @@ module Make(St : Mcsolver_types.S) = struct
let name, f_args, t_args, color = St.proof_debug proof in
let color = match color with None -> "YELLOW" | Some c -> c in
let aux fmt () =
Format.fprintf fmt "<TR><TD colspan=\"2\">%a</TD></TR><TR><TD BGCOLOR=\"%s\" rowspan=\"%d\">%s</TD>%a%a</TR>"
print_clause p.conclusion color (List.length f_args + List.length t_args) name
(fun fmt -> List.iter (fun a -> Format.fprintf fmt "<TD>%a</TD>" St.print_atom a)) f_args
(fun fmt -> List.iter (fun v -> Format.fprintf fmt "<TD>%a</TD>" St.print_semantic_var v)) t_args
Format.fprintf fmt "<TR><TD colspan=\"2\">%a</TD></TR><TR><TD BGCOLOR=\"%s\" rowspan=\"%d\">%s</TD>"
print_clause p.conclusion color (List.length f_args + List.length t_args) name;
if f_args <> [] then
Format.fprintf fmt "<TD>%a</TD>%a%a" St.print_atom (List.hd f_args)
(fun fmt -> List.iter (fun a -> Format.fprintf fmt "<TR><TD>%a</TD></TR>" St.print_atom a)) (List.tl f_args)
(fun fmt -> List.iter (fun v -> Format.fprintf fmt "<TR><TD>%a</TD></TR>" St.print_semantic_var v)) t_args
else
Format.fprintf fmt "<TD>%a</TD>%a" St.print_semantic_var (List.hd t_args)
(fun fmt -> List.iter (fun v -> Format.fprintf fmt "<TR><TD>%a</TD></TR>" St.print_semantic_var v)) (List.tl t_args)
in
print_dot_rule "BGCOLOR=\"LIGHTBLUE\"" aux () fmt p.conclusion
| Resolution (proof1, proof2, a) ->