Natural_deduction : ITM_main.items_of

let items_of_file (path : string) : t_itm list =
        match Sys.file_exists path with
        |false -> raise (Parse_error ("Cannot read from " ^ path ^ ": No such file"))
        |true -> 
        let ic : in_channel = open_in path in
        let lexbuf : Lexing.lexbuf = Lexing.from_channel ic in
        try ITM_parser.main ITM_lexer.token lexbuf with
        |PRF_main.Parse_error e -> 
                raise (Parse_error (String.concat "" [
                        "Parsing failed on line ";string_of_int (ITM_lexer.line_of_lexbuf lexbuf);" of "; path;"; ";
                        "Cannot parse the following proof:\n";e;
                ]))
        |FML_main.Parse_error e ->
                raise (Parse_error (String.concat "" [
                        "Parsing failed on line ";string_of_int (ITM_lexer.line_of_lexbuf lexbuf);" of ";path;"; ";
                        "Cannot parse the following formula: \'";e;"\'";
                ]))

        |_ -> raise (Parse_error (String.concat " " ["Parsing failed on line";string_of_int (ITM_lexer.line_of_lexbuf lexbuf);"of"; path]))