X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FtermViewer.ml;fp=helm%2FgTopLevel%2FtermViewer.ml;h=0000000000000000000000000000000000000000;hb=c7514aaa249a96c5fdd39b1123fbdb38d92f20b6;hp=be755821ef29f79ecd0f85b9aa5bff3e002f6a46;hpb=1c7fb836e2af4f2f3d18afd0396701f2094265ff;p=helm.git diff --git a/helm/gTopLevel/termViewer.ml b/helm/gTopLevel/termViewer.ml deleted file mode 100644 index be755821e..000000000 --- a/helm/gTopLevel/termViewer.ml +++ /dev/null @@ -1,294 +0,0 @@ -(* Copyright (C) 2000-2002, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Claudio Sacerdoti Coen *) -(* 29/01/2003 *) -(* *) -(* *) -(******************************************************************************) - -let use_stylesheets = ref false;;(* false performs the transformations in OCaml*) - -(* List utility functions *) -exception Skip;; - -let list_map_fail f = - let rec aux = - function - [] -> [] - | he::tl -> - try - let he' = f he in - he'::(aux tl) - with Skip -> - (aux tl) - in - aux -;; -(* End of the list utility functions *) - -(** A widget to render sequents **) - -class sequent_viewer obj = - object(self) - - inherit GMathViewAux.multi_selection_math_view obj - - val mutable current_infos = None - - (* returns the list of selected terms *) - (* selections which are not terms are ignored *) - method get_selected_terms = - let selections = self#get_selections in - list_map_fail - (function node -> - let xpath = - ((node : Gdome.element)#getAttributeNS - ~namespaceURI:Misc.helmns - ~localName:(Gdome.domString "xref"))#to_string - in - if xpath = "" then assert false (* "ERROR: No xref found!!!" *) - else - match current_infos with - Some (ids_to_terms,_,_) -> - let id = xpath in - (try - Hashtbl.find ids_to_terms id - with _ -> raise Skip) - | None -> assert false (* "ERROR: No current term!!!" *) - ) selections - - (* returns the list of selected hypotheses *) - (* selections which are not hypotheses are ignored *) - method get_selected_hypotheses = - let selections = self#get_selections in - list_map_fail - (function node -> - let xpath = - ((node : Gdome.element)#getAttributeNS - ~namespaceURI:Misc.helmns - ~localName:(Gdome.domString "xref"))#to_string - in - if xpath = "" then assert false (* "ERROR: No xref found!!!" *) - else - match current_infos with - Some (_,_,ids_to_hypotheses) -> - let id = xpath in - (try - Hashtbl.find ids_to_hypotheses id - with _ -> raise Skip) - | None -> assert false (* "ERROR: No current term!!!" *) - ) selections - - method load_sequent metasenv sequent = - let sequent_mml,(ids_to_terms,ids_to_father_ids,ids_to_hypotheses) = - ApplyStylesheets.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) - end -;; - -let sequent_viewer ?adjustmenth ?adjustmentv ?font_size ?font_manager - ?border_width ?width ?height ?packing ?show () = - let w = - GtkMathView.MathView.create - ?adjustmenth:(Gaux.may_map ~f:GData.as_adjustment adjustmenth) - ?adjustmentv:(Gaux.may_map ~f:GData.as_adjustment adjustmentv) - () - in - GtkBase.Container.set w ?border_width ?width ?height; - let mathview = GObj.pack_return (new sequent_viewer w) ~packing ~show in - begin - match font_size with - | Some size -> mathview#set_font_size size - | None -> () - end; - begin - match font_manager with - | Some manager -> mathview#set_font_manager_type ~fm_type:manager - | None -> () - end; - mathview -;; - - -(** A widget to render proofs **) - -class proof_viewer obj = - object(self) - - inherit GMathViewAux.single_selection_math_view 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 - Some node -> - let xpath = - ((node : Gdome.element)#getAttributeNS - ~namespaceURI:Misc.helmns - ~localName:(Gdome.domString "xref"))#to_string - in - if xpath = "" then assert false (* "ERROR: No xref found!!!" *) - else - begin - match current_infos with - Some (ids_to_terms, ids_to_father_ids, _, _) -> - let id = xpath in - LogicalOperations.to_sequent id ids_to_terms ids_to_father_ids - | None -> assert false (* "ERROR: No current term!!!" *) - end - | None -> assert false (* "ERROR: No selection!!!" *) - - method focus_sequent_of_selected_term = - match self#get_selection with - Some node -> - let xpath = - ((node : Gdome.element)#getAttributeNS - ~namespaceURI:Misc.helmns - ~localName:(Gdome.domString "xref"))#to_string - in - if xpath = "" then assert false (* "ERROR: No xref found!!!" *) - else - begin - match current_infos with - Some (ids_to_terms, ids_to_father_ids, _, _) -> - let id = xpath in - LogicalOperations.focus id ids_to_terms ids_to_father_ids - | None -> assert false (* "ERROR: No current term!!!" *) - 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 - 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) ; - 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") - ) ; -(* - self#load_doc ~dom:mml ; - current_mml <- Some 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); - (acic, ids_to_inner_types, ids_to_inner_sorts) - end -;; - -let proof_viewer ?adjustmenth ?adjustmentv ?font_size ?font_manager - ?border_width ?width ?height ?packing ?show () = - let w = - GtkMathView.MathView.create - ?adjustmenth:(Gaux.may_map ~f:GData.as_adjustment adjustmenth) - ?adjustmentv:(Gaux.may_map ~f:GData.as_adjustment adjustmentv) - () - in - GtkBase.Container.set w ?border_width ?width ?height; - let mathview = GObj.pack_return (new proof_viewer w) ~packing ~show in - begin - match font_size with - | Some size -> mathview#set_font_size size - | None -> () - end; - begin - match font_manager with - | Some manager -> mathview#set_font_manager_type ~fm_type:manager - | None -> () - end; - mathview -;; - -let _ = - Cexpr2pres_hashtbl.init Cexpr2pres.cexpr2pres Cexpr2pres.cexpr2pres_charcount -;;