helm/gTopLevel/termViewer.ml

   1 (* Copyright (C) 2000-2002, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://cs.unibo.it/helm/.
  24  *)
  25
  26 (***************************************************************************)
  27 (*                                                                         *)
  28 (*                             PROJECT HELM                                *)
  29 (*                                                                         *)
  30 (*                  29/01/2003 Claudio Sacerdoti Coen                      *)
  31 (*                                                                         *)
  32 (*                                                                         *)
  33 (***************************************************************************)
  34
  35 let use_stylesheets = ref false;;(* false performs the transformations in OCaml*)
  36
  37 (* List utility functions *)
  38 exception Skip;;
  39
  40 let list_map_fail f =
  41  let rec aux =
  42   function
  43      [] -> []
  44    | he::tl ->
  45       try
  46        let he' = f he in
  47         he'::(aux tl)
  48       with Skip ->
  49        (aux tl)
  50  in
  51   aux
  52 ;;
  53 (* End of the list utility functions *)
  54
  55 (** A widget to render sequents **)
  56
  57 class sequent_viewer obj =
  58  object(self)
  59
  60   inherit GMathViewAux.multi_selection_math_view obj
  61
  62   val mutable current_infos = None
  63
  64   (* returns the list of selected terms         *)
  65   (* selections which are not terms are ignored *)
  66   method get_selected_terms =
  67    prerr_endline (string_of_int (List.length self#get_selections)) ;
  68    let selections = self#get_selections in
  69     list_map_fail
  70      (function node ->
  71        let xpath =
  72         ((node : Gdome.element)#getAttributeNS
  73           ~namespaceURI:Misc.helmns
  74           ~localName:(Gdome.domString "xref"))#to_string
  75        in
  76         prerr_endline ("YAHHHHHHHHHH " ^ xpath) ;
  77         if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
  78         else
  79          match current_infos with
  80             Some (ids_to_terms,_,_) ->
  81              let id = xpath in
  82               (try
  83                 Hashtbl.find ids_to_terms id
  84                with _ -> raise Skip)
  85           | None -> assert false (* "ERROR: No current term!!!" *)
  86      ) selections
  87
  88   (* returns the list of selected hypotheses         *)
  89   (* selections which are not hypotheses are ignored *)
  90   method get_selected_hypotheses =
  91    let selections = self#get_selections in
  92     list_map_fail
  93      (function node ->
  94        let xpath =
  95         ((node : Gdome.element)#getAttributeNS
  96           ~namespaceURI:Misc.helmns
  97           ~localName:(Gdome.domString "xref"))#to_string
  98        in
  99         if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
 100         else
 101          match current_infos with
 102             Some (_,_,ids_to_hypotheses) ->
 103              let id = xpath in
 104               (try
 105                 Hashtbl.find ids_to_hypotheses id
 106                with _ -> raise Skip)
 107           | None -> assert false (* "ERROR: No current term!!!" *)
 108      ) selections
 109
 110   method load_sequent metasenv sequent =
 111 (**** SIAM QUI ****)
 112    let sequent_mml,(ids_to_terms,ids_to_father_ids,ids_to_hypotheses) =
 113      if !use_stylesheets then
 114        ApplyStylesheets.mml_of_cic_sequent metasenv sequent
 115      else
 116        ApplyTransformation.mml_of_cic_sequent metasenv sequent
 117    in
 118     self#load_doc ~dom:sequent_mml ;
 119 (*
 120 Misc.domImpl#saveDocumentToFile ~name:"/tmp/pippo" ~doc:sequent_mml () ;
 121 *)
 122      current_infos <-
 123      Some (ids_to_terms,ids_to_father_ids,ids_to_hypotheses)
 124  end
 125 ;;
 126
 127 let sequent_viewer ?hadjustment ?vadjustment ?font_size ?log_verbosity =
 128   GtkBase.Container.make_params ~cont:(
 129   OgtkMathViewProps.pack_return
 130     (fun p -> OgtkMathViewProps.set_params (new sequent_viewer (GtkMathViewProps.MathView.create p)) ~font_size ~log_verbosity)) []
 131 ;;
 132
 133 (*
 134 let sequent_viewer ?adjustmenth ?adjustmentv ?font_size ?font_manager
 135  ?border_width ?width ?height ?packing ?show () =
 136  let w =
 137    GtkMathView.MathView.create
 138     ?adjustmenth:(Gaux.may_map ~f:GData.as_adjustment adjustmenth)
 139     ?adjustmentv:(Gaux.may_map ~f:GData.as_adjustment adjustmentv)
 140     ()
 141  in
 142   GtkBase.Container.set w ?border_width ?width ?height;
 143  let mathview = GObj.pack_return (new sequent_viewer w) ~packing ~show in
 144  begin
 145     match font_size with
 146     | Some size -> mathview#set_font_size size
 147     | None      -> ()
 148   end;
 149   begin
 150     match font_manager with
 151     | Some manager -> mathview#set_font_manager_type ~fm_type:manager
 152     | None         -> ()
 153   end;
 154   mathview
 155 ;;
 156 *)
 157
 158 (** A widget to render proofs **)
 159
 160 class proof_viewer obj =
 161  object(self)
 162
 163   inherit GMathViewAux.single_selection_math_view obj
 164
 165 (*   initializer self#set_font_size 10 *)
 166
 167   val mutable current_infos = None
 168   val mutable current_mml = None
 169
 170   method make_sequent_of_selected_term =
 171    match self#get_selection with
 172       Some node ->
 173        let xpath =
 174         ((node : Gdome.element)#getAttributeNS
 175           ~namespaceURI:Misc.helmns
 176           ~localName:(Gdome.domString "xref"))#to_string
 177        in
 178         prerr_endline ("YAEEEEEEEEEEEEEEEEEEE " ^ xpath) ;
 179         if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
 180         else
 181          begin
 182           match current_infos with
 183              Some (ids_to_terms, ids_to_father_ids, _, _) ->
 184               let id = xpath in
 185                LogicalOperations.to_sequent id ids_to_terms ids_to_father_ids
 186            | None -> assert false (* "ERROR: No current term!!!" *)
 187          end
 188     | None -> assert false (* "ERROR: No selection!!!" *)
 189
 190   method focus_sequent_of_selected_term =
 191    match self#get_selection with
 192       Some node ->
 193        let xpath =
 194         ((node : Gdome.element)#getAttributeNS
 195           ~namespaceURI:Misc.helmns
 196           ~localName:(Gdome.domString "xref"))#to_string
 197        in
 198         if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
 199         else
 200          begin
 201           match current_infos with
 202              Some (ids_to_terms, ids_to_father_ids, _, _) ->
 203               let id = xpath in
 204                LogicalOperations.focus id ids_to_terms ids_to_father_ids
 205            | None -> assert false (* "ERROR: No current term!!!" *)
 206          end
 207     | None -> assert false (* "ERROR: No selection!!!" *)
 208
 209   method load_proof uri currentproof =
 210     let
 211       (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
 212        ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
 213       = Cic2acic.acic_object_of_cic_object currentproof
 214     in
 215     let mml =
 216       if !use_stylesheets then
 217         ApplyStylesheets.mml_of_cic_object
 218           ~explode_all:true uri acic ids_to_inner_sorts ids_to_inner_types
 219       else
 220         ApplyTransformation.mml_of_cic_object
 221           ~explode_all:true uri acic ids_to_inner_sorts ids_to_inner_types in
 222     current_infos <-
 223       Some
 224        (ids_to_terms,ids_to_father_ids,ids_to_conjectures,ids_to_hypotheses);
 225     (* self#load_doc ~dom:mml ;
 226        current_mml <- Some mml ; *)
 227     (match current_mml with
 228       None ->
 229         let time1 = Sys.time () in
 230         self#load_doc ~dom:mml ;
 231         let time2 = Sys.time () in
 232         prerr_endline ("Loading and displaying the proof took " ^ string_of_float (time2 -. time1) ^ "seconds") ;
 233         current_mml <- Some mml
 234     | Some current_mml' ->
 235         self#freeze ;
 236         let time1 = Sys.time () in
 237         XmlDiff.update_dom ~from:current_mml' mml ;
 238         let time2 = Sys.time () in
 239         prerr_endline ("XMLDIFF took " ^ string_of_float (time2 -. time1) ^ "seconds") ;
 240         self#thaw ;
 241         let time3 = Sys.time () in
 242         prerr_endline ("The refresh of the widget took " ^ string_of_float (time3 -. time2) ^ "seconds"));
 243     (acic, ids_to_inner_types, ids_to_inner_sorts)
 244   end
 245 ;;
 246
 247
 248 let proof_viewer ?hadjustment ?vadjustment ?font_size ?log_verbosity =
 249   GtkBase.Container.make_params ~cont:(
 250   OgtkMathViewProps.pack_return
 251     (fun p -> OgtkMathViewProps.set_params (new proof_viewer (GtkMathViewProps.MathView.create p)) ~font_size ~log_verbosity)) []
 252 ;;
 253
 254 (*
 255 let proof_viewer ?adjustmenth ?adjustmentv ?font_size ?font_manager
 256  ?border_width ?width ?height ?packing ?show () =
 257  let w =
 258    GtkMathView.MathView.create
 259     ?adjustmenth:(Gaux.may_map ~f:GData.as_adjustment adjustmenth)
 260     ?adjustmentv:(Gaux.may_map ~f:GData.as_adjustment adjustmentv)
 261     ()
 262  in
 263   GtkBase.Container.set w ?border_width ?width ?height;
 264  let mathview = GObj.pack_return (new proof_viewer w) ~packing ~show in
 265  begin
 266     match font_size with
 267     | Some size -> mathview#set_font_size size
 268     | None      -> ()
 269   end;
 270   begin
 271     match font_manager with
 272     | Some manager -> mathview#set_font_manager_type ~fm_type:manager
 273     | None         -> ()
 274   end;
 275   mathview
 276 ;;
 277 *)
 278
 279 let _ =
 280  Cexpr2pres_hashtbl.init Cexpr2pres.cexpr2pres Cexpr2pres.cexpr2pres_charcount
 281 ;;