X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FtermViewer.ml;h=d5950a1c9043cdd3985d3963e2b980f58e7c515c;hb=f60cb106a6a0aafff8f90d0240952516f04663f0;hp=192bbb413b6d203eddfc48c1faa06d3c22670af8;hpb=f7b2e35a7bdadb4fdf0e640428e694703ddf67a5;p=helm.git diff --git a/helm/gTopLevel/termViewer.ml b/helm/gTopLevel/termViewer.ml index 192bbb413..d5950a1c9 100644 --- a/helm/gTopLevel/termViewer.ml +++ b/helm/gTopLevel/termViewer.ml @@ -150,6 +150,7 @@ class proof_viewer obj = initializer self#set_font_size 10 val mutable current_infos = None + val mutable current_mml = None method make_sequent_of_selected_term = match self#get_selection with @@ -189,68 +190,105 @@ 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 + 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" ; 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 - (match acic with - Cic.ACurrentProof (id,idbody,n,conjectures,bo,ty,params) -> - let time1 = Sys.time () in - let content = - Cic2content.acic2content - (ref 0) ~name:(Some "prova") ~ids_to_inner_sorts - ~ids_to_inner_types bo in - let content2pres = - (Content2pres.proof2pres - (function p -> - (Cexpr2pres.cexpr2pres_charcount - (Content_expressions.acic2cexpr ids_to_inner_sorts p)))) in - let pres = content2pres content in - let time2 = Sys.time () in - (* prerr_endline ("Fine trasformazione:" ^ (string_of_float (time2 -. time1))); *) - let xmlpres = - Xml.xml_nempty "math" - ["xmlns","http://www.w3.org/1998/Math/MathML" ; - "xmlns:helm","http://www.cs.unibo.it/helm" ; - "xmlns:xlink","http://www.w3.org/1999/xlink" - ] (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 = Xml2Gdomexmath.document_of_xml Misc.domImpl xmlpres in - let time3 = Sys.time () in - (* ignore (Misc.domImpl#saveDocumentToFile mml "tmp1" ()); *) - (* prerr_endline "(******** FINE DOM **********)"; *) - 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) - | _ -> assert false); + 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"; +(* +ignore (Misc.domImpl#saveDocumentToFile current_mml "/tmp/current_mml_1.xml" ()) ; +ignore (Misc.domImpl#saveDocumentToFile mml "/tmp/mml_1.xml" ()) ; +*) + 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) ; (acic, ids_to_inner_types, ids_to_inner_sorts) end ;;