Commit 01009c56 authored by Andrei Paskevich's avatar Andrei Paskevich

remove the obsolete "report" parameter from Env.*

parent 24ce29c0
......@@ -71,15 +71,11 @@ type read_channel =
?debug:bool -> ?parse_only:bool -> ?type_only:bool ->
env -> string -> in_channel -> theory Mnm.t
type error_report = Format.formatter -> exn -> unit
let read_channel_table = Hashtbl.create 17 (* parser name -> read_channel *)
let error_report_table = Hashtbl.create 17 (* parser name -> error_report *)
let suffixes_table = Hashtbl.create 17 (* suffix -> parser name *)
let register_format name suffixes rc er =
let register_format name suffixes rc =
Hashtbl.add read_channel_table name rc;
Hashtbl.add error_report_table name er;
List.iter (fun s -> Hashtbl.add suffixes_table ("." ^ s) name) suffixes
exception UnknownFormat of string (* parser name *)
......@@ -108,11 +104,6 @@ let read_channel ?name ?debug ?parse_only ?type_only env file ic =
let rc = find_parser read_channel_table n in
rc ?debug ?parse_only ?type_only env file ic
let report ?name file fmt e =
let n = parser_for_file ?name file in
let er = find_parser error_report_table n in
er fmt e
let list_formats () =
let h = Hashtbl.create 17 in
let add s p =
......
......@@ -41,10 +41,8 @@ type read_channel =
?debug:bool -> ?parse_only:bool -> ?type_only:bool ->
env -> string -> in_channel -> theory Mnm.t
type error_report = Format.formatter -> exn -> unit
val register_format :
string -> string list -> read_channel -> error_report -> unit
string -> string list -> read_channel -> unit
(** [register_format name extensions f1 f2] registers a new format
under name [name], for files with extensions in list [extensions];
[f1] is the function to perform parsing;
......@@ -52,8 +50,6 @@ val register_format :
val read_channel : ?name:string -> read_channel
val report : ?name:string -> string -> error_report
exception UnknownFormat of string (* format name *)
val list_formats : unit -> (string * string list) list
......
......@@ -407,28 +407,21 @@ let do_input env drv = function
| "-" -> "stdin", stdin
| f -> f, open_in f
in
let report = Env.report ?name:!opt_parser fname in
try
let m =
Env.read_channel ?name:!opt_parser ~debug:!opt_debug
~parse_only:!opt_parse_only ~type_only:!opt_type_only
env fname cin
in
close_in cin;
if !opt_type_only then
()
else if Queue.is_empty tlist then
let glist = Queue.create () in
let add_th t th mi = Ident.Mid.add th.th_name (t,th) mi in
let do_th _ (t,th) = do_theory env drv fname t th trans glist in
Ident.Mid.iter do_th (Mnm.fold add_th m Ident.Mid.empty)
else
Queue.iter (do_local_theory env drv fname m) tlist
with
| Loc.Located (loc, e) ->
eprintf "@[%a%a@]@." Loc.report_position loc report e; exit 1
| e ->
eprintf "@[%a@]@." report e; exit 1
let m =
Env.read_channel ?name:!opt_parser ~debug:!opt_debug
~parse_only:!opt_parse_only ~type_only:!opt_type_only
env fname cin
in
close_in cin;
if !opt_type_only then
()
else if Queue.is_empty tlist then
let glist = Queue.create () in
let add_th t th mi = Ident.Mid.add th.th_name (t,th) mi in
let do_th _ (t,th) = do_theory env drv fname t th trans glist in
Ident.Mid.iter do_th (Mnm.fold add_th m Ident.Mid.empty)
else
Queue.iter (do_local_theory env drv fname m) tlist
let () =
try
......
......@@ -46,7 +46,6 @@
| Parsing.Parse_error -> Format.fprintf fmt "syntax error"
| _ -> raise exn
)
%}
/* Tokens */
......
......@@ -988,19 +988,7 @@ let retrieve lp env sl =
(** register Why parser *)
let error_report fmt = function
| Lexer.Error e ->
fprintf fmt "lexical error: %a" Lexer.report e;
| Parsing.Parse_error ->
fprintf fmt "syntax error"
| Denv.Error e ->
Denv.report fmt e
| Error e ->
report fmt e
| e ->
raise e
let () = Env.register_format "why" ["why"] read_channel error_report
let () = Env.register_format "why" ["why"] read_channel
(*
Local Variables:
......
......@@ -23,23 +23,15 @@ open Format
open Why
open Pgm_env
let rec report fmt = function
| Lexer.Error e ->
fprintf fmt "lexical error: %a" Lexer.report e;
| Pgm_lexer.Error e ->
fprintf fmt "lexical error: %a" Pgm_lexer.report e;
| Loc.Located (loc, e) ->
fprintf fmt "%a%a" Loc.report_position loc report e
| Parsing.Parse_error ->
fprintf fmt "syntax error"
| Typing.Error e ->
Typing.report fmt e
| Pgm_typing.Error e ->
Pgm_typing.report fmt e
| Denv.Error e ->
Denv.report fmt e
| e ->
raise e
let () = Exn_printer.register
(fun fmt exn -> match exn with
| Pgm_lexer.Error e ->
fprintf fmt "lexical error: %a" Pgm_lexer.report e;
| Parsing.Parse_error ->
fprintf fmt "syntax error"
| Pgm_typing.Error e ->
Pgm_typing.report fmt e
| _ -> raise exn)
let parse_only _env file c =
let lb = Lexing.from_channel c in
......@@ -77,8 +69,7 @@ let read_channel
end
end
let () =
Env.register_format "whyml" ["mlw"] read_channel report
let () = Env.register_format "whyml" ["mlw"] read_channel
(*
Local Variables:
......
......@@ -35,22 +35,18 @@ module Process : sig
val printFile : Format.formatter -> string -> string -> string -> unit
val read_channel : Env.read_channel
val report : Env.error_report
end = struct
let fromInclude = function | Include x -> x | _ -> assert false
let isInclude = function | Include _ -> true | _ -> false
(** report errors *)
let report fmt = function
let () = Exn_printer.register (fun fmt exn -> match exn with
| TptpLexer.LexicalError (s, pos) ->
Format.fprintf fmt "lexical error: %a@." TptpLexer.report (s, pos)
| TptpParser.Error ->
Format.fprintf fmt "syntax error.@." (*TODO : find how to report pos*)
| e ->
Format.fprintf fmt "exception uncaught : %s@." (Printexc.to_string e);
raise e
| e -> raise e)
(** for a given file, returns the list of declarations
for this file and all the files it includes, recursively *)
......@@ -146,8 +142,7 @@ open Init *)
(** register as a .p/.ax file parser *)
let () =
Env.register_format "tptp" ["p"] Process.read_channel Process.report
let () = Env.register_format "tptp" ["p"] Process.read_channel
(*
......
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