]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic/cicParser.ml
New experimental commit: metavariables representation is changed again,
[helm.git] / helm / ocaml / cic / cicParser.ml
index bf75243ec4300773479f1fe6b2c4dbbb356fee9e..241a5c1752caafe0af217271dd654545e31f4136 100644 (file)
@@ -46,7 +46,7 @@ class warner =
   end
 ;;
 
-exception EmptyUri;;
+exception EmptyUri of string;;
 
 (* given an uri u it returns the list of tokens of the base uri of u *)
 (* e.g.: token_of_uri "cic:/a/b/c/d.xml" returns ["a" ; "b" ; "c"]   *)
@@ -54,7 +54,8 @@ let tokens_of_uri uri =
  let uri' = UriManager.string_of_uri uri in
  let rec chop_list =
   function
-     [] -> raise EmptyUri
+     [] -> raise (EmptyUri uri')
+   | [fn] -> []
    | he::[fn] -> [he]
    | he::tl -> he::(chop_list tl)
  in
@@ -64,18 +65,14 @@ let tokens_of_uri uri =
 ;;
 
 (* given the filename of an xml file of a cic object it returns its internal *)
-(* representation. process_annotations is true if the annotations do really  *)
-(* matter                                                                    *)
-let term_of_xml filename uri process_annotations =
+(* representation.                                                           *)
+let annobj_of_xml filename uri =
  let module Y = Pxp_yacc in
   try 
     let d =
       (* sets the current base uri to resolve relative URIs *)
       CicParser3.current_sp := tokens_of_uri uri ;
       CicParser3.current_uri := uri ;
-      CicParser3.process_annotations := process_annotations ;
-      CicParser3.ids_to_targets :=
-       if process_annotations then Some (Hashtbl.create 500) else None ;
       let config = {Y.default_config with Y.warner = new warner} in
       Y.parse_document_entity config
 (*PXP       (Y.ExtID (Pxp_types.System filename,
@@ -83,13 +80,14 @@ let term_of_xml filename uri process_annotations =
 *)     (PxpUriResolver.from_file filename)
        CicParser3.domspec
     in
-     let ids_to_targets = !CicParser3.ids_to_targets in
-      let res = (CicParser2.get_term d#root, ids_to_targets) in
-       CicParser3.ids_to_targets := None ; (* let's help the GC *)
-       res
+     CicParser2.get_term d#root
   with
    e ->
      print_endline ("Filename: " ^ filename ^ "\nException: ") ;
      print_endline (Pxp_types.string_of_exn e) ;
      raise e
 ;;
+
+let obj_of_xml filename uri =
+ Deannotate.deannotate_obj (annobj_of_xml filename uri)
+;;