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 MatitaTypes
  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 (*
  56 class sequent_viewer obj =
  57  object(self)
  58
  59   inherit GMathViewAux.multi_selection_math_view obj
  60
  61   val mutable current_infos = None
  62
  63   method get_selected_terms =
  64    let selections = self#get_selections in
  65     list_map_fail
  66      (function node ->
  67        let xpath =
  68         ((node : Gdome.element)#getAttributeNS
  69           ~namespaceURI:Misc.helmns
  70           ~localName:(Gdome.domString "xref"))#to_string
  71        in
  72         if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
  73         else
  74          match current_infos with
  75             Some (ids_to_terms,_,_) ->
  76              let id = xpath in
  77               (try
  78                 Hashtbl.find ids_to_terms id
  79                with _ -> raise Skip)
  80           | None -> assert false (* "ERROR: No current term!!!" *)
  81      ) selections
  82
  83   method get_selected_hypotheses =
  84    let selections = self#get_selections in
  85     list_map_fail
  86      (function node ->
  87        let xpath =
  88         ((node : Gdome.element)#getAttributeNS
  89           ~namespaceURI:Misc.helmns
  90           ~localName:(Gdome.domString "xref"))#to_string
  91        in
  92         if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
  93         else
  94          match current_infos with
  95             Some (_,_,ids_to_hypotheses) ->
  96              let id = xpath in
  97               (try
  98                 Hashtbl.find ids_to_hypotheses id
  99                with _ -> raise Skip)
 100           | None -> assert false (* "ERROR: No current term!!!" *)
 101      ) selections
 102
 103   method load_sequent metasenv sequent =
 104    let sequent_mml,(ids_to_terms,ids_to_father_ids,ids_to_hypotheses) =
 105      mml_of_cic_sequent metasenv sequent
 106    in
 107     self#load_root ~root:sequent_mml#get_documentElement ;
 108      current_infos <-
 109       Some (ids_to_terms,ids_to_father_ids,ids_to_hypotheses)
 110  end
 111 *)
 112
 113 class proof_viewer obj =
 114  object(self)
 115
 116   inherit GMathViewAux.single_selection_math_view obj
 117
 118 (*   initializer self#set_log_verbosity 3 *)
 119
 120   val mutable current_infos = None
 121   val mutable current_mml = None
 122
 123   method load_proof (mml:Gdome.document) (metadata:MatitaTypes.hist_metadata) =
 124     let (acic, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts,
 125         ids_to_inner_types, ids_to_conjectures, ids_to_hypotheses) =
 126       metadata
 127     in
 128     current_infos <-
 129       Some
 130        (ids_to_terms,ids_to_father_ids,ids_to_conjectures,ids_to_hypotheses);
 131     match current_mml with
 132     |  None ->
 133         MatitaTypes.debug_print "no previous MathML";
 134         self#load_root ~root:mml#get_documentElement ;
 135         current_mml <- Some mml
 136     | Some current_mml' ->
 137         MatitaTypes.debug_print "Previous MathML available: xmldiffing ...";
 138         self#freeze ;
 139         XmlDiff.update_dom ~from:current_mml' mml ;
 140         self#thaw
 141   end
 142
 143  (** constructors *)
 144
 145 (*
 146 let sequent_viewer ?hadjustment ?vadjustment ?font_size ?log_verbosity =
 147   GtkBase.Widget.size_params
 148     ~cont:(OgtkMathViewProps.pack_return (fun p ->
 149       OgtkMathViewProps.set_params
 150         (new sequent_viewer (GtkMathViewProps.MathView_GMetaDOM.create p))
 151         ~font_size ~log_verbosity))
 152     []
 153 *)
 154
 155 let proof_viewer ?hadjustment ?vadjustment ?font_size ?log_verbosity =
 156   GtkBase.Widget.size_params
 157     ~cont:(OgtkMathViewProps.pack_return (fun p ->
 158       OgtkMathViewProps.set_params
 159         (new proof_viewer (GtkMathViewProps.MathView_GMetaDOM.create p))
 160         ~font_size ~log_verbosity))
 161     []
 162