Une nouvelle version du portail de gestion des comptes externes sera mise en production lundi 09 août. Elle permettra d'allonger la validité d'un compte externe jusqu'à 3 ans. Pour plus de détails sur cette version consulter : https://doc-si.inria.fr/x/FCeS

why3session.ml 2.3 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3 4 5 6 7 8 9 10
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
(*  Copyright 2010-2012   --   INRIA - CNRS - Paris-Sud University  *)
(*                                                                  *)
(*  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.                           *)
(*                                                                  *)
(********************************************************************)
11 12 13 14 15 16 17

open Format
open Why3
open Why3session_lib

let cmds =
  [|
MARCHE Claude's avatar
MARCHE Claude committed
18 19 20
    Why3session_info.cmd;
    Why3session_latex.cmd;
    Why3session_html.cmd;
21 22 23
    Why3session_copy.cmd_mod;
    Why3session_copy.cmd_copy;
    Why3session_copy.cmd_archive;
24
    Why3session_rm.cmd;
25 26
  |]

27
let exec_name = Sys.argv.(0)
28 29

let print_usage () =
30 31
  let maxl = Array.fold_left
    (fun acc e -> max acc (String.length e.cmd_name)) 0 cmds in
MARCHE Claude's avatar
MARCHE Claude committed
32
  eprintf "%s <command> [options] <session directories>@\n@\navailable commands:@.@[<hov>%a@]@\n@."
Andrei Paskevich's avatar
Andrei Paskevich committed
33
    exec_name
34 35
    (Pp.print_iter1 Array.iter Pp.newline
       (fun fmt e -> fprintf fmt "%s   @[<hov>%s@]"
36
         (Strings.pad_right ' ' e.cmd_name maxl) e.cmd_desc)) cmds;
37
  Arg.usage (Arg.align Why3session_lib.common_options) "common options:";
38
  eprintf "@\nspecific command options: %s <command> -help@." exec_name;
39 40 41 42 43
  exit 1

let () =
  if Array.length Sys.argv < 2 then print_usage ();
  let cmd_name = Sys.argv.(1) in
44
  begin
Andrei Paskevich's avatar
Andrei Paskevich committed
45
    match cmd_name with
46 47 48 49
      | "-h" | "--help" -> print_usage ()
      | "-v" | "--version" -> print_version (); exit 0
      | _ -> ()
  end;
50 51 52 53 54 55 56 57 58 59 60
  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;
      print_usage ()
    with M.Found cmd -> cmd
  in
  incr Arg.current;
61
  let cmd_usage = sprintf "%s %s [options]:" Sys.argv.(0) cmd_name in
62
  Arg.parse (Arg.align cmd.cmd_spec) anon_fun cmd_usage;
MARCHE Claude's avatar
MARCHE Claude committed
63 64 65 66 67
  try
    cmd.cmd_run ()
  with e when not (Debug.test_flag Debug.stack_trace) ->
    eprintf "@.%a@." Exn_printer.exn_printer e;
    exit 1