helm/matita/matitaMathView.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 open Printf
  36
  37 open MatitaTypes
  38
  39 (* List utility functions *)
  40 exception Skip
  41
  42 let list_map_fail f =
  43  let rec aux =
  44   function
  45      [] -> []
  46    | he::tl ->
  47       try
  48        let he' = f he in
  49         he'::(aux tl)
  50       with Skip ->
  51        (aux tl)
  52  in
  53   aux
  54
  55 (* End of the list utility functions *)
  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   method get_selected_terms =
  65    let selections = self#get_selections in
  66     list_map_fail
  67      (function node ->
  68        let xpath =
  69         ((node : Gdome.element)#getAttributeNS
  70           ~namespaceURI:Misc.helmns
  71           ~localName:(Gdome.domString "xref"))#to_string
  72        in
  73         if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
  74         else
  75          match current_infos with
  76             Some (ids_to_terms,_,_) ->
  77              let id = xpath in
  78               (try
  79                 Hashtbl.find ids_to_terms id
  80                with _ -> raise Skip)
  81           | None -> assert false (* "ERROR: No current term!!!" *)
  82      ) selections
  83
  84   method get_selected_hypotheses =
  85    let selections = self#get_selections in
  86     list_map_fail
  87      (function node ->
  88        let xpath =
  89         ((node : Gdome.element)#getAttributeNS
  90           ~namespaceURI:Misc.helmns
  91           ~localName:(Gdome.domString "xref"))#to_string
  92        in
  93         if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
  94         else
  95          match current_infos with
  96             Some (_,_,ids_to_hypotheses) ->
  97              let id = xpath in
  98               (try
  99                 Hashtbl.find ids_to_hypotheses id
 100                with _ -> raise Skip)
 101           | None -> assert false (* "ERROR: No current term!!!" *)
 102      ) selections
 103
 104   method load_sequent (mml:Gdome.document)
 105     (metadata:MatitaTypes.sequents_metadata) sequent_no
 106   =
 107     let (annconjecture, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts,
 108         ids_to_hypotheses)
 109     =
 110       try
 111         List.assoc sequent_no metadata
 112       with Not_found -> assert false
 113     in
 114     current_infos <- Some (ids_to_terms, ids_to_father_ids, ids_to_hypotheses);
 115     self#load_root ~root:mml#get_documentElement
 116  end
 117
 118 class proof_viewer obj =
 119  object(self)
 120
 121   inherit GMathViewAux.single_selection_math_view obj
 122
 123 (*   initializer self#set_log_verbosity 3 *)
 124
 125   val mutable current_infos = None
 126   val mutable current_mml = None
 127
 128   method load_proof (mml:Gdome.document) (metadata:MatitaTypes.proof_metadata) =
 129     let (acic, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts,
 130         ids_to_inner_types, ids_to_conjectures, ids_to_hypotheses) =
 131       metadata
 132     in
 133     current_infos <-
 134       Some
 135        (ids_to_terms,ids_to_father_ids,ids_to_conjectures,ids_to_hypotheses);
 136     match current_mml with
 137     |  None ->
 138         MatitaTypes.debug_print "no previous MathML";
 139         self#load_root ~root:mml#get_documentElement ;
 140         current_mml <- Some mml
 141     | Some current_mml' ->
 142         MatitaTypes.debug_print "Previous MathML available: xmldiffing ...";
 143         self#freeze ;
 144         XmlDiff.update_dom ~from:current_mml' mml ;
 145         self#thaw
 146   end
 147
 148 class sequents_viewer ~(notebook:GPack.notebook)
 149   ~(sequent_viewer:MatitaTypes.sequent_viewer) ()
 150 =
 151   object (self)
 152     val mutable pages = 0
 153     val mutable switch_page_callback = None
 154     val mutable mathmls = []
 155     val mutable metadata = None
 156     val mutable page2goal = []  (* associative list: page no -> goal no *)
 157     val mutable goal2page = []  (* the other way round *)
 158
 159     method reset =
 160       for i = 1 to pages do notebook#remove_page 0 done;
 161       pages <- 0;
 162       mathmls <- [];
 163       metadata <- None;
 164       page2goal <- [];
 165       goal2page <- [];
 166       (match switch_page_callback with
 167       | Some id ->
 168           GtkSignal.disconnect notebook#as_widget id;
 169           switch_page_callback <- None
 170       | None -> ())
 171
 172     method load_sequents (metadata': MatitaTypes.sequents_metadata) =
 173       metadata <- Some metadata';
 174       let sequents = metadata' in
 175       let sequents_no = List.length sequents in
 176       debug_print (sprintf "sequents no: %d" sequents_no);
 177       pages <- sequents_no;
 178       let widget = sequent_viewer#coerce in
 179       let page = ref 0 in
 180       List.iter
 181         (fun (metano, (asequent, _, _, ids_to_inner_sorts, _)) ->
 182           page2goal <- (!page, metano) :: page2goal;
 183           goal2page <- (metano, !page) :: goal2page;
 184           let tab_label =
 185             (GMisc.label ~text:(sprintf "?%d" metano) ~show:true ())#coerce
 186           in
 187           notebook#append_page ~tab_label widget;
 188           let mathml = lazy
 189             (let content_sequent = Cic2content.map_sequent asequent in
 190             let pres_sequent =
 191               Sequent2pres.sequent2pres ~ids_to_inner_sorts content_sequent
 192             in
 193             let xmlpres = Box.document_of_box pres_sequent in
 194             Xml2Gdome.document_of_xml Misc.domImpl xmlpres)
 195           in
 196           mathmls <- (metano, mathml) :: mathmls)
 197         sequents;
 198       mathmls <- List.rev mathmls;
 199       switch_page_callback <-
 200         (* TODO Zack the "#after" may probably be removed after Luca's fix for
 201         * widget not loading documents before being realized *)
 202         Some (notebook#connect#after#switch_page ~callback:(fun page ->
 203           debug_print "switch_page callback";
 204           self#render_page page))
 205
 206     method goto_sequent goal =
 207       let page =
 208         try
 209           List.assoc goal goal2page
 210         with Not_found -> assert false
 211       in
 212       notebook#goto_page page;
 213       self#render_page page
 214
 215     method private render_page page =
 216       let metadata =
 217         match metadata with Some metadata -> metadata | None -> assert false
 218       in
 219       let (metano, mathml) = List.nth mathmls page in
 220       sequent_viewer#load_sequent (Lazy.force mathml) metadata metano
 221
 222   end
 223
 224  (** constructors *)
 225
 226 let sequent_viewer ?hadjustment ?vadjustment ?font_size ?log_verbosity =
 227   GtkBase.Widget.size_params
 228     ~cont:(OgtkMathViewProps.pack_return (fun p ->
 229       OgtkMathViewProps.set_params
 230         (new sequent_viewer (GtkMathViewProps.MathView_GMetaDOM.create p))
 231         ~font_size ~log_verbosity))
 232     []
 233
 234 let proof_viewer ?hadjustment ?vadjustment ?font_size ?log_verbosity =
 235   GtkBase.Widget.size_params
 236     ~cont:(OgtkMathViewProps.pack_return (fun p ->
 237       OgtkMathViewProps.set_params
 238         (new proof_viewer (GtkMathViewProps.MathView_GMetaDOM.create p))
 239         ~font_size ~log_verbosity))
 240     []
 241
 242 let sequents_viewer ~(notebook:GPack.notebook)
 243   ~(sequent_viewer:MatitaTypes.sequent_viewer) ()
 244 =
 245   new sequents_viewer ~notebook ~sequent_viewer ()
 246