Commit 63980293 authored by François Bobot's avatar François Bobot
Browse files

why3html : add class verified and notverified

parent 9747a484
.verified{
color: green;
}
.notverified{
color: red;
}
\ No newline at end of file
...@@ -193,15 +193,22 @@ end ...@@ -193,15 +193,22 @@ end
module Jstree = module Jstree =
struct struct
let print_verified fmt b =
if b
then fprintf fmt "class='verified'"
else fprintf fmt "class='notverified'"
let print_prover fmt = function let print_prover fmt = function
| Detected_prover pd -> fprintf fmt "%s" pd.prover_name | Detected_prover pd -> fprintf fmt "%s" pd.prover_name
| Undetected_prover s -> fprintf fmt "%s" s | Undetected_prover s -> fprintf fmt "%s" s
let print_proof_status fmt = function let print_proof_status fmt = function
| Undone -> fprintf fmt "Undone" | Undone -> fprintf fmt "<span class='notverified'>Undone</span>"
| Done pr -> fprintf fmt "Done : %a" Call_provers.print_prover_result pr | Done pr -> fprintf fmt "<span class='verified'>Done : %a</span>"
Call_provers.print_prover_result pr
| InternalFailure exn -> | InternalFailure exn ->
fprintf fmt "Failure : %a"Exn_printer.exn_printer exn fprintf fmt "<span class='notverified'>Failure : %a</span>"
Exn_printer.exn_printer exn
let print_proof_attempt fmt pa = let print_proof_attempt fmt pa =
fprintf fmt "@[<hov><li rel='prover' ><a href='#'>%a : %a</a></li>@]" fprintf fmt "@[<hov><li rel='prover' ><a href='#'>%a : %a</a></li>@]"
...@@ -210,13 +217,17 @@ struct ...@@ -210,13 +217,17 @@ struct
let rec print_transf fmt tr = let rec print_transf fmt tr =
fprintf fmt fprintf fmt
"@[<hov><li rel='transf'><a href='#'>%s</a>@,<ul>%a</ul></li>@]" "@[<hov><li rel='transf'><a href='#'>\
<span %a>%s</span></a>@,<ul>%a</ul></li>@]"
print_verified tr.transf_verified
tr.transf_name tr.transf_name
(Pp.print_list Pp.newline print_goal) tr.subgoals (Pp.print_list Pp.newline print_goal) tr.subgoals
and print_goal fmt g = and print_goal fmt g =
fprintf fmt fprintf fmt
"@[<hov><li rel='goal'><a href='#'>%s</a>@,<ul>%a%a</ul></li>@]" "@[<hov><li rel='goal'><a href='#'>\
<span %a>%s</a></a>@,<ul>%a%a</ul></li>@]"
print_verified g.goal_verified
g.goal_name g.goal_name
(Pp.print_iter2 Mstr.iter Pp.newline Pp.nothing (Pp.print_iter2 Mstr.iter Pp.newline Pp.nothing
Pp.nothing print_proof_attempt) Pp.nothing print_proof_attempt)
...@@ -227,12 +238,17 @@ struct ...@@ -227,12 +238,17 @@ struct
let print_theory fmt th = let print_theory fmt th =
fprintf fmt fprintf fmt
"@[<hov><li rel='theory'><a href='#'>%s</a>@,<ul>%a</ul></li>@]" "@[<hov><li rel='theory'><a href='#'>\
<span %a>%s</span></a>@,<ul>%a</ul></li>@]"
print_verified th.theory_verified
th.theory_name th.theory_name
(Pp.print_list Pp.newline print_goal) th.goals (Pp.print_list Pp.newline print_goal) th.goals
let print_file fmt f = let print_file fmt f =
fprintf fmt "@[<hov><li rel='file'><a href='#'>%s</a>@,<ul>%a</ul></li>@]" fprintf fmt
"@[<hov><li rel='file'><a href='#'>\
<span %a>%s</span></a>@,<ul>%a</ul></li>@]"
print_verified f.file_verified
f.file_name f.file_name
(Pp.print_list Pp.newline print_theory) f.theories (Pp.print_list Pp.newline print_theory) f.theories
...@@ -289,6 +305,8 @@ PUBLIC \"-//W3C//DTD XHTML 1.0 Strict//EN\" ...@@ -289,6 +305,8 @@ PUBLIC \"-//W3C//DTD XHTML 1.0 Strict//EN\"
<head> <head>
<meta http-equiv=\"Content-Type\" content=\"text/html; charset=utf-8\" /> <meta http-equiv=\"Content-Type\" content=\"text/html; charset=utf-8\" />
<title>Why3 session of %s</title> <title>Why3 session of %s</title>
<link rel=\"stylesheet\" type=\"text/css\"
href=\"javascript/session.css\" />
<script type=\"text/javascript\" src=\"javascript/jquery.js\"></script> <script type=\"text/javascript\" src=\"javascript/jquery.js\"></script>
<script type=\"text/javascript\" src=\"javascript/jquery.jstree.js\"> <script type=\"text/javascript\" src=\"javascript/jquery.jstree.js\">
</script> </script>
......
Markdown is supported
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