X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FtermViewer.ml;h=e105d5f0ea32ef9a3df3b50b66a1e6bd80872628;hb=e7e2a523299d807370b292b44e77f46fad1638c9;hp=d5950a1c9043cdd3985d3963e2b980f58e7c515c;hpb=f60cb106a6a0aafff8f90d0240952516f04663f0;p=helm.git diff --git a/helm/gTopLevel/termViewer.ml b/helm/gTopLevel/termViewer.ml index d5950a1c9..e105d5f0e 100644 --- a/helm/gTopLevel/termViewer.ml +++ b/helm/gTopLevel/termViewer.ml @@ -33,7 +33,7 @@ (* *) (******************************************************************************) -let use_stylesheets = ref true;;(* false performs the transformations in OCaml*) +let use_stylesheets = ref false;;(* false performs the transformations in OCaml*) (* List utility functions *) exception Skip;; @@ -65,6 +65,7 @@ class sequent_viewer obj = (* returns the list of selected terms *) (* selections which are not terms are ignored *) method get_selected_terms = + prerr_endline (string_of_int (List.length self#get_selections)) ; let selections = self#get_selections in list_map_fail (function node -> @@ -73,6 +74,7 @@ class sequent_viewer obj = ~namespaceURI:Misc.helmns ~localName:(Gdome.domString "xref"))#to_string in + prerr_endline ("YAHHHHHHHHHH " ^ xpath) ; if xpath = "" then assert false (* "ERROR: No xref found!!!" *) else match current_infos with @@ -111,11 +113,21 @@ class sequent_viewer obj = ApplyStylesheets.mml_of_cic_sequent metasenv sequent in self#load_doc ~dom:sequent_mml ; - current_infos <- +(* +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 ?hadjustment ?vadjustment ?font_size ?log_verbosity = + GtkBase.Container.make_params ~cont:( + OgtkMathViewProps.pack_return + (fun p -> OgtkMathViewProps.set_params (new sequent_viewer (GtkMathViewProps.MathView.create p)) ~font_size ~log_verbosity)) [] +;; + +(* let sequent_viewer ?adjustmenth ?adjustmentv ?font_size ?font_manager ?border_width ?width ?height ?packing ?show () = let w = @@ -138,7 +150,7 @@ let sequent_viewer ?adjustmenth ?adjustmentv ?font_size ?font_manager end; mathview ;; - +*) (** A widget to render proofs **) @@ -147,7 +159,7 @@ class proof_viewer obj = inherit GMathViewAux.single_selection_math_view obj - initializer self#set_font_size 10 +(* initializer self#set_font_size 10 *) val mutable current_infos = None val mutable current_mml = None @@ -160,6 +172,7 @@ class proof_viewer obj = ~namespaceURI:Misc.helmns ~localName:(Gdome.domString "xref"))#to_string in + prerr_endline ("YAEEEEEEEEEEEEEEEEEEE " ^ xpath) ; if xpath = "" then assert false (* "ERROR: No xref found!!!" *) else begin @@ -190,109 +203,89 @@ class proof_viewer obj = end | None -> assert false (* "ERROR: No selection!!!" *) - method load_omdoc_proof uri ~ids_to_inner_sorts cobj = - if !use_stylesheets then - 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 (Content2cic.cobj2obj cobj) - in -prerr_endline "0000000000000000 USO GLI STYLESHEETS" ; + 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 - (match current_mml with - None -> -prerr_endline "0000000000000000 CARICO L'mml PRODOTTO" ; - self#load_doc ~dom:mml ; - current_mml <- Some mml - | Some current_mml -> - self#freeze ; - XmlDiff.update_dom ~from:current_mml mml ; - self#thaw) ; -(* 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 - let pres = Content2pres.content2pres ~ids_to_inner_sorts cobj 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 "(******** INIZIO CONTENT ==> PRES **********)"; - (* - 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 -> - self#load_doc ~dom:mml ; - current_mml <- Some mml - | Some current_mml -> - self#freeze ; -prerr_endline "XML_DIFF: prima passata"; + 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") + ) ; (* -ignore (Misc.domImpl#saveDocumentToFile current_mml "/tmp/current_mml_1.xml" ()) ; -ignore (Misc.domImpl#saveDocumentToFile mml "/tmp/mml_1.xml" ()) ; + self#load_doc ~dom:mml ; + current_mml <- Some mml ; *) - XmlDiff.update_dom ~from:current_mml mml ; -(* -prerr_endline "XML_DIFF: seconda passata"; -ignore (Misc.domImpl#saveDocumentToFile current_mml "/tmp/current_mml_2.xml" ()) ; -ignore (Misc.domImpl#saveDocumentToFile mml "/tmp/mml_2.xml" ()) ; - XmlDiff.update_dom ~from:current_mml mml ; -ignore (Misc.domImpl#saveDocumentToFile current_mml "/tmp/current_mml_3.xml" ()) ; -ignore (Misc.domImpl#saveDocumentToFile mml "/tmp/mml_3.xml" ()) ; -*) -prerr_endline "XML_DIFF: fine passate"; - self#thaw) ; -(* - self#load_doc ~dom: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) - - 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 = - 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) ; + 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); (acic, ids_to_inner_types, ids_to_inner_sorts) end ;; +let proof_viewer ?hadjustment ?vadjustment ?font_size ?log_verbosity = + GtkBase.Container.make_params ~cont:( + OgtkMathViewProps.pack_return + (fun p -> OgtkMathViewProps.set_params (new proof_viewer (GtkMathViewProps.MathView.create p)) ~font_size ~log_verbosity)) [] +;; + +(* let proof_viewer ?adjustmenth ?adjustmentv ?font_size ?font_manager ?border_width ?width ?height ?packing ?show () = let w = @@ -315,6 +308,7 @@ let proof_viewer ?adjustmenth ?adjustmentv ?font_size ?font_manager end; mathview ;; +*) let _ = Cexpr2pres_hashtbl.init Cexpr2pres.cexpr2pres Cexpr2pres.cexpr2pres_charcount