Commit 036366a4 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

bug fix: wrong extension when reading files. Also added some printf in the Why...

bug fix: wrong extension when reading files. Also added some printf in the Why core, I known that Andrei does not like it but I guess he won't notice. Who reads the commit messages anyway? Also added comments to env.mli, the end user will thank me a lot for that! What else? Ah yes, make bench does not work at all, a reference
to Graph is missing. I heard that Andrei played with the use or not use of ocamlgraph library. Seems to be wrong. But anyway, if Andrei does not feel like doing make bench before committing, why should I do it myself? That's all folks
parent 96109f04
...@@ -89,7 +89,9 @@ let parser_for_file ?name file = match name with ...@@ -89,7 +89,9 @@ let parser_for_file ?name file = match name with
in in
Hashtbl.find suffixes_table ext Hashtbl.find suffixes_table ext
with Invalid_argument _ | Not_found -> with Invalid_argument _ | Not_found ->
"why" Format.eprintf "Cannot determine format for file=%S@." file;
Format.eprintf "Using 'why' as default@.";
"why"
end end
| Some n -> | Some n ->
n n
...@@ -103,6 +105,12 @@ let read_channel ?name env file ic = ...@@ -103,6 +105,12 @@ let read_channel ?name env file ic =
let rc = find_parser read_channel_table n in let rc = find_parser read_channel_table n in
rc env file ic rc env file ic
let read_file ?name env file =
let cin = open_in file in
let m = read_channel ?name env file cin in
close_in cin;
m
let list_formats () = let list_formats () =
let h = Hashtbl.create 17 in let h = Hashtbl.create 17 in
let add s p = let add s p =
......
...@@ -45,6 +45,16 @@ val register_format : string -> string list -> read_channel -> unit ...@@ -45,6 +45,16 @@ val register_format : string -> string list -> read_channel -> unit
[f1] is the function to perform parsing *) [f1] is the function to perform parsing *)
val read_channel : ?name:string -> read_channel val read_channel : ?name:string -> read_channel
(** [read_channel ?name env f c] returns the map of theories
in channel [c]. When given, [name] enforces the format, otherwise
the format is chosen according to [f]'s extension.
Beware that it cannot be checked that [c] corresponds
to the contents of [f] *)
val read_file : ?name:string -> env -> string -> theory Mnm.t
(** [read_file ?name env f] returns the map of theories
in file [f]. When given, [name] enforces the format, otherwise
the format is chosen according to [f]'s extension. *)
exception UnknownFormat of string (* format name *) exception UnknownFormat of string (* format name *)
......
...@@ -395,16 +395,9 @@ module Helpers = struct ...@@ -395,16 +395,9 @@ module Helpers = struct
mth mth
let input_theories file : Theory.theory Theory.Mnm.t =
let cin = open_in file in
let m = Env.read_channel gconfig.env fname cin in
close_in cin;
m
let add_file f = let add_file f =
try try
let theories = input_theories f in let theories = Env.read_file gconfig.env f in
(* TODO: if syntax error, do something clean *)
let _dbfile = Db.add_file f in let _dbfile = Db.add_file f in
let parent = goals_model#append () in let parent = goals_model#append () in
let mfile = { file_name = f; let mfile = { file_name = f;
......
...@@ -97,9 +97,7 @@ let gconfig = ...@@ -97,9 +97,7 @@ let gconfig =
let theories : Theory.theory Theory.Mnm.t = let theories : Theory.theory Theory.Mnm.t =
try try
let cin = open_in fname in let m = Env.read_file gconfig.env fname in
let m = Env.read_channel gconfig.env fname cin in
close_in cin;
eprintf "Parsing/Typing Ok@."; eprintf "Parsing/Typing Ok@.";
m m
with e -> with e ->
......
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