X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fbinaries%2Ftranscript%2Ftop.ml;h=b66146b2ea9e375ea9b729b3eee5c9c9d7658ff6;hb=3b4ec24b0bf7b1cd23cdc632fa3fcbb9dbbda139;hp=5ef75dab70f4be01abf2d47740260e830ef2c448;hpb=298868e07163c21863d542136733d24bfbec2482;p=helm.git diff --git a/helm/software/components/binaries/transcript/top.ml b/helm/software/components/binaries/transcript/top.ml index 5ef75dab7..b66146b2e 100644 --- a/helm/software/components/binaries/transcript/top.ml +++ b/helm/software/components/binaries/transcript/top.ml @@ -24,12 +24,25 @@ *) let main = - let cwd = ref Filename.current_dir_name in - let help = "Usage: transcript [ -C ] [ | ]*" in + let help = "Usage: transcript [ -glmpx | -C ] [ | ]*" in let help_C = " set working directory to " in - let set_cwd dir = cwd := dir in - let process_package package = Engine.produce (Engine.make !cwd package) in - Engine.init (); + let help_g = " check for non existing objects" in + let help_l = " verbose lexing" in + let help_m = " minimal output generation" in + let help_p = " verbose parsing" in + let help_x = " verbose character escaping" in + let set_cwd dir = Options.cwd := dir; Engine.init () in + let process_file file = + if Sys.file_exists file || Sys.file_exists (file ^ Engine.suffix) then + begin Engine.produce (Engine.make file); Options.sources := [] end + else + Options.sources := file :: !Options.sources + in Arg.parse [ - ("-C", Arg.String set_cwd, help_C) - ] process_package help + ("-C", Arg.String set_cwd, help_C); + ("-g", Arg.Set Options.getter, help_g); + ("-l", Arg.Set Options.verbose_lexer, help_l); + ("-m", Arg.Clear Options.comments, help_m); + ("-p", Arg.Set Options.verbose_parser, help_p); + ("-x", Arg.Set Options.verbose_escape, help_x); + ] process_file help