Une MAJ de sécurité est nécessaire sur notre version actuelle. Elle sera effectuée lundi 02/08 entre 12h30 et 13h. L'interruption de service devrait durer quelques minutes (probablement moins de 5 minutes).

Commit 4f150358 authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Remove the "jstree" style from "session".

parent 06285130
......@@ -8,6 +8,7 @@ Tools
o add a command-line option --extra-expl-prefix to specify
additional possible prefixes for VC explanations. (Available for
why3 commands "prove" and "ide".)
* removed "jstree" style from the "session" command
* All split transformations respect the "stop_split" label now.
......@@ -864,8 +864,8 @@ Section~\ref{chap:starting}, respectively with style 1 and 2.
\subsection{Command \texttt{html}}
This command produces a summary of the proof session in HTML syntax.
There are three styles of output: `table', `simpletree', and
`jstree'. The default is `table'.
There are two styles of output: `table' and `simpletree'. The default is
The file generated is named \texttt{why3session.html} and is written
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
form of tree, similar to the tree view in the IDE. It uses only basic
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.
\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
\item[\texttt{-o \textsl{<dir>}}] sets the directory where to output
......@@ -101,7 +101,7 @@ _why3()
return 0
COMPREPLY=( $( compgen -W 'simple jstree' -- "$cur" ) )
COMPREPLY=( $( compgen -W 'simpletree table' -- "$cur" ) )
return 0
......@@ -19,14 +19,13 @@ module S = Session
let output_dir = ref ""
let opt_context = ref false
type style = SimpleTree | Jstree | Table
type style = SimpleTree | Table
let opt_style = ref Table
let default_style = "table"
let set_opt_style = function
| "simple" -> opt_style := SimpleTree
| "jstree" -> opt_style := Jstree
| "simpletree" -> opt_style := SimpleTree
| "table" -> opt_style := Table
| _ ->
eprintf "Unknown html style, ignored@."
......@@ -48,7 +47,7 @@ let spec =
"<path> output directory ('-' for stdout)") ::
("--context", Arg.Set opt_context,
" 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 ^ "'."
) ::
("--add_pp", Arg.Tuple
......@@ -333,244 +332,12 @@ PUBLIC \"-//W3C//DTD XHTML 1.0 Strict//EN\"\
module Jstree =
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"
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
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);
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);
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>@]"
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)
(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)
(Pp.print_iter2 PHprover.iter Pp.newline Pp.nothing
Pp.nothing print_proof_attempt)
(Pp.print_iter2 PHstr.iter Pp.newline Pp.nothing
Pp.nothing print_transf)
g.goal_transformations in
let print_theory fmt th =
let name =
let (l,t,_) = Theory.restore_path th.theory_name in
String.concat "." (l@[t])
with Not_found -> th.theory_name.Ident.id_string
fprintf fmt
"@[<hov><li rel='theory'><a href='#'>\
<span %a>%s</span></a>@,<ul>%a</ul></li>@]"
print_verified (Opt.inhabited th.theory_verified)
(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)
(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>@]"
(Pp.print_iter2 PHstr.iter Pp.newline Pp.nothing Pp.nothing print_file)
session.session_files in
fprintf fmt
"<a href='#' onclick=\"$('#%s_session').jstree('open_all');\">\
expand all\
</a> <a href='#' onclick=\"$('#%s_session').jstree('close_all');\">\
close all\
<div id=\"%s_session\" class=\"session\">\
<script type=\"text/javascript\" class=\"source\">\
$(function () {\
\"types\" : {\
\"types\" : {\
\"file\" : {\
\"icon\" : { \"image\" : \"images/folder16.png\"},\
\"theory\" : {\
\"icon\" : { \"image\" : \"images/folder16.png\"},\
\"goal\" : {\
\"icon\" : { \"image\" : \"images/file16.png\"},\
\"prover\" : {\
\"icon\" : { \"image\" : \"images/wizard16.png\"},\
\"transf\" : {\
\"icon\" : { \"image\" : \"images/configure16.png\"},\
\"plugins\" : [\"themes\",\"html_data\",\"types\"]\
name name name print_session_aux name name
let context : context = "<!DOCTYPE html\
PUBLIC \"-//W3C//DTD XHTML 1.0 Strict//EN\"\
<html xmlns=\"http://www.w3.org/1999/xhtml\">\
<meta http-equiv=\"Content-Type\" content=\"text/html; charset=utf-8\" />\
<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.jstree.js\">\
<script type=\"text/javascript\" src=\"javascript/session.js\">\
<iframe src=\"\" id='edited'>\
<p>Your browser does not support iframes.</p>\
<script type=\"text/javascript\" class=\"source\">\
$(function () {\
let run_files config =
let edited_dst = Filename.concat !output_dir "edited" in
if !opt_context then
if not (Sys.file_exists edited_dst) then Unix.mkdir edited_dst 0o755;
iter_files (run_file context print_session);
if !opt_context then
let data_dir = Whyconf.datadir (Whyconf.get_main config) in
(* copy images *)
let img_dir_src = Filename.concat data_dir "images" in
let img_dir_src = Filename.concat img_dir_src "boomy" in
let img_dir_dst = Filename.concat !output_dir "images" in
if not (Sys.file_exists img_dir_dst) then Unix.mkdir img_dir_dst 0o755;
List.iter (fun img_name ->
let from = Filename.concat img_dir_src img_name in
let to_ = Filename.concat img_dir_dst img_name in
Sysutil.copy_file from to_)
(* copy javascript *)
let js_dir_src = Filename.concat data_dir "javascript" in
let js_dir_dst = Filename.concat !output_dir "javascript" in
Sysutil.copy_dir js_dir_src js_dir_dst
let run () =
let _,config,should_exit1 = read_env_spec () in
let _,_,should_exit1 = read_env_spec () in
if should_exit1 then exit 1;
match !opt_style with
| Table -> iter_files Table.run_one
| SimpleTree -> iter_files Simple.run_one
| Jstree ->
if !output_dir = "-" then begin
Format.eprintf "Option \"-o -\" is not compatible with \"--style jstree\".@.";
exit 1
if !output_dir = "" then begin
let first = ref true in
iter_files (fun fname ->
if not !first then begin
Format.eprintf "Option \"-o -\" is mandatory when \"--style jstree\" is used for several files at once.@.";
exit 1
output_dir := Session.get_project_dir fname;
first := false);
Jstree.run_files config
let cmd =
{ cmd_spec = spec;
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