X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FtermViewer.ml;h=0f2019ad507b3a3c2d6c9a850ca537001ce3eefd;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=da7b6bdca762df7cb351d9385b0a38d00f9afccb;hpb=090e2272788bdbaa480e3e677d5c303f2a9d8d0d;p=helm.git diff --git a/helm/gTopLevel/termViewer.ml b/helm/gTopLevel/termViewer.ml index da7b6bdca..0f2019ad5 100644 --- a/helm/gTopLevel/termViewer.ml +++ b/helm/gTopLevel/termViewer.ml @@ -23,18 +23,40 @@ * 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*) +let debug = false +let debug_print s = if debug then prerr_endline s +type mml_of_cic_sequent = + Cic.metasenv -> + int * Cic.context * Cic.term -> + Gdome.document * + (Cic.annconjecture * + ((Cic.id, Cic.term) Hashtbl.t * + (Cic.id, Cic.id option) Hashtbl.t * + (string, Cic.hypothesis) Hashtbl.t * + (Cic.id, string) Hashtbl.t)) + + +type mml_of_cic_object = + 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;; @@ -55,7 +77,7 @@ let list_map_fail f = (** A widget to render sequents **) -class sequent_viewer obj = +class sequent_viewer ~(mml_of_cic_sequent:mml_of_cic_sequent) obj = object(self) inherit GMathViewAux.multi_selection_math_view obj @@ -65,12 +87,13 @@ class sequent_viewer obj = (* returns the list of selected terms *) (* selections which are not terms are ignored *) method get_selected_terms = + debug_print (string_of_int (List.length self#get_selections)) ; let selections = self#get_selections in list_map_fail (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!!!" *) @@ -92,7 +115,7 @@ class sequent_viewer obj = (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!!!" *) @@ -107,15 +130,30 @@ class sequent_viewer obj = ) selections method load_sequent metasenv sequent = - let sequent_mml,(ids_to_terms,ids_to_father_ids,ids_to_hypotheses) = - ApplyStylesheets.mml_of_cic_sequent metasenv sequent +(**** SIAM QUI ****) + let sequent_mml,(_,(ids_to_terms,ids_to_father_ids,ids_to_hypotheses,ids_to_inner_sorts)) = + mml_of_cic_sequent metasenv sequent in - self#load_doc ~dom:sequent_mml ; - current_infos <- - Some (ids_to_terms,ids_to_father_ids,ids_to_hypotheses) + self#load_root ~root:sequent_mml#get_documentElement ; +ignore (Misc.domImpl#saveDocumentToFile ~name:"/tmp/pippo" ~doc:sequent_mml ()); + current_infos <- + Some (ids_to_terms,ids_to_father_ids,ids_to_hypotheses) end ;; +let sequent_viewer ~(mml_of_cic_sequent: mml_of_cic_sequent) + ?hadjustment ?vadjustment ?font_size ?log_verbosity += + GtkBase.Widget.size_params ~cont:( + OgtkMathViewProps.pack_return + (fun p -> + OgtkMathViewProps.set_params + (new sequent_viewer ~mml_of_cic_sequent + (GtkMathViewProps.MathView_GMetaDOM.create p)) + ~font_size ~log_verbosity)) [] +;; + +(* let sequent_viewer ?adjustmenth ?adjustmentv ?font_size ?font_manager ?border_width ?width ?height ?packing ?show () = let w = @@ -138,11 +176,11 @@ let sequent_viewer ?adjustmenth ?adjustmentv ?font_size ?font_manager end; mathview ;; - +*) (** A widget to render proofs **) -class proof_viewer obj = +class proof_viewer ~(mml_of_cic_object:mml_of_cic_object) obj = object(self) inherit GMathViewAux.single_selection_math_view obj @@ -157,7 +195,7 @@ class proof_viewer obj = 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!!!" *) @@ -176,7 +214,7 @@ class proof_viewer obj = 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!!!" *) @@ -190,82 +228,56 @@ class proof_viewer obj = 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 - 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); + 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 ; *) + ignore(Misc.domImpl#saveDocumentToFile ~name:"/tmp/prova" ~doc:mml ()); + (match current_mml with + None -> + let time1 = Sys.time () in + self#load_root ~root:mml#get_documentElement ; + let time2 = Sys.time () in + debug_print ("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 + debug_print ("XMLDIFF took " ^ + string_of_float (time2 -. time1) ^ "seconds") ; + self#thaw ; + let time3 = Sys.time () in + debug_print ("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 ~(mml_of_cic_object: mml_of_cic_object) + ?hadjustment ?vadjustment ?font_size ?log_verbosity += + GtkBase.Widget.size_params ~cont:( + OgtkMathViewProps.pack_return + (fun p -> + OgtkMathViewProps.set_params + (new proof_viewer ~mml_of_cic_object + (GtkMathViewProps.MathView_GMetaDOM.create p)) + ~font_size ~log_verbosity)) [] +;; + +(* let proof_viewer ?adjustmenth ?adjustmentv ?font_size ?font_manager ?border_width ?width ?height ?packing ?show () = let w = @@ -288,7 +300,5 @@ let proof_viewer ?adjustmenth ?adjustmentv ?font_size ?font_manager end; mathview ;; +*) -let _ = - Cexpr2pres_hashtbl.init Cexpr2pres.cexpr2pres Cexpr2pres.cexpr2pres_charcount -;;