From 5c796440126e33778e4b3f763ce37b677b378cc5 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 29 Apr 2004 16:15:25 +0000 Subject: [PATCH] - moved applyTransformation initialization code to the relevant library - decoupled termViewer from ChosenTransformer --- helm/gTopLevel/gTopLevel.ml | 18 +++++++--- helm/gTopLevel/termViewer.ml | 64 +++++++++++++++++++++++++---------- helm/gTopLevel/termViewer.mli | 20 +++++++++++ 3 files changed, 79 insertions(+), 23 deletions(-) diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 0d0b7c4d1..e70946564 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -172,6 +172,7 @@ let check_window uris = lazy (let mmlwidget = TermViewer.sequent_viewer + ~mml_of_cic_sequent:ChosenTransformer.mml_of_cic_sequent ~packing:scrolled_window#add ~width:400 ~height:280 () in let expr = let term = @@ -2270,6 +2271,7 @@ class scratch_window = ~packing:(vbox#pack ~expand:true ~padding:5) () in let sequent_viewer = TermViewer.sequent_viewer + ~mml_of_cic_sequent:ChosenTransformer.mml_of_cic_sequent ~packing:(scrolled_window#add) ~width:400 ~height:280 () in object(self) val mutable term = Cic.Rel 1 (* dummy value *) @@ -2350,8 +2352,9 @@ object(self) GBin.scrolled_window ~border_width:10 ~packing:(vbox1#pack ~expand:true ~padding:5) () in let proofw = - TermViewer.sequent_viewer ~width:400 ~height:275 - ~packing:(scrolled_window1#add) () in + TermViewer.sequent_viewer + ~mml_of_cic_sequent:ChosenTransformer.mml_of_cic_sequent + ~width:400 ~height:275 ~packing:(scrolled_window1#add) () in let _ = proofw_ref <- Some proofw in let hbox3 = GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in @@ -2530,8 +2533,9 @@ class empty_page = GBin.scrolled_window ~border_width:10 ~packing:(vbox1#pack ~expand:true ~padding:5) () in let proofw = - TermViewer.sequent_viewer ~width:400 ~height:275 - ~packing:(scrolled_window1#add) () in + TermViewer.sequent_viewer + ~mml_of_cic_sequent:ChosenTransformer.mml_of_cic_sequent + ~width:400 ~height:275 ~packing:(scrolled_window1#add) () in object(self) method proofw = (assert false : TermViewer.sequent_viewer) method content = vbox1 @@ -2848,7 +2852,11 @@ end (* MAIN *) let initialize_everything () = - let output = TermViewer.proof_viewer ~width:350 ~height:280 () in + let output = + TermViewer.proof_viewer + ~mml_of_cic_object:ChosenTransformer.mml_of_cic_object + ~width:350 ~height:280 () + in let notebook = new notebook in let rendering_window' = new rendering_window output notebook in rendering_window'#set_auto_disambiguation !auto_disambiguation; diff --git a/helm/gTopLevel/termViewer.ml b/helm/gTopLevel/termViewer.ml index 91b2dd1a7..841c61edf 100644 --- a/helm/gTopLevel/termViewer.ml +++ b/helm/gTopLevel/termViewer.ml @@ -32,6 +32,24 @@ (* *) (***************************************************************************) +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;; @@ -52,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 @@ -62,7 +80,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)) ; + debug_print (string_of_int (List.length self#get_selections)) ; let selections = self#get_selections in list_map_fail (function node -> @@ -71,7 +89,6 @@ 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 @@ -108,21 +125,27 @@ class sequent_viewer obj = method load_sequent metasenv sequent = (**** SIAM QUI ****) let sequent_mml,(ids_to_terms,ids_to_father_ids,ids_to_hypotheses) = - ChosenTransformer.mml_of_cic_sequent metasenv sequent + mml_of_cic_sequent metasenv sequent in self#load_doc ~dom:sequent_mml ; (* Misc.domImpl#saveDocumentToFile ~name:"/tmp/pippo" ~doc:sequent_mml () ; *) current_infos <- - Some (ids_to_terms,ids_to_father_ids,ids_to_hypotheses) + Some (ids_to_terms,ids_to_father_ids,ids_to_hypotheses) end ;; -let sequent_viewer ?hadjustment ?vadjustment ?font_size ?log_verbosity = +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 (GtkMathViewProps.MathView.create p)) ~font_size ~log_verbosity)) [] + (fun p -> + OgtkMathViewProps.set_params + (new sequent_viewer ~mml_of_cic_sequent + (GtkMathViewProps.MathView.create p)) + ~font_size ~log_verbosity)) [] ;; (* @@ -152,7 +175,7 @@ let sequent_viewer ?adjustmenth ?adjustmentv ?font_size ?font_manager (** 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 @@ -170,7 +193,6 @@ 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 @@ -208,7 +230,7 @@ class proof_viewer obj = = Cic2acic.acic_object_of_cic_object currentproof in let mml = - ChosenTransformer.mml_of_cic_object + mml_of_cic_object ~explode_all:true uri acic ids_to_inner_sorts ids_to_inner_types in current_infos <- @@ -221,26 +243,35 @@ class proof_viewer obj = 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") ; + 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 - prerr_endline ("XMLDIFF took " ^ string_of_float (time2 -. time1) ^ "seconds") ; + debug_print ("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")); + 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 ?hadjustment ?vadjustment ?font_size ?log_verbosity = +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 (GtkMathViewProps.MathView.create p)) ~font_size ~log_verbosity)) [] + (fun p -> + OgtkMathViewProps.set_params + (new proof_viewer ~mml_of_cic_object + (GtkMathViewProps.MathView.create p)) + ~font_size ~log_verbosity)) [] ;; (* @@ -268,6 +299,3 @@ let proof_viewer ?adjustmenth ?adjustmentv ?font_size ?font_manager ;; *) -let _ = - Cexpr2pres_hashtbl.init Cexpr2pres.cexpr2pres Cexpr2pres.cexpr2pres_charcount -;; diff --git a/helm/gTopLevel/termViewer.mli b/helm/gTopLevel/termViewer.mli index 0cc9ba93b..8fa37e531 100644 --- a/helm/gTopLevel/termViewer.mli +++ b/helm/gTopLevel/termViewer.mli @@ -33,9 +33,25 @@ (* *) (******************************************************************************) +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 + (** A widget to render sequents **) class sequent_viewer : + mml_of_cic_sequent:mml_of_cic_sequent -> Gtk_mathview.math_view Gtk.obj -> object inherit GMathViewAux.multi_selection_math_view @@ -52,6 +68,7 @@ class sequent_viewer : end val sequent_viewer : + mml_of_cic_sequent:mml_of_cic_sequent -> ?hadjustment:GData.adjustment -> ?vadjustment:GData.adjustment -> ?font_size:int -> @@ -66,6 +83,7 @@ val sequent_viewer : (** A widget to render proofs **) class proof_viewer : + mml_of_cic_object:mml_of_cic_object -> Gtk_mathview.math_view Gtk.obj -> object inherit GMathViewAux.single_selection_math_view @@ -88,6 +106,7 @@ class proof_viewer : end val proof_viewer : + mml_of_cic_object:mml_of_cic_object -> ?hadjustment:GData.adjustment -> ?vadjustment:GData.adjustment -> ?font_size:int -> @@ -98,3 +117,4 @@ val proof_viewer : ?packing:(GObj.widget -> unit) -> ?show:bool -> unit -> proof_viewer + -- 2.39.2