From: Stefano Zacchiroli Date: Mon, 19 Sep 2005 12:41:02 +0000 (+0000) Subject: - added support for -debug, which avoid catching top level exceptions (still useless... X-Git-Tag: LAST_BEFORE_NEW~103 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1946ca7a51df0acb35d8e2ea001d194f1d2ccb12;p=helm.git - added support for -debug, which avoid catching top level exceptions (still useless until we find a way to let the program die on uncaught exceptions raised by gtk callbacks) - enable whelp syntax on command line - uses Arg for command line parsing --- diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml index 38c161424..bc06a56e5 100644 --- a/helm/matita/matita.ml +++ b/helm/matita/matita.ml @@ -157,23 +157,51 @@ let _ = end (** Debugging }}} *) + (** {2 Command line parsing} *) + +let debug = ref false +let args = ref [] +let add_arg arg = args := arg :: !args + +let arg_spec = + let std_arg_spec = [] in + let debug_arg_spec = + if BuildTimeConf.debug then + [ "-debug", Arg.Set debug, + "Do not catch top-level exception (useful for backtrace inspection)"; ] + else [] + in + std_arg_spec @ debug_arg_spec + +let usage () = + let heading = sprintf "Matita v%s\nUsage: " BuildTimeConf.version in + if Helm_registry.get "matita.mode" = "cicbrowser" then + heading ^ "cicbrowser [ URL | Whelp query ]\nOptions:" + else + heading ^ "matita [ FILE ]" + +let set_matita_mode () = + let matita_mode = + if Filename.basename Sys.argv.(0) = "cicbrowser" + then "cicbrowser" + else "matita" + in + Helm_registry.set "matita.mode" matita_mode + + (** {2 Main} *) + let _ = + set_matita_mode (); + Arg.parse arg_spec add_arg (usage ()); + Helm_registry.set_bool "matita.catch_top_level_exn" (not !debug); at_exit (fun () -> print_endline "\nThanks for using Matita!\n"); Sys.catch_break true; - if Filename.basename Sys.argv.(0) = "cicbrowser" then begin (* cicbrowser *) - Helm_registry.set "matita.mode" "cicbrowser"; + if Helm_registry.get "matita.mode" = "cicbrowser" then (* cicbrowser *) let browser = MatitaMathView.cicBrowser () in - let uri = - try - String.concat " " (List.tl (Array.to_list Sys.argv)) - with Failure _ -> "cic:/" - in + let uri = match !args with [] -> "cic:/" | _ -> String.concat " " !args in browser#loadInput uri - end else begin (* matita *) - Helm_registry.set "matita.mode" "matita"; - (try - gui#loadScript Sys.argv.(1); - with Invalid_argument _ -> ()); + else begin (* matita *) + (try gui#loadScript (List.hd !args) with Failure _ -> ()); gui#main#mainWin#show (); end; try