From 4be3764541d8caa00737a686156907e7f2ae720c Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Thu, 22 Jan 2004 15:45:42 +0000 Subject: [PATCH] Now applying ocaml transformations to sequents as well. --- helm/gTopLevel/termViewer.ml | 130 +++++++++++++---------------------- 1 file changed, 48 insertions(+), 82 deletions(-) diff --git a/helm/gTopLevel/termViewer.ml b/helm/gTopLevel/termViewer.ml index e105d5f0e..409c7cd70 100644 --- a/helm/gTopLevel/termViewer.ml +++ b/helm/gTopLevel/termViewer.ml @@ -23,15 +23,14 @@ * http://cs.unibo.it/helm/. *) -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Claudio Sacerdoti Coen *) -(* 29/01/2003 *) -(* *) -(* *) -(******************************************************************************) +(***************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* 29/01/2003 Claudio Sacerdoti Coen *) +(* *) +(* *) +(***************************************************************************) let use_stylesheets = ref false;;(* false performs the transformations in OCaml*) @@ -109,8 +108,12 @@ class sequent_viewer obj = ) selections method load_sequent metasenv sequent = +(**** SIAM QUI ****) let sequent_mml,(ids_to_terms,ids_to_father_ids,ids_to_hypotheses) = - ApplyStylesheets.mml_of_cic_sequent metasenv sequent + if !use_stylesheets then + ApplyStylesheets.mml_of_cic_sequent metasenv sequent + else + ApplyTransformation.mml_of_cic_sequent metasenv sequent in self#load_doc ~dom:sequent_mml ; (* @@ -204,81 +207,44 @@ class proof_viewer obj = | 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 - if !use_stylesheets then - let mml = - ApplyStylesheets.mml_of_cic_object - ~explode_all:true uri acic ids_to_inner_sorts ids_to_inner_types - in - self#load_doc ~dom:mml ; - current_mml <- Some mml ; - current_infos <- - Some - (ids_to_terms,ids_to_father_ids,ids_to_conjectures,ids_to_hypotheses) ; - else - (match acic with - Cic.ACurrentProof (id,idbody,n,conjectures,bo,ty,params) -> - let time1 = Sys.time () in - let content = - Cic2content.annobj2content - ~ids_to_inner_sorts ~ids_to_inner_types acic in - let pres = Content2pres.content2pres ~ids_to_inner_sorts content in - let time2 = Sys.time () in - (* prerr_endline ("Fine trasformazione:" ^ (string_of_float (time2 -. time1))); *) - let xmlpres = Mpresentation.print_mpres pres in - let time25 = Sys.time () in - (* - prerr_endline ("FINE printing to stream:" ^ (string_of_float (time25 -. time2))); - Xml.pp xmlpres (Some "tmp"); - let time3 = Sys.time () in - prerr_endline ("FINE valutazione e printing dello stream:" ^ (string_of_float (time3 -. time25))); - *) - (try - prerr_endline "(******** INIZIO DOM **********)"; - let mml = Xml2Gdome.document_of_xml Misc.domImpl xmlpres in - let time3 = Sys.time () in - (* ignore (Misc.domImpl#saveDocumentToFile mml "tmp1" ()); *) - prerr_endline "(******** FINE DOM **********)"; - (match current_mml with - None -> - let time1 = Sys.time () in - self#load_doc ~dom:mml ; - let time2 = Sys.time () in - prerr_endline ("Loading and displaying the proof took " ^ string_of_float (time2 -. time1) ^ "seconds") ; - current_mml <- Some mml - | Some current_mml' -> - self#freeze ; - let time1 = Sys.time () in - XmlDiff.update_dom ~from:current_mml' mml ; - let time2 = Sys.time () in - prerr_endline ("XMLDIFF took " ^ string_of_float (time2 -. time1) ^ "seconds") ; - self#thaw ; - let time3 = Sys.time () in - prerr_endline ("The refresh of the widget took " ^ string_of_float (time3 -. time2) ^ "seconds") - ) ; -(* - self#load_doc ~dom:mml ; - current_mml <- Some mml ; -*) - prerr_endline ("Fine loading:" ^ (string_of_float (time3 -. time2))) - (* - self#load_uri "tmp"; - let time4 = Sys.time () in - prerr_endline - ("Fine loading:" ^ (string_of_float (time4 -. time3))) - *) - with (GdomeInit.DOMException (_,s)) as e -> - prerr_endline s; raise e) - | _ -> assert false); + 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 = + if !use_stylesheets then + ApplyStylesheets.mml_of_cic_object + ~explode_all:true uri acic ids_to_inner_sorts ids_to_inner_types + else + ApplyTransformation.mml_of_cic_object + ~explode_all:true uri acic ids_to_inner_sorts ids_to_inner_types 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 ; *) + (match current_mml with + None -> + let time1 = Sys.time () in + self#load_doc ~dom:mml ; + let time2 = Sys.time () in + prerr_endline ("Loading and displaying the proof took " ^ string_of_float (time2 -. time1) ^ "seconds") ; + current_mml <- Some mml + | Some current_mml' -> + self#freeze ; + let time1 = Sys.time () in + XmlDiff.update_dom ~from:current_mml' mml ; + let time2 = Sys.time () in + prerr_endline ("XMLDIFF took " ^ string_of_float (time2 -. time1) ^ "seconds") ; + self#thaw ; + let time3 = Sys.time () in + prerr_endline ("The refresh of the widget took " ^ string_of_float (time3 -. time2) ^ "seconds")); (acic, ids_to_inner_types, ids_to_inner_sorts) - end + end ;; + let proof_viewer ?hadjustment ?vadjustment ?font_size ?log_verbosity = GtkBase.Container.make_params ~cont:( OgtkMathViewProps.pack_return -- 2.39.2