why3session_main.ml 2.52 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
MARCHE Claude's avatar
MARCHE Claude committed
4
(*  Copyright 2010-2017   --   INRIA - CNRS - Paris-Sud University  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
5 6 7 8
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
9
(*                                                                  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
10
(********************************************************************)
11 12 13 14 15 16 17

open Format
open Why3
open Why3session_lib

let cmds =
  [|
MARCHE Claude's avatar
MARCHE Claude committed
18
    Why3session_info.cmd;
MARCHE Claude's avatar
MARCHE Claude committed
19
    Why3session_html.cmd;
MARCHE Claude's avatar
MARCHE Claude committed
20
    Why3session_latex.cmd;
MARCHE Claude's avatar
MARCHE Claude committed
21
(*
22
    Why3session_csv.cmd;
23 24 25
    Why3session_copy.cmd_mod;
    Why3session_copy.cmd_copy;
    Why3session_copy.cmd_archive;
26
    Why3session_rm.cmd;
27
    Why3session_output.cmd;
28
    Why3session_run.cmd;
29
*)
30 31
  |]

32
let exec_name = Filename.basename Sys.argv.(0)
33

34
let print_usage fmt () =
35 36
  let maxl = Array.fold_left
    (fun acc e -> max acc (String.length e.cmd_name)) 0 cmds in
37 38
  fprintf fmt "Usage: %s <command> [options] <session directories>@\n@\n\
      Available commands:@.@[<hov>%a@]@\n@."
Andrei Paskevich's avatar
Andrei Paskevich committed
39
    exec_name
40
    (Pp.print_iter1 Array.iter Pp.newline
41
       (fun fmt e -> fprintf fmt "  %s   @[<hov>%s@]"
42
         (Strings.pad_right ' ' e.cmd_name maxl) e.cmd_desc)) cmds;
43 44 45 46
  let usage = Arg.usage_string
    (Arg.align Why3session_lib.common_options) "Common options:" in
  fprintf fmt "%s@\nSpecific command options: %s <command> --help@."
    usage exec_name
47 48

let () =
49 50 51 52
  if Array.length Sys.argv < 2 then begin
    print_usage err_formatter ();
    exit 1
  end;
53
  let cmd_name = Sys.argv.(1) in
54
  begin
Andrei Paskevich's avatar
Andrei Paskevich committed
55
    match cmd_name with
56 57
      | "-h" | "-help" | "--help" ->
        print_usage std_formatter (); exit 0
58 59
      | _ -> ()
  end;
60 61 62 63 64 65 66
  let module M = struct exception Found of cmd end in
  let cmd =
    try
      Array.iter (fun e ->
        if e.cmd_name = cmd_name
        then raise (M.Found e)) cmds;
      eprintf "command %s unknown@." cmd_name;
67 68
      print_usage err_formatter ();
      exit 1
69 70 71
    with M.Found cmd -> cmd
  in
  incr Arg.current;
72
  let cmd_usage = sprintf "Usage: %s %s [options]" exec_name cmd_name in
73
  Arg.parse (Arg.align cmd.cmd_spec) anon_fun cmd_usage;
MARCHE Claude's avatar
MARCHE Claude committed
74 75 76 77 78
  try
    cmd.cmd_run ()
  with e when not (Debug.test_flag Debug.stack_trace) ->
    eprintf "@.%a@." Exn_printer.exn_printer e;
    exit 1