Commit fd79bfde authored by Guillaume Melquiond's avatar Guillaume Melquiond

Merge branch 'bugfix/v0.87'

parents c4416c9a 28fe8606
...@@ -2,9 +2,6 @@ ...@@ -2,9 +2,6 @@
/examples/hoare_logic/draft/ export-ignore /examples/hoare_logic/draft/ export-ignore
/tests/ export-ignore /tests/ export-ignore
/bench/encoding/ export-ignore /bench/encoding/ export-ignore
/share/images/boomy/ export-ignore
/share/images/boomy.rc export-ignore
/share/javascript/ export-ignore
/misc/ export-ignore /misc/ export-ignore
/ROADMAP export-ignore /ROADMAP export-ignore
/DEVELOPER.readme export-ignore /DEVELOPER.readme export-ignore
...@@ -12,5 +9,4 @@ ...@@ -12,5 +9,4 @@
.gitignore export-ignore .gitignore export-ignore
.gitattributes export-ignore .gitattributes export-ignore
/check.sh export-ignore /check.sh export-ignore
/.merlin.in export-ignore
/TODO export-ignore /TODO export-ignore
* marks an incompatible change * marks an incompatible change
Version 0.87.0, March 15, 2016
================================
Language Language
* Add new logical connectives "by" and "so" as keywords * Add new logical connectives "by" and "so" as keywords
...@@ -8,6 +11,7 @@ Tools ...@@ -8,6 +11,7 @@ Tools
o add a command-line option --extra-expl-prefix to specify o add a command-line option --extra-expl-prefix to specify
additional possible prefixes for VC explanations. (Available for additional possible prefixes for VC explanations. (Available for
why3 commands "prove" and "ide".) why3 commands "prove" and "ide".)
* removed "jstree" style from the "session" command
Transformations Transformations
* All split transformations respect the "stop_split" label now. * All split transformations respect the "stop_split" label now.
...@@ -45,7 +49,7 @@ Provers ...@@ -45,7 +49,7 @@ Provers
o support for Zenon_modulo 0.4.1 (released Jul 2, 2015) o support for Zenon_modulo 0.4.1 (released Jul 2, 2015)
Distribution Distribution
* non-free files are distributed in an extra tar file: "boomy" icon set, * non-free files have been removed: "boomy" icon set,
javascript helpers for "why3 session html --style jstree" javascript helpers for "why3 session html --style jstree"
Version 0.86.3, February 8, 2016 Version 0.86.3, February 8, 2016
......
...@@ -315,7 +315,6 @@ endif ...@@ -315,7 +315,6 @@ endif
cp -f share/images/*.png $(DATADIR)/why3/images cp -f share/images/*.png $(DATADIR)/why3/images
cp -f share/why3session.dtd $(DATADIR)/why3 cp -f share/why3session.dtd $(DATADIR)/why3
cp -f share/Makefile.config $(DATADIR)/why3 cp -f share/Makefile.config $(DATADIR)/why3
cp -rf share/javascript $(DATADIR)/why3/javascript
cp -f share/vim/why3.vim $(DATADIR)/why3/vim/why3.vim cp -f share/vim/why3.vim $(DATADIR)/why3/vim/why3.vim
cp -f share/lang/why3.lang $(DATADIR)/why3/lang/why3.lang cp -f share/lang/why3.lang $(DATADIR)/why3/lang/why3.lang
...@@ -1927,8 +1926,6 @@ wc: ...@@ -1927,8 +1926,6 @@ wc:
NAME = why3-@VERSION@ NAME = why3-@VERSION@
# see .gitattributes for the list of files that are not distributed # see .gitattributes for the list of files that are not distributed
MORE_DIST = configure doc/manual.pdf MORE_DIST = configure doc/manual.pdf
EXTRANAME = why3-extra-@VERSION@
EXTRA_DIST = share/images/boomy.rc share/images/boomy share/javascript
dist: $(MORE_DIST) dist: $(MORE_DIST)
rm -rf distrib/$(NAME)/ distrib/$(NAME).tar.gz rm -rf distrib/$(NAME)/ distrib/$(NAME).tar.gz
...@@ -1937,9 +1934,6 @@ dist: $(MORE_DIST) ...@@ -1937,9 +1934,6 @@ dist: $(MORE_DIST)
git archive --format tar --prefix $(NAME)/ HEAD | tar x -C distrib/ git archive --format tar --prefix $(NAME)/ HEAD | tar x -C distrib/
for f in $(MORE_DIST); do cp $$f distrib/$(NAME)/$$f; done for f in $(MORE_DIST); do cp $$f distrib/$(NAME)/$$f; done
cd distrib; tar cf $(NAME).tar $(NAME); gzip -f --best $(NAME).tar cd distrib; tar cf $(NAME).tar $(NAME); gzip -f --best $(NAME).tar
mkdir distrib/$(EXTRANAME)
cp -r $(EXTRA_DIST) distrib/$(EXTRANAME)
cd distrib; tar cf $(EXTRANAME).tar $(EXTRANAME); gzip -f --best $(EXTRANAME).tar
############### ###############
......
...@@ -1599,7 +1599,6 @@ See manual Section xx ...@@ -1599,7 +1599,6 @@ See manual Section xx
* INSTALL (done) * INSTALL (done)
* LICENSE (done) * LICENSE (done)
* OCAML-LICENSE (done) * OCAML-LICENSE (done)
* TODO: licence pour les boomy icons
* debuguer cpulimit pour gappa (pb de return code) * debuguer cpulimit pour gappa (pb de return code)
......
# Why version # Why version
VERSION=0.86+git VERSION=0.87.0
...@@ -864,8 +864,8 @@ Section~\ref{chap:starting}, respectively with style 1 and 2. ...@@ -864,8 +864,8 @@ Section~\ref{chap:starting}, respectively with style 1 and 2.
\subsection{Command \texttt{html}} \subsection{Command \texttt{html}}
This command produces a summary of the proof session in HTML syntax. This command produces a summary of the proof session in HTML syntax.
There are three styles of output: `table', `simpletree', and There are two styles of output: `table' and `simpletree'. The default is
`jstree'. The default is `table'. `table'.
The file generated is named \texttt{why3session.html} and is written The file generated is named \texttt{why3session.html} and is written
in the session directory by default (see option \texttt{-o} to in the session directory by default (see option \texttt{-o} to
...@@ -908,16 +908,10 @@ The style `simpletree' displays the contents of the session under the ...@@ -908,16 +908,10 @@ 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 form of tree, similar to the tree view in the IDE. It uses only basic
HTML tags such as \verb|<ul>| and \verb|<li>|. HTML tags such as \verb|<ul>| and \verb|<li>|.
The style `jstree' displays a dynamic tree view of the session, where
you can click on various parts to expand or shrink some parts of the
tree. Clicking on an edited proof script also shows the contents of
this script. Technically, it uses the `jstree' plugin of the javascript
library `jquery'.
Specific options for this command are as follows. Specific options for this command are as follows.
\begin{description} \begin{description}
\item[\texttt{-{}-style \textsl{<style>}}] sets the style to use, among \item[\texttt{-{}-style \textsl{<style>}}] sets the style to use, among
\texttt{simpletree}, \texttt{jstree}, and \texttt{table}; defaults to \texttt{simpletree} and \texttt{table}; defaults to
\texttt{table}. \texttt{table}.
\item[\texttt{-o \textsl{<dir>}}] sets the directory where to output \item[\texttt{-o \textsl{<dir>}}] sets the directory where to output
......
...@@ -108,7 +108,7 @@ ...@@ -108,7 +108,7 @@
%BEGIN LATEX %BEGIN LATEX
\begin{LARGE} \begin{LARGE}
%END LATEX %END LATEX
Version \whyversion{}, February 2016 Version \whyversion{}, March 2016
%BEGIN LATEX %BEGIN LATEX
\end{LARGE} \end{LARGE}
%END LATEX %END LATEX
......
...@@ -69,7 +69,7 @@ timelimit = 2 ...@@ -69,7 +69,7 @@ timelimit = 2
default_editor = "editor %f" default_editor = "editor %f"
error_color = "orange" error_color = "orange"
goal_color = "gold" goal_color = "gold"
iconset = "boomy" iconset = "fatcow"
intro_premises = true intro_premises = true
premise_color = "chartreuse" premise_color = "chartreuse"
print_labels = false print_labels = false
......
archive: "https://gforge.inria.fr/frs/download.php/file/35537/why3-0.86.3.tar.gz" archive: "https://gforge.inria.fr/frs/download.php/file/35643/why3-0.87.0.tar.gz"
checksum: "910d5acca0082e94b8a86baf01600e03" checksum: "e587a45b94201de16529a15c72b978df"
...@@ -19,7 +19,7 @@ tags: [ ...@@ -19,7 +19,7 @@ tags: [
] ]
available: [ ocaml-version >= "4.01.0" ] available: [ ocaml-version >= "4.01.0" ]
depends: [ depends: [
"why3-base" { = "0.86.3" } "why3-base" { = "0.87.0" }
"lablgtk" "lablgtk"
"conf-gtksourceview" "conf-gtksourceview"
"zarith" "zarith"
......
...@@ -101,7 +101,7 @@ _why3() ...@@ -101,7 +101,7 @@ _why3()
return 0 return 0
;; ;;
--style) --style)
COMPREPLY=( $( compgen -W 'simple jstree' -- "$cur" ) ) COMPREPLY=( $( compgen -W 'simpletree table' -- "$cur" ) )
return 0 return 0
;; ;;
session) session)
......
[iconset boomy]
name = "Boomy"
license = "license.txt"
default = "undone32"
undone = "undone32"
scheduled = "pausehalf32"
running = "play32"
valid = "accept32"
unknown = "help32"
invalid = "delete32"
timeout = "clock32"
outofmemory = "deletefile32"
steplimitexceeded = "cut32"
failure = "bug32"
valid_obs = "obsaccept32"
unknown_obs = "obshelp32"
invalid_obs = "obsdelete32"
timeout_obs = "obsclock32"
outofmemory_obs = "obsdeletefile32"
steplimitexceeded_obs = "cut32"
failure_obs = "obsbug32"
yes = "accept32"
no = "delete32"
file = "folder32"
theory = "folder32"
goal = "file32"
prover = "wizard32"
transf = "configure32"
#TODO change metas
metas = "movefile32"
editor = "edit32"
replay = "refresh32"
cancel = "cut32"
reload = "movefile32"
remove = "delete32"
cleaning = "trashb32"
Boomy toolbar icon set license
This is a legal agreement between You, the user, and Milosz Wlazlo.
By downloading the Boomy icon set, You agree to the following:
All icons in the Boomy toolbar package are for personal use only. You
may also use the icons in open source and freeware projects as long as
you give credits to the author of the icons and link to his website
(miloszwl.deviantart.com).
The image data may be changed by You in a limited way, only by
combining the included icons and adjusting hue, saturation,
brightness.
All icons are provided "As is". The Miloszwl.com shall not be liable
for any kind of harm caused by use of, or the inability to use, this
icon set or any individual image.
You agree that all ownership and copyrights of the icons remain the
property of Milosz Wlazlo (Miloszwl.com). You may not resell or
redistribute the icons in any kind of commercial project or internet
icon archive.
Contact: miloszwl@miloszwl.com
Web: miloszwl.deviantart.com
This diff is collapsed.
This source diff could not be displayed because it is too large. You can view the blob instead.
.verified{
color: green;
}
.notverified{
color: red;
}
#edited{
right:0px;
top: 20px;
position: fixed;
z-index: 50;
width: 50%;
height: 600px;
}
function showedited(s){
var iframe = document.getElementById("edited");
var addr = "edited/"+s;
iframe.src = addr;
$("#edited").show()
}
\ No newline at end of file
/*
* jsTree default theme 1.0
* Supported features: dots/no-dots, icons/no-icons, focused, loading
* Supported plugins: ui (hovered, clicked), checkbox, contextmenu, search
*/
.jstree-default li,
.jstree-default ins { background-image:url("d.png"); background-repeat:no-repeat; background-color:transparent; }
.jstree-default li { background-position:-90px 0; background-repeat:repeat-y; }
.jstree-default li.jstree-last { background:transparent; }
.jstree-default .jstree-open > ins { background-position:-72px 0; }
.jstree-default .jstree-closed > ins { background-position:-54px 0; }
.jstree-default .jstree-leaf > ins { background-position:-36px 0; }
.jstree-default .jstree-hovered { background:#e7f4f9; border:1px solid #d8f0fa; padding:0 2px 0 1px; }
.jstree-default .jstree-clicked { background:#beebff; border:1px solid #99defd; padding:0 2px 0 1px; }
.jstree-default a .jstree-icon { background-position:-56px -19px; }
.jstree-default a.jstree-loading .jstree-icon { background:url("throbber.gif") center center no-repeat !important; }
.jstree-default.jstree-focused { background:#ffffee; }
.jstree-default .jstree-no-dots li,
.jstree-default .jstree-no-dots .jstree-leaf > ins { background:transparent; }
.jstree-default .jstree-no-dots .jstree-open > ins { background-position:-18px 0; }
.jstree-default .jstree-no-dots .jstree-closed > ins { background-position:0 0; }
.jstree-default .jstree-no-icons a .jstree-icon { display:none; }
.jstree-default .jstree-search { font-style:italic; }
.jstree-default .jstree-no-icons .jstree-checkbox { display:inline-block; }
.jstree-default .jstree-no-checkboxes .jstree-checkbox { display:none !important; }
.jstree-default .jstree-checked > a > .jstree-checkbox { background-position:-38px -19px; }
.jstree-default .jstree-unchecked > a > .jstree-checkbox { background-position:-2px -19px; }
.jstree-default .jstree-undetermined > a > .jstree-checkbox { background-position:-20px -19px; }
.jstree-default .jstree-checked > a > .jstree-checkbox:hover { background-position:-38px -37px; }
.jstree-default .jstree-unchecked > a > .jstree-checkbox:hover { background-position:-2px -37px; }
.jstree-default .jstree-undetermined > a > .jstree-checkbox:hover { background-position:-20px -37px; }
#vakata-dragged.jstree-default ins { background:transparent !important; }
#vakata-dragged.jstree-default .jstree-ok { background:url("d.png") -2px -53px no-repeat !important; }
#vakata-dragged.jstree-default .jstree-invalid { background:url("d.png") -18px -53px no-repeat !important; }
#jstree-marker.jstree-default { background:url("d.png") -41px -57px no-repeat !important; text-indent:-100px; }
.jstree-default a.jstree-search { color:aqua; }
.jstree-default .jstree-locked a { color:silver; cursor:default; }
#vakata-contextmenu.jstree-default-context,
#vakata-contextmenu.jstree-default-context li ul { background:#f0f0f0; border:1px solid #979797; -moz-box-shadow: 1px 1px 2px #999; -webkit-box-shadow: 1px 1px 2px #999; box-shadow: 1px 1px 2px #999; }
#vakata-contextmenu.jstree-default-context li { }
#vakata-contextmenu.jstree-default-context a { color:black; }
#vakata-contextmenu.jstree-default-context a:hover,
#vakata-contextmenu.jstree-default-context .vakata-hover > a { padding:0 5px; background:#e8eff7; border:1px solid #aecff7; color:black; -moz-border-radius:2px; -webkit-border-radius:2px; border-radius:2px; }
#vakata-contextmenu.jstree-default-context li.jstree-contextmenu-disabled a,
#vakata-contextmenu.jstree-default-context li.jstree-contextmenu-disabled a:hover { color:silver; background:transparent; border:0; padding:1px 4px; }
#vakata-contextmenu.jstree-default-context li.vakata-separator { background:white; border-top:1px solid #e0e0e0; margin:0; }
#vakata-contextmenu.jstree-default-context li ul { margin-left:-4px; }
/* IE6 BEGIN */
.jstree-default li,
.jstree-default ins,
#vakata-dragged.jstree-default .jstree-invalid,
#vakata-dragged.jstree-default .jstree-ok,
#jstree-marker.jstree-default { _background-image:url("d.gif"); }
.jstree-default .jstree-open ins { _background-position:-72px 0; }
.jstree-default .jstree-closed ins { _background-position:-54px 0; }
.jstree-default .jstree-leaf ins { _background-position:-36px 0; }
.jstree-default a ins.jstree-icon { _background-position:-56px -19px; }
#vakata-contextmenu.jstree-default-context ins { _display:none; }
#vakata-contextmenu.jstree-default-context li { _zoom:1; }
.jstree-default .jstree-undetermined a .jstree-checkbox { _background-position:-20px -19px; }
.jstree-default .jstree-checked a .jstree-checkbox { _background-position:-38px -19px; }
.jstree-default .jstree-unchecked a .jstree-checkbox { _background-position:-2px -19px; }
/* IE6 END */
\ No newline at end of file
...@@ -482,15 +482,6 @@ version_ok = "7.0" ...@@ -482,15 +482,6 @@ version_ok = "7.0"
command = "%e -noprompt" command = "%e -noprompt"
driver = "drivers/mathematica.drv" driver = "drivers/mathematica.drv"
[ATP safeprover]
name = "SafeProver"
exec = "safeprover"
version_switch = "-version"
version_regexp = "The safe prover, version \\([^ \n\t]+\\)"
version_ok = "0.0.0"
command = "%e %f"
driver = "drivers/safeprover.drv"
# Coq 8.5: do not limit memory # Coq 8.5: do not limit memory
[ITP coq] [ITP coq]
name = "Coq" name = "Coq"
......
...@@ -30,37 +30,35 @@ val create_label : string -> label ...@@ -30,37 +30,35 @@ val create_label : string -> label
(* functions for working with counterexample model labels *) (* functions for working with counterexample model labels *)
val remove_model_labels : labels : Slab.t -> Slab.t val remove_model_labels : labels : Slab.t -> Slab.t
(** Returns a copy of labels without labels "model" and "model_projected". *) (** Returns a copy of labels without labels ["model"] and ["model_projected"]. *)
val append_to_model_trace_label : labels : Slab.t -> val append_to_model_trace_label : labels : Slab.t ->
to_append : string -> to_append : string ->
Slab.t Slab.t
(** The returned set of labels will contain the same set of labels (** The returned set of labels will contain the same set of labels
as argument labels except that a label of the form "model_trace:*" as argument labels except that a label of the form ["model_trace:*"]
will be "model_trace:*to_append."*) will be ["model_trace:*to_append"]. *)
val append_to_model_element_name : labels : Slab.t -> val append_to_model_element_name : labels : Slab.t ->
to_append : string -> to_append : string ->
Slab.t Slab.t
(** The returned set of labels will contain the same set of labels (** The returned set of labels will contain the same set of labels
as argument labels except that a label of the form "model_trace:name@context" as argument labels except that a label of the form ["model_trace:*@*"]
will be "model_trace:nameto_append@context."*) will be ["model_trace:*to_append@*"]. *)
val get_model_element_name : labels : Slab.t -> string val get_model_element_name : labels : Slab.t -> string
(** If labels contain a label of the form "model_trace:name@*", (** If labels contain a label of the form ["model_trace:name@*"],
return name. return ["name"].
Throws Not_found if there is no element name (there is no Throws [Not_found] if there is no label of the form ["model_trace:*"]. *)
label of the form "model_trace:+". *)
val get_model_trace_string : labels : Slab.t -> string val get_model_trace_string : labels : Slab.t -> string
(** If labels contain a label of the form "model_trace:mt_string*", (** If labels contain a label of the form ["model_trace:mt_string"],
return mt_string. return ["mt_string"].
Throws Not_found if there is no mt_string (there is no Throws [Not_found] if there is no label of the form ["model_trace:*"]. *)
label of the form "model_trace:*". *)
val get_model_trace_label : labels : Slab.t -> Slab.elt val get_model_trace_label : labels : Slab.t -> Slab.elt
(** Return label of the for "model_trace:*". (** Return a label of the form ["model_trace:*"].
Throws Not_found if there is no such label.*) Throws [Not_found] if there is no such label. *)
(** {2 Identifiers} *) (** {2 Identifiers} *)
......
...@@ -47,4 +47,4 @@ val has_prefix : string -> string -> bool ...@@ -47,4 +47,4 @@ val has_prefix : string -> string -> bool
val remove_prefix : string -> string -> string val remove_prefix : string -> string -> string
(** [remove_prefix pref s] removes the prefix [pref] from [s]. Raises (** [remove_prefix pref s] removes the prefix [pref] from [s]. Raises
[Not_found if [s] does not start with [pref] *) [Not_found] if [s] does not start with [pref] *)
...@@ -19,14 +19,13 @@ module S = Session ...@@ -19,14 +19,13 @@ module S = Session
let output_dir = ref "" let output_dir = ref ""
let opt_context = ref false let opt_context = ref false
type style = SimpleTree | Jstree | Table type style = SimpleTree | Table
let opt_style = ref Table let opt_style = ref Table
let default_style = "table" let default_style = "table"
let set_opt_style = function let set_opt_style = function
| "simple" -> opt_style := SimpleTree | "simpletree" -> opt_style := SimpleTree
| "jstree" -> opt_style := Jstree
| "table" -> opt_style := Table | "table" -> opt_style := Table
| _ -> | _ ->
eprintf "Unknown html style, ignored@." eprintf "Unknown html style, ignored@."
...@@ -48,7 +47,7 @@ let spec = ...@@ -48,7 +47,7 @@ let spec =
"<path> output directory ('-' for stdout)") :: "<path> output directory ('-' for stdout)") ::
("--context", Arg.Set opt_context, ("--context", Arg.Set opt_context,
" add context around the generated HTML code") :: " add context around the generated HTML code") ::
("--style", Arg.Symbol (["simpletree";"jstree";"table"], set_opt_style), ("--style", Arg.Symbol (["simpletree";"table"], set_opt_style),
" style to use, defaults to '" ^ default_style ^ "'." " style to use, defaults to '" ^ default_style ^ "'."
) :: ) ::
("--add_pp", Arg.Tuple ("--add_pp", Arg.Tuple
...@@ -333,244 +332,12 @@ PUBLIC \"-//W3C//DTD XHTML 1.0 Strict//EN\"\ ...@@ -333,244 +332,12 @@ PUBLIC \"-//W3C//DTD XHTML 1.0 Strict//EN\"\
end end
module Jstree =
struct
let print_verified fmt b =
if b
then fprintf fmt "class='verified'"
else fprintf fmt "class='notverified'"
let print_prover = Whyconf.print_prover
let print_proof_status fmt = function
| Interrupted -> fprintf fmt "<span class='notverified'>Not yet run</span>"
| Unedited -> fprintf fmt "<span class='notverified'>Not yet edited</span>"
| JustEdited | Scheduled | Running -> assert false
| Done pr -> fprintf fmt "<span class='verified'>Done: %a</span>"
Call_provers.print_prover_result pr
| InternalFailure exn ->
fprintf fmt "<span class='notverified'>Failure: %a</span>"
Exn_printer.exn_printer exn
let cmd_regexp = Str.regexp "%\\(.\\)"
let pp_run input cmd output =
let replace s = match Str.matched_group 1 s with
| "%" -> "%"
| "i" -> input
| "o" -> output
| _ -> failwith "unknown format specifier, use %%i, %%o"
in
let cmd = Str.global_substitute cmd_regexp replace cmd in
let c = Sys.command cmd in
if c <> 0 then
eprintf "[Error] '%s' stopped abnormaly : code %i" cmd c
let find_pp edited =
let edited_dst = Filename.concat !output_dir "edited" in
let basename = Filename.basename edited in
try
let suff,(cmd,suff_out) =
List.find (fun (s,_) -> Strings.ends_with basename s) !opt_pp in
let base =
String.sub basename 0 (String.length basename - String.length suff) in
let base_dst = (base^suff_out) in
if !opt_context then
pp_run edited cmd (Filename.concat edited_dst base_dst);
base_dst
with Not_found ->
eprintf "Default %s@." basename;
(* default printer *)
let base = try Filename.chop_extension basename with _ -> basename in
let base_dst = base^".txt" in
if !opt_context then
Sysutil.copy_file edited (Filename.concat edited_dst base_dst);
base_dst
let print_session name fmt session =
let print_proof_attempt fmt pa =
match get_edited_as_abs session pa with
| None ->
fprintf fmt "@[<hov><li rel='prover' ><a href='#'>%a : %a</a></li>@]"
print_prover pa.proof_prover
print_proof_status pa.proof_state
| Some f ->
let output = find_pp f in
fprintf fmt "@[<hov><li rel='prover' ><a href='#' \
onclick=\"showedited('%s'); return false;\">%a : %a</a></li>@]"
output
print_prover pa.proof_prover
print_proof_status pa.proof_state in
let rec print_transf fmt tr =
fprintf fmt
"@[<hov><li rel='transf'><a href='#'>\
<span %a>%s</span></a>@,<ul>%a</ul></li>@]"
print_verified (Opt.inhabited tr.transf_verified)
tr.transf_name
(Pp.print_list Pp.newline print_goal) tr.transf_goals
and print_goal fmt g =
fprintf fmt
"@[<hov><li rel='goal'><a href='#'>\
<span %a>%s</a></a>@,<ul>%a%a</ul></li>@]"
print_verified (Opt.inhabited g.goal_verified)
g.goal_name.Ident.id_string
(Pp.print_iter2 PHprover.iter Pp.newline Pp.nothing
Pp.nothing print_proof_attempt)
g.goal_external_proofs
(Pp.print_iter2 PHstr.iter Pp.newline Pp.nothing
Pp.nothing print_transf)
g.goal_transformations in
let print_theory fmt th =
let name =
try
let (l,t,_) = Theory.restore_path th.theory_name in
String.concat "." (l@[t])
with Not_found -> th.theory_name.Ident.id_string
in
fprintf fmt
"@[<hov><li rel='theory'><a href='#'>\
<span %a>%s</span></a>@,<ul>%a</ul></li>@]"
print_verified (Opt.inhabited th.theory_verified)
name
(Pp.print_list Pp.newline print_goal) th.theory_goals in
let print_file fmt f =
fprintf fmt
"@[<hov><li rel='file'><a href='#'>\
<span %a>%s</span></a>@,<ul>%a</ul></li>@]"
print_verified (Opt.inhabited f.file_verified)
f.file_name
(Pp.print_list Pp.newline print_theory) f.file_theories in
let print_session_aux fmt name =
fprintf fmt "@[<hov><ul><a href='#'>%s</a>@,%a</ul>@]"
name
(Pp.print_iter2 PHstr.iter Pp.newline Pp.nothing Pp.nothing print_file)
session.session_files in