Commit 5cae7968 authored by MARCHE Claude's avatar MARCHE Claude

why3session html: output file is now why3session.html

parent ba9543a2
* marks an incompatible change * marks an incompatible change
tools
* file generated by "why3session html f.mlw" is now
"f/why3session.html" and not "f/f.html"
library library
* renamed array.ArraySorted -> array.IntArraySorted * renamed array.ArraySorted -> array.IntArraySorted
array.ArraySorted is now generic, with type and order relation parameters array.ArraySorted is now generic, with type and order relation parameters
......
...@@ -458,10 +458,10 @@ gallery:: ...@@ -458,10 +458,10 @@ gallery::
why3session html $$x; \ why3session html $$x; \
echo "exporting $$f"; \ echo "exporting $$f"; \
mkdir -p $(GALLERYDIR)/$$f; \ mkdir -p $(GALLERYDIR)/$$f; \
cp examples/$$f.mlw examples/$$f/$$f.html $(GALLERYDIR)/$$f/; \ cp examples/$$f.mlw examples/$$f/why3session.html $(GALLERYDIR)/$$f/; \
rm -f $(GALLERYDIR)/$$f/$$f.zip; \ rm -f $(GALLERYDIR)/$$f/$$f.zip; \
cd examples/; \ cd examples/; \
zip -r $(GALLERYDIR)/$$f/$$f.zip $$f.mlw $$f/$$f.html $$f; \ zip -r $(GALLERYDIR)/$$f/$$f.zip $$f.mlw $$f; \
cd ..; \ cd ..; \
done done
...@@ -475,10 +475,10 @@ gallery:: ...@@ -475,10 +475,10 @@ gallery::
mkdir -p $(GALLERYDIR)/$$f; \ mkdir -p $(GALLERYDIR)/$$f; \
if test -f examples/$$f.mlw; then cp examples/$$f.mlw $(GALLERYDIR)/$$f/; fi; \ if test -f examples/$$f.mlw; then cp examples/$$f.mlw $(GALLERYDIR)/$$f/; fi; \
if test -f examples/$$f.why; then cp examples/$$f.why $(GALLERYDIR)/$$f/; fi; \ if test -f examples/$$f.why; then cp examples/$$f.why $(GALLERYDIR)/$$f/; fi; \
cp examples/$$f/$$f.html $(GALLERYDIR)/$$f/; \ cp examples/$$f/why3session.html $(GALLERYDIR)/$$f/; \
rm -f $(GALLERYDIR)/$$f/$$f.zip; \ rm -f $(GALLERYDIR)/$$f/$$f.zip; \
cd examples/; \ cd examples/; \
zip -r $(GALLERYDIR)/$$f/$$f.zip $$f.mlw $$f/$$f.html $$f zip -r $(GALLERYDIR)/$$f/$$f.zip $$f.mlw $$f
######## ########
# XML DTD validation # XML DTD validation
......
...@@ -844,6 +844,10 @@ This command produces a summary of the proof session in HTML syntax. ...@@ -844,6 +844,10 @@ This command produces a summary of the proof session in HTML syntax.
There are three styles of output: `table', `simpletree', and There are three styles of output: `table', `simpletree', and
`jstree'. The default is `table'. `jstree'. The default is `table'.
The file generated is named \texttt{why3session.html} and is written
in the session directory by default (see option \texttt{-o} to
override this default).
\begin{figure}[t] \begin{figure}[t]
%BEGIN LATEX %BEGIN LATEX
\begin{center} \begin{center}
......
...@@ -78,7 +78,7 @@ let run_file (context : context) print_session fname = ...@@ -78,7 +78,7 @@ let run_file (context : context) print_session fname =
let basename = Filename.basename project_dir in let basename = Filename.basename project_dir in
let cout = let cout =
if output_dir = "-" then stdout else if output_dir = "-" then stdout else
open_out (Filename.concat output_dir (basename^".html")) open_out (Filename.concat output_dir ("why3session.html"))
in in
let fmt = formatter_of_out_channel cout in let fmt = formatter_of_out_channel cout in
if !opt_context if !opt_context
......
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