+(* note, this function works cause moo files are transitively closed *)
+let process_notation_of_file file =
+ let ic = open_in file in
+ let istream = Stream.of_channel ic in
+ let notation_ids = ref [] in
+ try
+ while true do
+ match GrafiteParser.parse_statement istream with
+ | GA.Executable (_, GA.Command (_, notation)) ->
+ let stm, ids = CicNotation.process_notation notation in
+ notation_ids := ids @ !notation_ids
+ | _ -> ()
+ done; []
+ with
+ | End_of_file -> close_in ic; !notation_ids
+ | CicNotationParser.Parse_error _ as exn ->
+ prerr_endline ("Unable to parse: " ^ file);
+ prerr_endline (MatitaExcPp.to_string exn);
+ raise exn
+