(string * Cic.annterm) list (* id, name, inductive, arity, constructors *)
| Meta_subst of Cic.annterm option
| Obj_class of Cic.object_class
+ | Obj_flavour of Cic.object_flavour
| Obj_field of string (* field name *)
| Obj_generated
| Tag of string * (string * string) list (* tag name, attributes *)
sprintf "Inductive_type %s (id=%s)" name id
| Meta_subst _ -> "Meta_subst"
| Obj_class _ -> "Obj_class"
+ | Obj_flavour _ -> "Obj_flavour"
| Obj_field name -> "Obj_field " ^ name
| Obj_generated -> "Obj_generated"
| Tag (tag, _) -> "Tag " ^ tag)
| "attributes" ->
let rec aux acc = function (* retrieve object attributes *)
| Obj_class c :: tl -> aux (`Class c :: acc) tl
+ | Obj_flavour f :: tl -> aux (`Flavour f :: acc) tl
| Obj_generated :: tl -> aux (`Generated :: acc) tl
| tl -> acc, tl
in
(match pop_tag_attrs ctxt with
| ["name", name] -> Obj_field name
| _ -> attribute_error ())
+ | "flavour" ->
+ push ctxt
+ (match pop_tag_attrs ctxt with
+ | [ "value", "definition"] -> Obj_flavour `Definition
+ | [ "value", "fact"] -> Obj_flavour `Fact
+ | [ "value", "lemma"] -> Obj_flavour `Lemma
+ | [ "value", "remark"] -> Obj_flavour `Remark
+ | [ "value", "theorem"] -> Obj_flavour `Theorem
+ | [ "value", "variant"] -> Obj_flavour `Variant
+ | _ -> attribute_error ())
| "class" ->
let class_modifiers = pop_class_modifiers ctxt in
push ctxt
(** {2 Parser internals} *)
+let has_gz_suffix fname =
+ try
+ let idx = String.rindex fname '.' in
+ let suffix = String.sub fname idx (String.length fname - idx) in
+ suffix = ".gz"
+ with Not_found -> false
+
let parse uri filename =
let ctxt = new_parser_context uri in
ctxt.filename <- filename;
ctxt.xml_parser <- Some xml_parser;
try
(try
- P.parse xml_parser (`Gzip_file filename);
+ let xml_source =
+ if has_gz_suffix filename then `Gzip_file filename
+ else `File filename
+ in
+ P.parse xml_parser xml_source
with exn ->
ctxt.xml_parser <- None;
(* ZACK: the above "<- None" is vital for garbage collection. Without it