X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FtermViewer.ml;h=841c61edfb184dd2811a065af11401b1dbbc9c7a;hb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1;hp=9a9c9c9b884ae941d0d976dcf20cb49735b39f1f;hpb=d05dd15ef48652976f82de6ecff3931cfa2055e9;p=helm.git diff --git a/helm/gTopLevel/termViewer.ml b/helm/gTopLevel/termViewer.ml index 9a9c9c9b8..841c61edf 100644 --- a/helm/gTopLevel/termViewer.ml +++ b/helm/gTopLevel/termViewer.ml @@ -23,15 +23,32 @@ * http://cs.unibo.it/helm/. *) -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Claudio Sacerdoti Coen *) -(* 29/01/2003 *) -(* *) -(* *) -(******************************************************************************) +(***************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* 29/01/2003 Claudio Sacerdoti Coen *) +(* *) +(* *) +(***************************************************************************) + +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.id, Cic.term) Hashtbl.t * + (Cic.id, Cic.id option) Hashtbl.t * + (string, Cic.hypothesis) Hashtbl.t) + +type mml_of_cic_object = + explode_all:bool -> + UriManager.uri -> + Cic.annobj -> + (string, string) Hashtbl.t -> + (string, Cic2acic.anntypes) Hashtbl.t -> Gdome.document (* List utility functions *) exception Skip;; @@ -53,7 +70,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 @@ -63,6 +80,7 @@ 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 -> @@ -105,15 +123,32 @@ 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 + 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) +(* +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.Container.make_params ~cont:( + OgtkMathViewProps.pack_return + (fun p -> + OgtkMathViewProps.set_params + (new sequent_viewer ~mml_of_cic_sequent + (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 = @@ -136,18 +171,19 @@ 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 - initializer self#set_font_size 10 +(* 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 @@ -188,24 +224,57 @@ 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 + 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 + mml_of_cic_object + ~explode_all:true uri acic ids_to_inner_sorts ids_to_inner_types in - self#load_doc ~dom:mml ; - current_infos <- + 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 + (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 + 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 ;; + +let proof_viewer ~(mml_of_cic_object: mml_of_cic_object) + ?hadjustment ?vadjustment ?font_size ?log_verbosity += + GtkBase.Container.make_params ~cont:( + OgtkMathViewProps.pack_return + (fun p -> + OgtkMathViewProps.set_params + (new proof_viewer ~mml_of_cic_object + (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 = @@ -228,3 +297,5 @@ let proof_viewer ?adjustmenth ?adjustmentv ?font_size ?font_manager end; mathview ;; +*) +