Commit 38e42c8d authored by Andrei Paskevich's avatar Andrei Paskevich

several fixes

parent 6c5c3c9c
......@@ -1147,7 +1147,7 @@ let why3tac ?(timelimit=timelimit) s gl =
| Whyconf.ProverNotFound (_, fp) ->
let pl =
Mprover.fold (fun prover p l -> if not p.interactive
then (Pp.string_of_wnl Whyconf.print_prover prover) :: l
then ("\"" ^ Whyconf.prover_parseable_format prover ^ "\"") :: l
else l)
(get_provers config) [] in
let msg = pr_str "No such prover `"
......@@ -1158,7 +1158,8 @@ let why3tac ?(timelimit=timelimit) s gl =
errorlabstrm "Whyconf.ProverNotFound" msg
| Whyconf.ProverAmbiguity (_, fp,provers) ->
let pl = Mprover.keys provers in
let pl = List.map (Pp.string_of_wnl Whyconf.print_prover) pl in
let pl = List.map (fun prover ->
"\"" ^ Whyconf.prover_parseable_format prover ^ "\"") pl in
let msg = pr_str "More than one prover corresponding to `" ++
pr_fp fp ++ pr_str "'." ++
pr_spc () ++ pr_str "Corresponding provers are:" ++ pr_fnl () ++
......@@ -1168,7 +1169,6 @@ let why3tac ?(timelimit=timelimit) s gl =
let msg = pr_str "Syntax error prover identification '" ++
pr_str s ++ pr_str "' : name[,version[,alternative]|,,alternative]" in
errorlabstrm "Whyconf.ParseFilterProver" msg
| e ->
Printexc.print_backtrace stderr; flush stderr;
Format.eprintf "@[exception: %a@]@." Exn_printer.exn_printer e;
......
......@@ -35,7 +35,9 @@ let magicnumber = 14
exception WrongMagicNumber
let why3_regexp_of_string s = (** define a regexp in why3 *)
if s.[0] = '^' then Str.regexp s else Str.regexp ("^"^Str.quote s^"$")
if s = "" then Str.regexp "^$" else
if s.[0] = '^' then Str.regexp s else
Str.regexp ("^" ^ Str.quote s ^ "$")
(* lib and shared dirs *)
......
......@@ -130,5 +130,6 @@ module Args = struct
(fun (s,f,_,_) -> if not (is_info_flag s) then set_flag f)
(list_flags ());
Queue.iter (fun flag -> let flag = lookup_flag flag in set_flag flag)
opt_list_flags
opt_list_flags;
if test_flag stack_trace then Printexc.record_backtrace true
end
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment