Skip to content

GitLab

Attention une mise à jour du serveur va être effectuée le vendredi 16 avril entre 12h et 12h30. Cette mise à jour va générer une interruption du service de quelques minutes.

Commit 8a8bcf05 authored by MARCHE Claude's avatar MARCHE Claude
Browse files
Options

moved src/ide/session_html into src/why3session/why3session_html

parent 8bfbf655
Hide whitespace changes
Inline Side-by-side
Showing with 60 additions and 108 deletions
Makefile.in
View file @ 8a8bcf05
......@@ -669,7 +669,7 @@ install_local: bin/why3replayer
###############
SESSION_FILES = why3session_lib why3session_copy why3session_info \
why3session_output why3session_rm why3session
why3session_latex why3session_html why3session_rm why3session
SESSIONMODULES = $(addprefix src/why3session/, $(SESSION_FILES))
......@@ -715,38 +715,6 @@ install_no_local::
install_local: bin/why3session
###############
# Stats
###############
STATS_FILES = stats
STATSMODULES = $(addprefix src/ide/, $(STATS_FILES))
STATSDEP = $(addsuffix .dep, $(STATSMODULES))
STATSCMO = $(addsuffix .cmo, $(STATSMODULES))
STATSCMX = $(addsuffix .cmx, $(STATSMODULES))
$(STATSDEP): DEPFLAGS += -I src/ide
$(STATSCMO) $(STATSCMX): INCLUDES += -I src/ide
# build targets
byte: bin/why3stats.byte
opt: bin/why3stats.opt
bin/why3stats.opt: src/why3.cmxa $(PGMCMX) $(STATSCMX)
$(if $(QUIET), @echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
$(STRIP) $@
bin/why3stats.byte: src/why3.cma $(PGMCMO) $(STATSCMO)
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
bin/why3stats: bin/why3stats.@OCAMLBEST@
ln -sf why3stats.@OCAMLBEST@ $@
# depend and clean targets
ifneq "$(MAKECMDGOALS)" "clean"
......@@ -763,38 +731,6 @@ install_no_local::
install_local: bin/why3stats
###############
# Html
###############
HTML_FILES = html_session
HTMLMODULES = $(addprefix src/ide/, $(HTML_FILES))
HTMLDEP = $(addsuffix .dep, $(HTMLMODULES))
HTMLCMO = $(addsuffix .cmo, $(HTMLMODULES))
HTMLCMX = $(addsuffix .cmx, $(HTMLMODULES))
$(HTMLDEP): DEPFLAGS += -I src/ide
$(HTMLCMO) $(HTMLCMX): INCLUDES += -I src/ide
# build targets
byte: bin/why3html.byte
opt: bin/why3html.opt
bin/why3html.opt: src/why3.cmxa $(PGMCMX) $(HTMLCMX)
$(if $(QUIET), @echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
$(STRIP) $@
bin/why3html.byte: src/why3.cma $(PGMCMO) $(HTMLCMO)
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
bin/why3html: bin/why3html.@OCAMLBEST@
ln -sf why3html.@OCAMLBEST@ $@
# depend and clean targets
ifneq "$(MAKECMDGOALS)" "clean"
......
ROADMAP
View file @ 8a8bcf05
......@@ -144,14 +144,16 @@ https://gforge.inria.fr/tracker/index.php?func=detail&aid=13736&group_id=2990
* (CLAUDE) why3session
- passe sur la documentation ecrite par Francois reecrite par Guillaume
- DONE option -latex deplacée de why3replayer vers why3session
- option -html deplacée de why3replayer vers why3session
- reprendre une partie de src/ide/stats.ml, et virer executable why3stats
- DONE "why3replayer -latex" remplacé par "why3session latex"
- "why3html" remplacé par "why3session html"
- "why3stats" (src/ide/stats.ml) remplacé par "why3session stats"
ou par "why3session info" avec des options
* (JCF) renommer why3html en why3doc
* (JCF) ameliorer why3doc
- rajouter la production des liens
- mettre la bibliotheque standard de Why3 en HTML, sur le site Web
- entree makefile pour produire la bibliotheque standard de Why3 en HTML
(pour mettre sur le site Web)
* provers
......
src/why3session/why3session.ml
View file @ 8a8bcf05
......@@ -28,18 +28,21 @@ let cmds =
Why3session_copy.cmd_archive;
Why3session_info.cmd;
Why3session_rm.cmd;
Why3session_output.cmd;
Why3session_latex.cmd;
Why3session_html.cmd;
|]
let usage = "why3session cmd [opts]"
let exec_name = Sys.argv.(0)
let print_usage () =
let maxl = Array.fold_left
(fun acc e -> max acc (String.length e.cmd_name)) 0 cmds in
eprintf "%s@.@.command:@.@[<hov>%a@]@."
usage (Pp.print_iter1 Array.iter Pp.newline
(fun fmt e -> fprintf fmt "%s @[<hov>%s@]"
(Util.padd_string ' ' e.cmd_name maxl) e.cmd_desc)) cmds;
eprintf "%s <command> [options]@.@.available commands:@.@[<hov>%a@]@\n@."
exec_name
(Pp.print_iter1 Array.iter Pp.newline
(fun fmt e -> fprintf fmt "%s @[<hov>%s@]"
(Util.padd_string ' ' e.cmd_name maxl) e.cmd_desc)) cmds;
eprintf "detailed command options: %s <command> -help@." exec_name;
exit 1
......@@ -61,6 +64,6 @@ let () =
with M.Found cmd -> cmd
in
incr Arg.current;
let cmd_usage = sprintf "why3session %s [opts]:" cmd_name in
let cmd_usage = sprintf "%s %s [options]:" Sys.argv.(0) cmd_name in
Arg.parse (Arg.align cmd.cmd_spec) anon_fun cmd_usage;
cmd.cmd_run ()
src/ide/html_session.ml → src/why3session/why3session_html.ml
View file @ 8a8bcf05
......@@ -87,6 +87,7 @@ replace by the input file and '%o' which will be replaced by the output file.";
]
(*
let version_msg = sprintf
"Why3 html session output, version %s (build date: %s)"
Config.version Config.builddate
......@@ -104,24 +105,29 @@ let () =
printf "%s@." version_msg;
exit 0
end
*)
(* let () = *)
(* List.iter (fun (in_,(cmd,out)) -> *)
(* printf "in : %s, cmd : %s, out : %s@." in_ cmd out) !opt_pp *)
(*
let () =
Debug.Opt.set_flags_selected ();
if Debug.Opt.option_list () then exit 0
*)
let output_dir =
match !output_dir with
| "" -> printf
"Error: output_dir must be set@.";
(*
| "" ->
printf "Error: output_dir must be set@.";
exit 1
| "-" when !opt_context ->
printf
"Error: context and stdout output can't be set at the same time@.";
exit 1
*)
| _ -> !output_dir
let edited_dst = Filename.concat output_dir "edited"
......@@ -417,7 +423,26 @@ $(function () {
end
(*
let () =
match !opt_style with
| Simple -> Simple.run_files ()
| Jstree -> Jstree.run_files ()
*)
let run_one _fname = ()
open Why3session_lib
let run () =
let should_exit1 = read_simple_spec () in
if should_exit1 then exit 1;
iter_files run_one
let cmd =
{ cmd_spec = spec;
cmd_desc = "output session in HTML format.";
cmd_name = "html";
cmd_run = run;
}
src/why3session/why3session_output.ml → src/why3session/why3session_latex.ml
View file @ 8a8bcf05
......@@ -25,25 +25,23 @@ open Format
module S = Session
let opt_latex = ref ""
let opt_latex2 = ref ""
let opt_style = ref 1
let opt_output_dir = ref ""
let opt_longtable = ref false
let spec =
("-latex",
Arg.Set_string opt_latex,
" [Dir_output] produce latex statistics") ::
("-latex2",
Arg.Set_string opt_latex2,
" [Dir_output] produce latex statistics") ::
("-style <n>",
Arg.Set_int opt_style,
" sets output style (1 or 2, default 1)") ::
("-dir <path>",
Arg.Set_string opt_output_dir,
" where to produce LaTeX files (default: session dir)") ::
("-longtable",
Arg.Set opt_longtable,
" produce latex statistics using longtable package") ::
" produce tables using longtable package instead of tabular") ::
simple_spec
(* Statistics in LaTeX*)
let rec transf_depth tr =
......@@ -292,24 +290,12 @@ let print_latex_statistics n table dir session =
let table () = if !opt_longtable then "longtable" else "tabular"
let run_one fname =
if !opt_longtable && !opt_latex == "" && !opt_latex2 == "" then
begin
eprintf
"[Error] I can't use option longtable without latex ou latex2@.";
exit 1
end;
let project_dir = Session.get_project_dir fname in
let session = Session.read_session project_dir in
if !opt_latex <> "" then
print_latex_statistics 1 (table ()) !opt_latex session
else
if !opt_latex2 <> "" then
print_latex_statistics 2 (table()) !opt_latex2 session
else
begin
eprintf "Specify output format e.g. --latex@.";
exit 1
end
let dir = if !opt_output_dir = "" then project_dir else
!opt_output_dir
in
print_latex_statistics !opt_style (table ()) dir session
let run () =
let should_exit1 = read_simple_spec () in
......@@ -319,7 +305,7 @@ let run () =
let cmd =
{ cmd_spec = spec;
cmd_desc = "output session in some formats.";
cmd_name = "output";
cmd_desc = "output session in LaTeX format.";
cmd_name = "latex";
cmd_run = run;
}
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