X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic%2FcicParser.ml;h=a289683772312aa3114040a53261b48fe186ce7d;hb=b9af9f1c0de6a1735b492f5c793a87a8fce218cc;hp=619e947f21d4af37334eff3052fec896cc5592fd;hpb=1b1ae2b73035d4a09792ee53c51e7c6dd5bbd41c;p=helm.git

diff --git a/helm/ocaml/cic/cicParser.ml b/helm/ocaml/cic/cicParser.ml
index 619e947f2..a28968377 100644
--- a/helm/ocaml/cic/cicParser.ml
+++ b/helm/ocaml/cic/cicParser.ml
@@ -64,6 +64,7 @@ type stack_entry =
       (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 *)
@@ -99,6 +100,7 @@ let string_of_stack ctxt =
           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)
@@ -615,6 +617,7 @@ let end_element ctxt 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
@@ -627,6 +630,16 @@ let end_element ctxt tag =
         (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
@@ -658,6 +671,13 @@ let end_element ctxt tag =
 
 (** {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;
@@ -671,7 +691,11 @@ let parse uri 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