Commit 33f61172 authored by Andrei Paskevich's avatar Andrei Paskevich

put back Loc.report_position and remove Loc.string

Loc.report_position adds a colon and a newline at the end.
parent efb6e95f
......@@ -102,6 +102,9 @@ let opt_command = ref None
let opt_task = ref None
let opt_bisect = ref false
let opt_print_libdir = ref false
let opt_print_datadir = ref false
let opt_print_theory = ref false
let opt_print_namespace = ref false
let opt_list_transforms = ref false
......@@ -199,17 +202,28 @@ let option_list = Arg.align [
" Set all debug flags (except parse_only and type_only)";
"--debug", Arg.String add_opt_debug,
"<flag> Set a debug flag";
"--print-libdir", Arg.Set opt_print_libdir,
" Print location of binary components (plugins, etc)";
"--print-datadir", Arg.Set opt_print_datadir,
" Print location of non-binary data (theories, modules, etc)";
"--version", Arg.Set opt_version,
" Print version information" ]
let () =
try
let () = try
Arg.parse option_list add_opt_file usage_msg;
if !opt_version then begin
printf "%s@." version_msg;
exit 0
end;
if !opt_print_libdir then begin
printf "%s@." Config.libdir;
exit 0
end;
if !opt_print_datadir then begin
printf "%s@." Config.datadir;
exit 0
end;
(** Debug flag *)
if !opt_debug_all then begin
......@@ -322,7 +336,6 @@ let () =
exit 1
end;
opt_loadpath := List.rev_append !opt_loadpath (Whyconf.loadpath main);
if !opt_timelimit = None then opt_timelimit := Some (Whyconf.timelimit main);
if !opt_memlimit = None then opt_memlimit := Some (Whyconf.memlimit main);
......@@ -341,6 +354,7 @@ let () =
add_meta task meta [MAstr s]
in
opt_task := List.fold_left add_meta !opt_task !opt_metas
with e when not (Debug.test_flag Debug.stack_trace) ->
eprintf "%a@." Exn_printer.exn_printer e;
exit 1
......@@ -500,7 +514,7 @@ let do_input env drv = function
close_in cin;
if !opt_type_only then
()
else
else
match !opt_coq_realization with
| Some f ->
Queue.iter (do_coq_realize_theory env drv f fname m) tlist
......
......@@ -76,22 +76,13 @@ let compare (_,l1,b1,e1) (_,l2,b2,e2) =
Pervasives.compare e1 e2
let gen_report_position fmt (f,l,b,e) =
fprintf fmt "File \"%s\", " f;
fprintf fmt "line %d, characters %d-%d" l b e
let string =
let buf = Buffer.create 1024 in
fun loc ->
let fmt = Format.formatter_of_buffer buf in
Format.fprintf fmt "%a@?" gen_report_position loc;
let s = Buffer.contents buf in
Buffer.reset buf;
s
fprintf fmt "File \"%s\", line %d, characters %d-%d" f l b e
let report_position fmt = fprintf fmt "%a:@\n" gen_report_position
let () = Exn_printer.register
(fun fmt exn -> match exn with
| Located (loc,e) ->
fprintf fmt "%a:@\n%a@\n" gen_report_position loc
Exn_printer.exn_printer e
fprintf fmt "%a%a" report_position loc Exn_printer.exn_printer e
| _ -> raise exn)
......@@ -36,8 +36,6 @@ val join : position -> position -> position
exception Located of position * exn
val string : position -> string
val dummy_position : position
val user_position : string -> int -> int -> int -> position
......@@ -48,4 +46,5 @@ val compare : position -> position -> int
val gen_report_position : formatter -> position -> unit
val report_position : formatter -> position -> unit
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