why3session_html.ml 13.3 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-2011                                               *)
(*    François Bobot                                                      *)
(*    Jean-Christophe Filliâtre                                           *)
(*    Claude Marché                                                       *)
(*    Andrei Paskevich                                                    *)
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)

20
open Format
21
open Why3
22
open Why3session_lib
23 24

let output_dir = ref ""
25
let opt_context = ref false
26

27
type style = Simple | Jstree
28

29
let opt_style = ref Simple
30 31 32 33 34

let set_opt_style = function
  | "simple" -> opt_style := Simple
  | "jstree" -> opt_style := Jstree
  | _ -> assert false
35

36 37 38 39 40 41 42 43 44
let opt_pp = ref []

let set_opt_pp_in,set_opt_pp_cmd,set_opt_pp_out =
  let suf = ref "" in
  let cmd = ref "" in
  (fun s -> suf := s),
  (fun s -> cmd := s),
  (fun s -> opt_pp := (!suf,(!cmd,s))::!opt_pp)

45
let spec =
46 47
  ("-o",
   Arg.Set_string output_dir,
48 49 50
   " The directory to output the files ('-' for stdout)") ::
  ("--context", Arg.Set opt_context,
   " Add context around the generated code in order to allow direct \
51
    visualisation (header, css, ...). It also add in the directory \
52 53 54 55 56
    all the needed external file. It can't be set with stdout output") ::
  ("--style", Arg.Symbol (["simple";"jstree"], set_opt_style),
   " Set the style to use. 'simple' use only 'ul' and 'il' tag. 'jstree' use \
    the 'jstree' plugin of the javascript library 'jquery'.") ::
  ("--add_pp", Arg.Tuple
57 58 59 60 61 62
    [Arg.String set_opt_pp_in;
     Arg.String set_opt_pp_cmd;
     Arg.String set_opt_pp_out],
  "<suffix> <cmd> <out_suffix> \
Add for the given prefix the given pretty-printer, \
the new file as the given out_suffix. cmd must contain '%i' which will be \
63 64 65
replace by the input file and '%o' which will be replaced by the output file.") ::
  ("--coqdoc",
   Arg.Unit (fun ()->
66
    opt_pp := (".v",("coqdoc --no-index --html -o %o %i",".html"))::!opt_pp),
67 68
  " same as '--add_pp .v \"coqdoc --no-index --html -o %o %i\" .html'") ::
  simple_spec
69

70
(*
71
let version_msg = sprintf
72 73 74
  "Why3 html session output, version %s (build date: %s)"
  Config.version Config.builddate

75
let usage_str = sprintf
76 77 78 79 80 81 82 83 84
  "Usage: %s [options] [<file.why>|<project directory>] ... "
  (Filename.basename Sys.argv.(0))

let set_file f = Queue.push f files

let () = Arg.parse spec set_file usage_str

let () =
  if !opt_version then begin
85
    printf "%s@." version_msg;
86 87
    exit 0
  end
88
*)
89

90 91 92 93
(* let () = *)
(*   List.iter (fun (in_,(cmd,out)) -> *)
(*     printf "in : %s, cmd : %s, out : %s@." in_ cmd out) !opt_pp *)

94
(*
95 96 97
let () =
  Debug.Opt.set_flags_selected ();
  if  Debug.Opt.option_list () then exit 0
98
*)
99

100
(*
101
let output_dir =
102
  match !output_dir with
103
   | "" ->
104
      printf "Error: output_dir must be set@.";
105 106 107 108 109 110
      exit 1
    | "-" when !opt_context ->
      printf
        "Error: context and stdout output can't be set at the same time@.";
      exit 1
    | _ -> !output_dir
111

112 113
let edited_dst = Filename.concat output_dir "edited"

François Bobot's avatar
François Bobot committed
114
let whyconf = Whyconf.read_config !opt_config
115
  *)
François Bobot's avatar
François Bobot committed
116 117

open Session
118 119
open Util

120
type context =
121
    (string ->
François Bobot's avatar
François Bobot committed
122
     (formatter -> notask session -> unit) -> notask session
123 124
     -> unit, formatter, unit) format

125 126 127 128 129 130 131 132 133 134 135
let run_file (context : context) print_session fname =
  let project_dir = Session.get_project_dir fname in
  let session = Session.read_session project_dir in
  let output_dir =
    if !output_dir = "" then project_dir else !output_dir
  in
  let basename = Filename.basename project_dir in
  let cout =
    if output_dir = "-" then stdout else
      open_out (Filename.concat output_dir (basename^".html"))
  in
136 137 138 139 140 141 142 143 144 145 146
  let fmt = formatter_of_out_channel cout in
  if !opt_context
  then fprintf fmt context basename (print_session basename) session
  else print_session basename fmt session;
  pp_print_flush fmt ();
  if output_dir <> "-" then close_out cout


module Simple =
struct

147
  let print_prover = Whyconf.print_prover
148 149

  let print_proof_status fmt = function
François Bobot's avatar
François Bobot committed
150
    | Undone _ -> fprintf fmt "Undone"
151 152 153
    | Done pr -> fprintf fmt "Done : %a" Call_provers.print_prover_result pr
    | InternalFailure exn ->
      fprintf fmt "Failure : %a"Exn_printer.exn_printer exn
154

155 156
  let print_proof_attempt fmt pa =
    fprintf fmt "<li>%a : %a</li>"
François Bobot's avatar
François Bobot committed
157
      print_prover pa.proof_prover
158 159 160 161 162
      print_proof_status pa.proof_state

  let rec print_transf fmt tr =
    fprintf fmt "<li>%s : <ul>%a</ul></li>"
      tr.transf_name
François Bobot's avatar
François Bobot committed
163
      (Pp.print_list Pp.newline print_goal) tr.transf_goals
164 165 166

  and print_goal fmt g =
    fprintf fmt "<li>%s : <ul>%a%a</ul></li>"
François Bobot's avatar
François Bobot committed
167 168
      g.goal_name.Ident.id_string
      (Pp.print_iter2 PHprover.iter Pp.newline Pp.nothing
169
         Pp.nothing print_proof_attempt)
François Bobot's avatar
François Bobot committed
170 171
      g.goal_external_proofs
      (Pp.print_iter2 PHstr.iter Pp.newline Pp.nothing
172
         Pp.nothing print_transf)
François Bobot's avatar
François Bobot committed
173
      g.goal_transformations
174 175 176

  let print_theory fmt th =
    fprintf fmt "<li>%s : <ul>%a</ul></li>"
François Bobot's avatar
François Bobot committed
177 178
      th.theory_name.Ident.id_string
      (Pp.print_list Pp.newline print_goal) th.theory_goals
179 180 181 182

  let print_file fmt f =
    fprintf fmt "<li>%s : <ul>%a</ul></li>"
      f.file_name
François Bobot's avatar
François Bobot committed
183
      (Pp.print_list Pp.newline print_theory) f.file_theories
184 185 186

  let print_session _name fmt s =
    fprintf fmt "<ul>%a</ul>"
François Bobot's avatar
François Bobot committed
187 188
      (Pp.print_iter2 PHstr.iter Pp.newline Pp.nothing Pp.nothing
         print_file) s.session_files
189 190 191


  let context : context = "<!DOCTYPE html
192 193 194 195
PUBLIC \"-//W3C//DTD XHTML 1.0 Strict//EN\"
\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd\">
<html xmlns=\"http://www.w3.org/1999/xhtml\">
<head>
196
<title>Why3 session of %s</title>
197 198 199 200 201 202
</head>
<body>
%a
</body>
</html>
"
203

204
  let run_one = run_file context print_session
205

206
end
207

208 209
(*

210 211 212
module Jstree =
struct

213 214 215 216 217
  let print_verified fmt b =
    if b
    then fprintf fmt "class='verified'"
    else fprintf fmt "class='notverified'"

218
  let print_prover = Whyconf.print_prover
219 220

  let print_proof_status fmt = function
François Bobot's avatar
François Bobot committed
221
    | Undone _ -> fprintf fmt "<span class='notverified'>Undone</span>"
222 223
    | Done pr -> fprintf fmt "<span class='verified'>Done : %a</span>"
      Call_provers.print_prover_result pr
224
    | InternalFailure exn ->
225 226
      fprintf fmt "<span class='notverified'>Failure : %a</span>"
        Exn_printer.exn_printer exn
227

228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261
  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 basename = Filename.basename edited in
    try
      let suff,(cmd,suff_out) =
        List.find (fun (s,_) -> 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

262
  let print_proof_attempt fmt pa =
François Bobot's avatar
François Bobot committed
263
    match pa.proof_edited_as with
264 265
      | None ->
        fprintf fmt "@[<hov><li rel='prover' ><a href='#'>%a : %a</a></li>@]"
François Bobot's avatar
François Bobot committed
266
          print_prover pa.proof_prover
267 268 269 270 271 272
          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
François Bobot's avatar
François Bobot committed
273
          print_prover pa.proof_prover
274
          print_proof_status pa.proof_state
275 276 277

  let rec print_transf fmt tr =
    fprintf fmt
278 279 280
      "@[<hov><li rel='transf'><a href='#'>\
<span %a>%s</span></a>@,<ul>%a</ul></li>@]"
      print_verified tr.transf_verified
281
      tr.transf_name
François Bobot's avatar
François Bobot committed
282
      (Pp.print_list Pp.newline print_goal) tr.transf_goals
283 284 285

  and print_goal fmt g =
    fprintf fmt
286 287 288
      "@[<hov><li rel='goal'><a href='#'>\
<span %a>%s</a></a>@,<ul>%a%a</ul></li>@]"
      print_verified g.goal_verified
François Bobot's avatar
François Bobot committed
289 290
      g.goal_name.Ident.id_string
      (Pp.print_iter2 PHprover.iter Pp.newline Pp.nothing
291
         Pp.nothing print_proof_attempt)
François Bobot's avatar
François Bobot committed
292 293
      g.goal_external_proofs
      (Pp.print_iter2 PHstr.iter Pp.newline Pp.nothing
294
         Pp.nothing print_transf)
François Bobot's avatar
François Bobot committed
295
      g.goal_transformations
296 297 298

  let print_theory fmt th =
    fprintf fmt
299 300 301
      "@[<hov><li rel='theory'><a href='#'>\
<span %a>%s</span></a>@,<ul>%a</ul></li>@]"
      print_verified th.theory_verified
François Bobot's avatar
François Bobot committed
302 303
      th.theory_name.Ident.id_string
      (Pp.print_list Pp.newline print_goal) th.theory_goals
304 305

  let print_file fmt f =
306 307 308 309
    fprintf fmt
      "@[<hov><li rel='file'><a href='#'>\
<span %a>%s</span></a>@,<ul>%a</ul></li>@]"
      print_verified f.file_verified
310
      f.file_name
François Bobot's avatar
François Bobot committed
311
      (Pp.print_list Pp.newline print_theory) f.file_theories
312 313 314 315

  let print_session_aux name fmt s =
    fprintf fmt "@[<hov><ul><a href='#'>%s</a>@,%a</ul>@]"
      name
François Bobot's avatar
François Bobot committed
316 317
      (Pp.print_iter2 PHstr.iter Pp.newline Pp.nothing Pp.nothing print_file)
      s.session_files
318 319 320 321 322 323 324 325 326 327 328 329 330 331


  let print_session name fmt s =
    fprintf fmt
      "<a href='#' onclick=\"$('#%s_session').jstree('open_all');\">
expand all
</a> <a href='#' onclick=\"$('#%s_session').jstree('close_all');\">
close all
</a>
<div id=\"%s_session\" class=\"session\">
%a
</div>
<script type=\"text/javascript\" class=\"source\">
$(function () {
332
  $(\"#%s_session\").jstree({
333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366
      \"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\"]
        });
});
</script>
"
  name name name (print_session_aux name) s name


  let context : context = "<!DOCTYPE html
PUBLIC \"-//W3C//DTD XHTML 1.0 Strict//EN\"
\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd\">
<html xmlns=\"http://www.w3.org/1999/xhtml\">
<head>
    <meta http-equiv=\"Content-Type\" content=\"text/html; charset=utf-8\" />
    <title>Why3 session of %s</title>
367 368
    <link rel=\"stylesheet\" type=\"text/css\"
     href=\"javascript/session.css\" />
369
    <script type=\"text/javascript\" src=\"javascript/jquery.js\"></script>
370 371 372 373
    <script type=\"text/javascript\" src=\"javascript/jquery.jstree.js\">\
</script>
    <script type=\"text/javascript\" src=\"javascript/session.js\">\
</script>
374 375 376
</head>
<body>
%a
377 378 379 380 381 382 383 384
<iframe src=\"\"  id='edited'>
<p>Your browser does not support iframes.</p>
</iframe>
<script type=\"text/javascript\" class=\"source\">
$(function () {
  $('#edited').hide()
})
</script>
385 386 387 388 389
</body>
</html>
"

  let run_files () =
390 391
    if !opt_context then
      if not (Sys.file_exists edited_dst) then Unix.mkdir edited_dst 0o755;
392 393
    Queue.iter (run_file context print_session) files;
    if !opt_context then
François Bobot's avatar
François Bobot committed
394
      let data_dir = Whyconf.datadir (Whyconf.get_main whyconf) in
395 396 397 398 399 400 401 402 403 404 405 406 407 408 409
      (** copy images *)
      let img_dir_src = Filename.concat data_dir "images" 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_)
        ["folder16.png";"file16.png";"wizard16.png";"configure16.png"];
      (** 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

end
410
*)
411 412


413
let run_one fname =
414
  match !opt_style with
415 416 417 418 419
    | Simple -> Simple.run_one fname
    | Jstree ->
      eprintf "style jstree not yet available@.";
      exit 1
      (* Jstree.run_files () *)
420 421 422 423 424 425 426 427 428 429 430 431 432 433 434

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;
  }
435 436 437 438 439 440 441


(*
Local Variables:
compile-command: "unset LANG; make -C ../.. bin/why3session.byte"
End:
*)