]> matita.cs.unibo.it Git - helm.git/blob - helm/gTopLevel/termViewer.ml
snapshort
[helm.git] / 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 debug = false
36 let debug_print s = if debug then prerr_endline s
37
38 type mml_of_cic_sequent =
39  Cic.metasenv ->
40  int * Cic.context * Cic.term ->
41  Gdome.document * 
42  (Cic.annconjecture *
43   ((Cic.id, Cic.term) Hashtbl.t *
44    (Cic.id, Cic.id option) Hashtbl.t *
45    (string, Cic.hypothesis) Hashtbl.t *
46    (Cic.id, string) Hashtbl.t))
47    
48
49 type mml_of_cic_object =
50   Cic.obj ->
51   Gdome.document * 
52   (Cic.annobj * 
53    ((Cic.id, Cic.term) Hashtbl.t * 
54     (Cic.id, Cic.id option) Hashtbl.t *
55     (Cic.id, Cic.conjecture) Hashtbl.t * 
56     (Cic.id, Cic.hypothesis) Hashtbl.t *
57     (Cic.id, string) Hashtbl.t *   
58     (Cic.id, Cic2acic.anntypes) Hashtbl.t))
59   
60 (* List utility functions *)
61 exception Skip;;
62
63 let list_map_fail f =
64  let rec aux =
65   function
66      [] -> []
67    | he::tl ->
68       try
69        let he' = f he in
70         he'::(aux tl)
71       with Skip ->
72        (aux tl)
73  in
74   aux
75 ;;
76 (* End of the list utility functions *)
77
78 (** A widget to render sequents **)
79
80 class sequent_viewer ~(mml_of_cic_sequent:mml_of_cic_sequent) obj =
81  object(self)
82
83   inherit GMathViewAux.multi_selection_math_view obj
84
85   val mutable current_infos = None
86
87   (* returns the list of selected terms         *)
88   (* selections which are not terms are ignored *)
89   method get_selected_terms =
90    debug_print (string_of_int (List.length self#get_selections)) ;
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.helm_ns
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_terms,_,_) ->
103              let id = xpath in
104               (try
105                 Hashtbl.find ids_to_terms id
106                with _ -> raise Skip)
107           | None -> assert false (* "ERROR: No current term!!!" *)
108      ) selections
109
110   (* returns the list of selected hypotheses         *)
111   (* selections which are not hypotheses are ignored *)
112   method get_selected_hypotheses =
113    let selections = self#get_selections in
114     list_map_fail
115      (function node ->
116        let xpath =
117         ((node : Gdome.element)#getAttributeNS
118           ~namespaceURI:Misc.helm_ns
119           ~localName:(Gdome.domString "xref"))#to_string
120        in
121         if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
122         else
123          match current_infos with
124             Some (_,_,ids_to_hypotheses) ->
125              let id = xpath in
126               (try
127                 Hashtbl.find ids_to_hypotheses id
128                with _ -> raise Skip)
129           | None -> assert false (* "ERROR: No current term!!!" *)
130      ) selections
131   
132   method load_sequent metasenv sequent =
133 (**** SIAM QUI ****)
134    let sequent_mml,(_,(ids_to_terms,ids_to_father_ids,ids_to_hypotheses,ids_to_inner_sorts)) =
135      mml_of_cic_sequent metasenv sequent
136    in
137     self#load_root ~root:sequent_mml#get_documentElement ;
138 ignore (Misc.domImpl#saveDocumentToFile ~name:"/tmp/pippo" ~doc:sequent_mml ());
139      current_infos <-
140       Some (ids_to_terms,ids_to_father_ids,ids_to_hypotheses)
141  end
142 ;;
143
144 let sequent_viewer ~(mml_of_cic_sequent: mml_of_cic_sequent)
145   ?hadjustment ?vadjustment ?font_size ?log_verbosity
146 =
147   GtkBase.Widget.size_params ~cont:(
148   OgtkMathViewProps.pack_return
149     (fun p ->
150       OgtkMathViewProps.set_params
151         (new sequent_viewer ~mml_of_cic_sequent
152           (GtkMathViewProps.MathView_GMetaDOM.create p))
153         ~font_size ~log_verbosity)) []
154 ;;
155
156 (*
157 let sequent_viewer ?adjustmenth ?adjustmentv ?font_size ?font_manager
158  ?border_width ?width ?height ?packing ?show () =
159  let w =
160    GtkMathView.MathView.create
161     ?adjustmenth:(Gaux.may_map ~f:GData.as_adjustment adjustmenth)
162     ?adjustmentv:(Gaux.may_map ~f:GData.as_adjustment adjustmentv)
163     ()
164  in
165   GtkBase.Container.set w ?border_width ?width ?height;
166  let mathview = GObj.pack_return (new sequent_viewer w) ~packing ~show in
167  begin
168     match font_size with
169     | Some size -> mathview#set_font_size size
170     | None      -> ()
171   end;
172   begin
173     match font_manager with
174     | Some manager -> mathview#set_font_manager_type ~fm_type:manager
175     | None         -> ()
176   end;
177   mathview
178 ;;
179 *)
180
181 (** A widget to render proofs **)
182
183 class proof_viewer ~(mml_of_cic_object:mml_of_cic_object) obj =
184  object(self)
185
186   inherit GMathViewAux.single_selection_math_view obj
187
188 (*   initializer self#set_font_size 10 *)
189
190   val mutable current_infos = None
191   val mutable current_mml = None
192
193   method make_sequent_of_selected_term =
194    match self#get_selection with
195       Some node ->
196        let xpath =
197         ((node : Gdome.element)#getAttributeNS
198           ~namespaceURI:Misc.helm_ns
199           ~localName:(Gdome.domString "xref"))#to_string
200        in
201         if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
202         else
203          begin
204           match current_infos with
205              Some (ids_to_terms, ids_to_father_ids, _, _) ->
206               let id = xpath in
207                LogicalOperations.to_sequent id ids_to_terms ids_to_father_ids
208            | None -> assert false (* "ERROR: No current term!!!" *)
209          end
210     | None -> assert false (* "ERROR: No selection!!!" *)
211
212   method focus_sequent_of_selected_term =
213    match self#get_selection with
214       Some node ->
215        let xpath =
216         ((node : Gdome.element)#getAttributeNS
217           ~namespaceURI:Misc.helm_ns
218           ~localName:(Gdome.domString "xref"))#to_string
219        in
220         if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
221         else
222          begin
223           match current_infos with
224              Some (ids_to_terms, ids_to_father_ids, _, _) ->
225               let id = xpath in
226                LogicalOperations.focus id ids_to_terms ids_to_father_ids
227            | None -> assert false (* "ERROR: No current term!!!" *)
228          end
229     | None -> assert false (* "ERROR: No selection!!!" *)
230
231   method load_proof currentproof =
232     let mml,
233          (acic,
234            (ids_to_terms,ids_to_father_ids,ids_to_conjectures,
235             ids_to_hypotheses,ids_to_inner_sorts,ids_to_inner_types)) =
236       mml_of_cic_object currentproof
237     in
238     current_infos <-
239       Some
240        (ids_to_terms,ids_to_father_ids,ids_to_conjectures,ids_to_hypotheses);
241     (* self#load_doc ~dom:mml ;
242        current_mml <- Some mml ; *)
243     ignore(Misc.domImpl#saveDocumentToFile ~name:"/tmp/prova" ~doc:mml ());
244     (match current_mml with
245       None ->
246         let time1 = Sys.time () in
247         self#load_root ~root:mml#get_documentElement ;
248         let time2 = Sys.time () in
249         debug_print ("Loading and displaying the proof took " ^
250           string_of_float (time2 -. time1) ^ "seconds") ;
251         current_mml <- Some mml
252     | Some current_mml' ->
253         self#freeze ;
254         let time1 = Sys.time () in
255         XmlDiff.update_dom ~from:current_mml' mml ;
256         let time2 = Sys.time () in
257         debug_print ("XMLDIFF took " ^
258           string_of_float (time2 -. time1) ^ "seconds") ;
259         self#thaw ;
260         let time3 = Sys.time () in
261         debug_print ("The refresh of the widget took " ^
262           string_of_float (time3 -. time2) ^ "seconds"));
263     (acic, ids_to_inner_types, ids_to_inner_sorts)
264   end
265 ;;
266
267
268 let proof_viewer ~(mml_of_cic_object: mml_of_cic_object)
269   ?hadjustment ?vadjustment ?font_size ?log_verbosity
270 =
271   GtkBase.Widget.size_params ~cont:(
272   OgtkMathViewProps.pack_return
273     (fun p ->
274       OgtkMathViewProps.set_params
275         (new proof_viewer ~mml_of_cic_object
276           (GtkMathViewProps.MathView_GMetaDOM.create p))
277         ~font_size ~log_verbosity)) []
278 ;;
279
280 (*
281 let proof_viewer ?adjustmenth ?adjustmentv ?font_size ?font_manager
282  ?border_width ?width ?height ?packing ?show () =
283  let w =
284    GtkMathView.MathView.create
285     ?adjustmenth:(Gaux.may_map ~f:GData.as_adjustment adjustmenth)
286     ?adjustmentv:(Gaux.may_map ~f:GData.as_adjustment adjustmentv)
287     ()
288  in
289   GtkBase.Container.set w ?border_width ?width ?height;
290  let mathview = GObj.pack_return (new proof_viewer w) ~packing ~show in
291  begin
292     match font_size with
293     | Some size -> mathview#set_font_size size
294     | None      -> ()
295   end;
296   begin
297     match font_manager with
298     | Some manager -> mathview#set_font_manager_type ~fm_type:manager
299     | None         -> ()
300   end;
301   mathview
302 ;;
303 *)
304