Commit 4ea727a2 authored by MARCHE Claude's avatar MARCHE Claude

Fixed HTML dump of sessions, and the doc

parent 89c38c59
......@@ -771,9 +771,13 @@ There are three styles of output: 'table', 'simpletree' and
\end{figure}
The style 'table' outputs the contents of the session as a table,
similar to the LaTeX output above. Figure~\ref{fig:html} is the HTML table
produced for the 'HelloProof' example, as typically shown in a Web
browser.
similar to the LaTeX output above. Figure~\ref{fig:html} is the HTML
table produced for the 'HelloProof' example, as typically shown in a
Web browser. The gray cells filled with \texttt{---} just mean that
the prover was not run on the corresponding goal. Green background
means the result was ``Valid'', other cases are in orange
background. The red background for a goal means that the goal was not
proved.
The style ''simpletree' displays the contents of the session under the form of tree, similar to the tree view in the IDE. It uses only basic HTMl tags such as \verb|<ul>| and \verb|<li>|.
......
......@@ -132,7 +132,8 @@ let print_results fmt provers proofs =
try
let pr = S.PHprover.find proofs p in
let s = pr.S.proof_state in
match s with
begin
match s with
| S.Done res ->
begin
match res.Call_provers.pr_answer with
......@@ -153,6 +154,8 @@ let print_results fmt provers proofs =
end
| S.Undone _ -> fprintf fmt "E0E0E0\">Undone"
| S.InternalFailure _ -> fprintf fmt "E0E0E0\">Internal Failure"
end;
if pr.S.proof_obsolete then fprintf fmt "(obsolete)"
with Not_found -> fprintf fmt "E0E0E0\">---"
end;
fprintf fmt "</td>") provers
......
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