X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FtermViewer.ml;h=da7b6bdca762df7cb351d9385b0a38d00f9afccb;hb=4faf0e37e7019de16dd6862bb34d84f799a2a230;hp=4f57d80ede454fae9f0e2403d37f17de00df6240;hpb=75f24bc40a8b7b1d00e6e88cb9a7b08c6551cac7;p=helm.git diff --git a/helm/gTopLevel/termViewer.ml b/helm/gTopLevel/termViewer.ml index 4f57d80ed..da7b6bdca 100644 --- a/helm/gTopLevel/termViewer.ml +++ b/helm/gTopLevel/termViewer.ml @@ -147,7 +147,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 @@ -190,14 +190,14 @@ 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 + 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 @@ -207,76 +207,61 @@ class proof_viewer obj = current_infos <- Some (ids_to_terms,ids_to_father_ids,ids_to_conjectures,ids_to_hypotheses) ; - else -prerr_endline "(******** INIZIO CONTENT ==> PRES **********)"; - 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 ("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 ;;