From 06c2b37f3d7d4e14cabeef3b18211e5d12b9b4eb Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Fri, 1 Oct 2004 16:32:36 +0000 Subject: [PATCH] snapshot --- helm/matita/matita.ml | 53 ++++++++++++++++++-------------- helm/matita/matitaMathView.ml | 55 +++++++++++++++++----------------- helm/matita/matitaMathView.mli | 30 ++++++++++++++----- helm/matita/matitaProof.ml | 29 +++++++++--------- helm/matita/matitaTypes.ml | 21 ++++++++----- 5 files changed, 108 insertions(+), 80 deletions(-) diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml index 5fb0cb906..3c543d5c1 100644 --- a/helm/matita/matita.ml +++ b/helm/matita/matita.ml @@ -42,6 +42,12 @@ let (get_proof, set_proof, has_proof) = let debug_print = MatitaTypes.debug_print +let save_dom = + let domImpl = lazy (Gdome.domImplementation ()) in + fun ~doc ~dest -> + ignore + ((Lazy.force domImpl)#saveDocumentToFile ~doc ~name:dest ~indent:true ()) + (** {2 Initialization} *) let _ = Helm_registry.load_from "matita.conf.xml" @@ -56,8 +62,11 @@ let disambiguator = () let proof_viewer = let mml_of_cic_object = BuildTimeConf.Transformer.mml_of_cic_object in - MatitaMathView.proof_viewer ~mml_of_cic_object ~show:true - ~packing:(gui#proof#scrolledProof#add) () +(* + let frame = GBin.frame ~packing:(gui#proof#scrolledProof#add) ~show:true () in + MatitaMathView.proof_viewer ~show:true ~packing:(frame#add) () +*) + MatitaMathView.proof_viewer ~show:true ~packing:(gui#proof#scrolledProof#add) () (* let sequent_viewer = let mml_of_cic_sequent = BuildTimeConf.Transformer.mml_of_cic_sequent in @@ -70,28 +79,28 @@ let new_proof (proof: MatitaTypes.proof) = * - ids_to_inner_types, ids_to_inner_sorts handling * - sequent viewer notification *) - let xmldump_observer _ (status, _) = print_endline proof#toString in - ignore (proof#attach_observer ~interested_in:StatefulProofEngine.all_events - xmldump_observer); -(* - let proof_observer _ (status, ()) = -prerr_endline "proof_observer"; - let ((uri_opt, metasenv, bo, ty), _) = status in + let xmldump_observer _ _ = print_endline proof#toString in + let proof_observer _ (status, metadata) = + debug_print "proof_observer"; + let (acic, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts, + ids_to_inner_types, ids_to_conjectures, ids_to_hypotheses) = + metadata + in + let ((uri_opt, _, _, _), _) = status in let uri = MatitaTypes.unopt_uri uri_opt in - (* TODO CSC [] is wrong *) - let proof = Cic.Constant (UriManager.name_of_uri uri,Some bo,ty,[]) in -try - ignore (proof_viewer#load_proof uri proof) -with exn -> -prerr_endline "proof_observer exception:"; -prerr_endline (Printexc.to_string exn); -raise exn - in - let proof_observer_id = - proof#attach_observer ~interested_in:StatefulProofEngine.all_events - proof_observer + debug_print "apply transformation"; + let mathml = + BuildTimeConf.Transformer.mml_of_cic_object + ~explode_all:true uri acic ids_to_inner_sorts ids_to_inner_types + in + if BuildTimeConf.debug then save_dom ~doc:mathml ~dest:"/tmp/matita.xml"; + proof_viewer#load_proof mathml metadata; + debug_print "/proof_observer" in -*) + ignore (proof#attach_observer ~interested_in:StatefulProofEngine.all_events + xmldump_observer); + ignore (proof#attach_observer ~interested_in:StatefulProofEngine.all_events + proof_observer); proof#notify; set_proof (Some proof) diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index c323dbbf0..58a6f7a96 100644 --- a/helm/matita/matitaMathView.ml +++ b/helm/matita/matitaMathView.ml @@ -35,7 +35,7 @@ open MatitaTypes (* List utility functions *) -exception Skip;; +exception Skip let list_map_fail f = let rec aux = @@ -49,10 +49,11 @@ let list_map_fail f = (aux tl) in aux -;; + (* End of the list utility functions *) -class sequent_viewer ~(mml_of_cic_sequent:mml_of_cic_sequent) obj = +(* +class sequent_viewer obj = object(self) inherit GMathViewAux.multi_selection_math_view obj @@ -107,57 +108,55 @@ class sequent_viewer ~(mml_of_cic_sequent:mml_of_cic_sequent) obj = current_infos <- Some (ids_to_terms,ids_to_father_ids,ids_to_hypotheses) end -;; +*) -class proof_viewer ~(mml_of_cic_object:mml_of_cic_object) obj = +class proof_viewer obj = object(self) inherit GMathViewAux.single_selection_math_view obj +(* initializer self#set_log_verbosity 3 *) + val mutable current_infos = None val mutable current_mml = None - 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 = - mml_of_cic_object - ~explode_all:true uri acic ids_to_inner_sorts ids_to_inner_types + method load_proof (mml:Gdome.document) (metadata:MatitaTypes.hist_metadata) = + let (acic, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts, + ids_to_inner_types, ids_to_conjectures, ids_to_hypotheses) = + metadata in current_infos <- Some (ids_to_terms,ids_to_father_ids,ids_to_conjectures,ids_to_hypotheses); - (match current_mml with - None -> + match current_mml with + | None -> + MatitaTypes.debug_print "no previous MathML"; self#load_root ~root:mml#get_documentElement ; current_mml <- Some mml | Some current_mml' -> + MatitaTypes.debug_print "Previous MathML available: xmldiffing ..."; self#freeze ; XmlDiff.update_dom ~from:current_mml' mml ; - self#thaw); - (acic, ids_to_inner_types, ids_to_inner_sorts) + self#thaw end (** constructors *) -let sequent_viewer ~(mml_of_cic_sequent: mml_of_cic_sequent) = +(* +let sequent_viewer ?hadjustment ?vadjustment ?font_size ?log_verbosity = GtkBase.Widget.size_params ~cont:(OgtkMathViewProps.pack_return (fun p -> OgtkMathViewProps.set_params - (new sequent_viewer ~mml_of_cic_sequent - (GtkMathViewProps.MathView_GMetaDOM.create p)) - ?font_size:None ?log_verbosity:None)) - ?width:None ?height:None [] + (new sequent_viewer (GtkMathViewProps.MathView_GMetaDOM.create p)) + ~font_size ~log_verbosity)) + [] +*) -let proof_viewer ~(mml_of_cic_object: mml_of_cic_object) = +let proof_viewer ?hadjustment ?vadjustment ?font_size ?log_verbosity = GtkBase.Widget.size_params ~cont:(OgtkMathViewProps.pack_return (fun p -> OgtkMathViewProps.set_params - (new proof_viewer ~mml_of_cic_object - (GtkMathViewProps.MathView_GMetaDOM.create p)) - ?font_size:None ?log_verbosity:None)) - ?width:None ?height:None [] + (new proof_viewer (GtkMathViewProps.MathView_GMetaDOM.create p)) + ~font_size ~log_verbosity)) + [] diff --git a/helm/matita/matitaMathView.mli b/helm/matita/matitaMathView.mli index 51a1743f6..0aef1cc18 100644 --- a/helm/matita/matitaMathView.mli +++ b/helm/matita/matitaMathView.mli @@ -23,15 +23,29 @@ * http://helm.cs.unibo.it/ *) -val sequent_viewer : - mml_of_cic_sequent:MatitaTypes.mml_of_cic_sequent -> - ?packing:(GObj.widget -> unit) -> ?show:bool -> - unit -> - MatitaTypes.sequent_viewer - val proof_viewer : - mml_of_cic_object:MatitaTypes.mml_of_cic_object -> - ?packing:(GObj.widget -> unit) -> ?show:bool -> + ?hadjustment:GData.adjustment -> + ?vadjustment:GData.adjustment -> + ?font_size:int -> + ?log_verbosity:int -> + ?width:int -> + ?height:int -> + ?packing:(GObj.widget -> unit) -> + ?show:bool -> unit -> MatitaTypes.proof_viewer +(* +val sequent_viewer : + ?hadjustment:GData.adjustment -> + ?vadjustment:GData.adjustment -> + ?font_size:int -> + ?log_verbosity:int -> + ?width:int -> + ?height:int -> + ?packing:(GObj.widget -> unit) -> + ?show:bool -> + unit -> + MatitaTypes.sequent_viewer +*) + diff --git a/helm/matita/matitaProof.ml b/helm/matita/matitaProof.ml index 98b9cf02c..17b44ffd3 100644 --- a/helm/matita/matitaProof.ml +++ b/helm/matita/matitaProof.ml @@ -23,26 +23,25 @@ * http://helm.cs.unibo.it/ *) + (** create a Cic.CurrentProof from a given proof *) +let currentProof (uri, metasenv, bo, ty) = + let uri = MatitaTypes.unopt_uri uri in + (* TODO CSC: Wrong: [] is just plainly wrong *) + Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, []) + class proof ?uri ~typ ~metasenv ~body () = object (self) - inherit [unit] StatefulProofEngine.status ?uri ~typ ~body ~metasenv - (fun _ -> ()) - (fun _ _ -> ()) - () - - method private currentProof = - let (uri, metasenv, bo, ty) = self#proof in - let uri = - match uri with - | Some uri -> uri - | None -> MatitaTypes.untitled_con_uri - in - (* TODO CSC: Wrong: [] is just plainly wrong *) - Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, []) + inherit [MatitaTypes.hist_metadata] + StatefulProofEngine.status ?uri ~typ ~body ~metasenv + (fun proof -> + Cic2acic.acic_object_of_cic_object (currentProof (fst proof))) + (fun (old_proof, old_metadata) new_proof -> + Cic2acic.acic_object_of_cic_object (currentProof (fst new_proof))) + () method toXml = - let currentproof = self#currentProof in + let currentproof = currentProof self#proof in let (acurrentproof,_,_,ids_to_inner_sorts,_,_,_) = Cic2acic.acic_object_of_cic_object ~eta_fix:false currentproof in diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml index 2811fd5d4..70f912ae0 100644 --- a/helm/matita/matitaTypes.ml +++ b/helm/matita/matitaTypes.ml @@ -77,9 +77,18 @@ class type disambiguator = (DisambiguateTypes.environment * Cic.metasenv * Cic.term) end +type hist_metadata = + Cic.annobj * + (Cic.id, Cic.term) Hashtbl.t * + (Cic.id, Cic.id option) Hashtbl.t * + (Cic.id, string) Hashtbl.t * + (Cic.id, Cic2acic.anntypes) Hashtbl.t * + (Cic.id, Cic.conjecture) Hashtbl.t * + (Cic.id, Cic.hypothesis) Hashtbl.t + class type proof = object - inherit [unit] StatefulProofEngine.status + inherit [hist_metadata] StatefulProofEngine.status (** return a pair of "xml" (as defined in Xml module) representing the * * current proof type and body, respectively *) @@ -113,9 +122,10 @@ type mml_of_cic_sequent = type mml_of_cic_object = explode_all:bool -> UriManager.uri -> Cic.annobj -> - (string, string) Hashtbl.t -> - (string, Cic2acic.anntypes) Hashtbl.t -> Gdome.document + (string, string) Hashtbl.t -> (string, Cic2acic.anntypes) Hashtbl.t -> + Gdome.document + (** TODO Zack to be reviewed and unified with proof_viewer above *) class type sequent_viewer = object inherit GMathViewAux.multi_selection_math_view @@ -138,10 +148,7 @@ class type proof_viewer = (** @return the annotated cic term and the ids_to_inner_types and * ids_to_inner_sorts maps *) - method load_proof : - UriManager.uri -> Cic.obj -> - Cic.annobj * (Cic.id, Cic2acic.anntypes) Hashtbl.t * - (Cic.id, string) Hashtbl.t + method load_proof: Gdome.document -> hist_metadata -> unit end -- 2.39.2