type mml_of_cic_sequent =
Cic.metasenv ->
int * Cic.context * Cic.term ->
- Gdome.document *
+ Gdome.document *
+ (Cic.annconjecture *
((Cic.id, Cic.term) Hashtbl.t *
(Cic.id, Cic.id option) Hashtbl.t *
- (string, Cic.hypothesis) Hashtbl.t)
+ (string, Cic.hypothesis) Hashtbl.t *
+ (Cic.id, string) Hashtbl.t))
+
type mml_of_cic_object =
- explode_all:bool ->
- UriManager.uri ->
- Cic.annobj ->
- (string, string) Hashtbl.t ->
- (string, Cic2acic.anntypes) Hashtbl.t -> Gdome.document
-
+ Cic.obj ->
+ Gdome.document *
+ (Cic.annobj *
+ ((Cic.id, Cic.term) Hashtbl.t *
+ (Cic.id, Cic.id option) Hashtbl.t *
+ (Cic.id, Cic.conjecture) Hashtbl.t *
+ (Cic.id, Cic.hypothesis) Hashtbl.t *
+ (Cic.id, string) Hashtbl.t *
+ (Cic.id, Cic2acic.anntypes) Hashtbl.t))
+
(* List utility functions *)
exception Skip;;
(function node ->
let xpath =
((node : Gdome.element)#getAttributeNS
- ~namespaceURI:Misc.helmns
+ ~namespaceURI:Misc.helm_ns
~localName:(Gdome.domString "xref"))#to_string
in
if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
(function node ->
let xpath =
((node : Gdome.element)#getAttributeNS
- ~namespaceURI:Misc.helmns
+ ~namespaceURI:Misc.helm_ns
~localName:(Gdome.domString "xref"))#to_string
in
if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
method load_sequent metasenv sequent =
(**** SIAM QUI ****)
- let sequent_mml,(ids_to_terms,ids_to_father_ids,ids_to_hypotheses) =
+ let sequent_mml,(_,(ids_to_terms,ids_to_father_ids,ids_to_hypotheses,ids_to_inner_sorts)) =
mml_of_cic_sequent metasenv sequent
in
-prerr_endline "PRIMA DI SALVARE IL FILE" ;
self#load_root ~root:sequent_mml#get_documentElement ;
-prerr_endline "SALVO IL FILE IN TEMP" ;
-Misc.domImpl#saveDocumentToFile ~name:"/tmp/pippo" ~doc:sequent_mml () ;
+ignore (Misc.domImpl#saveDocumentToFile ~name:"/tmp/pippo" ~doc:sequent_mml ());
current_infos <-
Some (ids_to_terms,ids_to_father_ids,ids_to_hypotheses)
end
Some node ->
let xpath =
((node : Gdome.element)#getAttributeNS
- ~namespaceURI:Misc.helmns
+ ~namespaceURI:Misc.helm_ns
~localName:(Gdome.domString "xref"))#to_string
in
if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
Some node ->
let xpath =
((node : Gdome.element)#getAttributeNS
- ~namespaceURI:Misc.helmns
+ ~namespaceURI:Misc.helm_ns
~localName:(Gdome.domString "xref"))#to_string
in
if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
end
| None -> assert false (* "ERROR: No selection!!!" *)
- method load_proof uri currentproof =
- let
- (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
- ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
- = Cic2acic.acic_object_of_cic_object currentproof
- in
- let mml =
- mml_of_cic_object
- ~explode_all:true uri acic ids_to_inner_sorts ids_to_inner_types
+ method load_proof currentproof =
+ let mml,
+ (acic,
+ (ids_to_terms,ids_to_father_ids,ids_to_conjectures,
+ ids_to_hypotheses,ids_to_inner_sorts,ids_to_inner_types)) =
+ mml_of_cic_object currentproof
in
current_infos <-
Some
(ids_to_terms,ids_to_father_ids,ids_to_conjectures,ids_to_hypotheses);
(* self#load_doc ~dom:mml ;
current_mml <- Some mml ; *)
-Misc.domImpl#saveDocumentToFile ~name:"/tmp/prova" ~doc:mml () ;
+ ignore(Misc.domImpl#saveDocumentToFile ~name:"/tmp/prova" ~doc:mml ());
(match current_mml with
None ->
let time1 = Sys.time () in