]> matita.cs.unibo.it Git - helm.git/blob - helm/gTopLevel/termViewer.ml
d5950a1c9043cdd3985d3963e2b980f58e7c515c
[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 (*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
31 (*                                 29/01/2003                                 *)
32 (*                                                                            *)
33 (*                                                                            *)
34 (******************************************************************************)
35
36 let use_stylesheets = ref true;;(* false performs the transformations in OCaml*)
37
38 (* List utility functions *)
39 exception Skip;;
40
41 let list_map_fail f =
42  let rec aux =
43   function
44      [] -> []
45    | he::tl ->
46       try
47        let he' = f he in
48         he'::(aux tl)
49       with Skip ->
50        (aux tl)
51  in
52   aux
53 ;;
54 (* End of the list utility functions *)
55
56 (** A widget to render sequents **)
57
58 class sequent_viewer obj =
59  object(self)
60
61   inherit GMathViewAux.multi_selection_math_view obj
62
63   val mutable current_infos = None
64
65   (* returns the list of selected terms         *)
66   (* selections which are not terms are ignored *)
67   method get_selected_terms =
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         if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
77         else
78          match current_infos with
79             Some (ids_to_terms,_,_) ->
80              let id = xpath in
81               (try
82                 Hashtbl.find ids_to_terms id
83                with _ -> raise Skip)
84           | None -> assert false (* "ERROR: No current term!!!" *)
85      ) selections
86
87   (* returns the list of selected hypotheses         *)
88   (* selections which are not hypotheses are ignored *)
89   method get_selected_hypotheses =
90    let selections = self#get_selections in
91     list_map_fail
92      (function node ->
93        let xpath =
94         ((node : Gdome.element)#getAttributeNS
95           ~namespaceURI:Misc.helmns
96           ~localName:(Gdome.domString "xref"))#to_string
97        in
98         if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
99         else
100          match current_infos with
101             Some (_,_,ids_to_hypotheses) ->
102              let id = xpath in
103               (try
104                 Hashtbl.find ids_to_hypotheses id
105                with _ -> raise Skip)
106           | None -> assert false (* "ERROR: No current term!!!" *)
107      ) selections
108   
109   method load_sequent metasenv sequent =
110    let sequent_mml,(ids_to_terms,ids_to_father_ids,ids_to_hypotheses) =
111     ApplyStylesheets.mml_of_cic_sequent metasenv sequent
112    in
113     self#load_doc ~dom:sequent_mml ;
114     current_infos <-
115      Some (ids_to_terms,ids_to_father_ids,ids_to_hypotheses)
116  end
117 ;;
118
119 let sequent_viewer ?adjustmenth ?adjustmentv ?font_size ?font_manager
120  ?border_width ?width ?height ?packing ?show () =
121  let w =
122    GtkMathView.MathView.create
123     ?adjustmenth:(Gaux.may_map ~f:GData.as_adjustment adjustmenth)
124     ?adjustmentv:(Gaux.may_map ~f:GData.as_adjustment adjustmentv)
125     ()
126  in
127   GtkBase.Container.set w ?border_width ?width ?height;
128  let mathview = GObj.pack_return (new sequent_viewer w) ~packing ~show in
129  begin
130     match font_size with
131     | Some size -> mathview#set_font_size size
132     | None      -> ()
133   end;
134   begin
135     match font_manager with
136     | Some manager -> mathview#set_font_manager_type ~fm_type:manager
137     | None         -> ()
138   end;
139   mathview
140 ;;
141
142
143 (** A widget to render proofs **)
144
145 class proof_viewer obj =
146  object(self)
147
148   inherit GMathViewAux.single_selection_math_view obj
149
150   initializer self#set_font_size 10
151
152   val mutable current_infos = None
153   val mutable current_mml = None
154
155   method make_sequent_of_selected_term =
156    match self#get_selection with
157       Some node ->
158        let xpath =
159         ((node : Gdome.element)#getAttributeNS
160           ~namespaceURI:Misc.helmns
161           ~localName:(Gdome.domString "xref"))#to_string
162        in
163         if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
164         else
165          begin
166           match current_infos with
167              Some (ids_to_terms, ids_to_father_ids, _, _) ->
168               let id = xpath in
169                LogicalOperations.to_sequent id ids_to_terms ids_to_father_ids
170            | None -> assert false (* "ERROR: No current term!!!" *)
171          end
172     | None -> assert false (* "ERROR: No selection!!!" *)
173
174   method focus_sequent_of_selected_term =
175    match self#get_selection with
176       Some node ->
177        let xpath =
178         ((node : Gdome.element)#getAttributeNS
179           ~namespaceURI:Misc.helmns
180           ~localName:(Gdome.domString "xref"))#to_string
181        in
182         if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
183         else
184          begin
185           match current_infos with
186              Some (ids_to_terms, ids_to_father_ids, _, _) ->
187               let id = xpath in
188                LogicalOperations.focus id ids_to_terms ids_to_father_ids
189            | None -> assert false (* "ERROR: No current term!!!" *)
190          end
191     | None -> assert false (* "ERROR: No selection!!!" *)
192
193   method load_omdoc_proof uri ~ids_to_inner_sorts cobj =
194    if !use_stylesheets then
195     let
196      (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
197       ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
198     =
199      Cic2acic.acic_object_of_cic_object (Content2cic.cobj2obj cobj)
200     in
201 prerr_endline "0000000000000000 USO GLI STYLESHEETS" ;
202      let mml =
203       ApplyStylesheets.mml_of_cic_object
204        ~explode_all:true uri acic ids_to_inner_sorts ids_to_inner_types
205      in
206       (match current_mml with
207           None ->
208 prerr_endline "0000000000000000 CARICO L'mml PRODOTTO" ;
209            self#load_doc ~dom:mml ;
210            current_mml <- Some mml
211         | Some current_mml ->
212            self#freeze ;
213            XmlDiff.update_dom ~from:current_mml mml ;
214            self#thaw) ;
215 (*
216       self#load_doc ~dom:mml ;
217       current_mml <- Some mml ;
218 *)
219       current_infos <-
220        Some
221         (ids_to_terms,ids_to_father_ids,ids_to_conjectures,ids_to_hypotheses) ;
222    else
223     let pres = Content2pres.content2pres ~ids_to_inner_sorts cobj in
224     let time2 = Sys.time () in
225     (* prerr_endline ("Fine trasformazione:" ^ (string_of_float (time2 -. time1))); *)
226     let xmlpres = Mpresentation.print_mpres pres in
227     let time25 = Sys.time () in
228 prerr_endline "(******** INIZIO CONTENT ==> PRES **********)";
229      (*
230      prerr_endline ("FINE printing to stream:" ^ (string_of_float (time25 -. time2)));
231      Xml.pp xmlpres (Some "tmp");
232      let time3 = Sys.time () in
233       prerr_endline ("FINE valutazione e printing dello stream:" ^ (string_of_float (time3 -. time25)));
234      *)
235     (try 
236       prerr_endline "(******** INIZIO DOM **********)";
237       let mml = Xml2Gdome.document_of_xml Misc.domImpl xmlpres in
238       let time3 = Sys.time () in
239       (* ignore (Misc.domImpl#saveDocumentToFile mml "tmp1" ()); *)
240       prerr_endline "(******** FINE DOM **********)";
241       (match current_mml with
242           None ->
243            self#load_doc ~dom:mml ;
244            current_mml <- Some mml
245         | Some current_mml ->
246            self#freeze ;
247 prerr_endline "XML_DIFF: prima passata";
248 (*
249 ignore (Misc.domImpl#saveDocumentToFile current_mml "/tmp/current_mml_1.xml" ()) ;
250 ignore (Misc.domImpl#saveDocumentToFile mml "/tmp/mml_1.xml" ()) ;
251 *)
252            XmlDiff.update_dom ~from:current_mml mml ;
253 (*
254 prerr_endline "XML_DIFF: seconda passata";
255 ignore (Misc.domImpl#saveDocumentToFile current_mml "/tmp/current_mml_2.xml" ()) ;
256 ignore (Misc.domImpl#saveDocumentToFile mml "/tmp/mml_2.xml" ()) ;
257            XmlDiff.update_dom ~from:current_mml mml ;
258 ignore (Misc.domImpl#saveDocumentToFile current_mml "/tmp/current_mml_3.xml" ()) ;
259 ignore (Misc.domImpl#saveDocumentToFile mml "/tmp/mml_3.xml" ()) ;
260 *)
261 prerr_endline "XML_DIFF: fine passate";
262            self#thaw) ;
263 (*
264       self#load_doc ~dom:mml;
265 *)
266       prerr_endline ("Fine loading:" ^ (string_of_float (time3 -. time2)))
267      (*
268       self#load_uri "tmp";
269       let time4 = Sys.time () in
270       prerr_endline
271        ("Fine loading:" ^ (string_of_float (time4 -. time3)))
272      *)
273     with (GdomeInit.DOMException (_,s)) as e ->
274        prerr_endline s; raise e)
275
276   method load_proof uri currentproof =
277    let
278     (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
279      ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
280    =
281     Cic2acic.acic_object_of_cic_object currentproof
282    in
283     let mml =
284      ApplyStylesheets.mml_of_cic_object
285       ~explode_all:true uri acic ids_to_inner_sorts ids_to_inner_types
286     in
287      self#load_doc ~dom:mml ;
288      current_mml <- Some mml ;
289      current_infos <-
290       Some
291        (ids_to_terms,ids_to_father_ids,ids_to_conjectures,ids_to_hypotheses) ;
292     (acic, ids_to_inner_types, ids_to_inner_sorts)
293  end
294 ;;
295
296 let proof_viewer ?adjustmenth ?adjustmentv ?font_size ?font_manager
297  ?border_width ?width ?height ?packing ?show () =
298  let w =
299    GtkMathView.MathView.create
300     ?adjustmenth:(Gaux.may_map ~f:GData.as_adjustment adjustmenth)
301     ?adjustmentv:(Gaux.may_map ~f:GData.as_adjustment adjustmentv)
302     ()
303  in
304   GtkBase.Container.set w ?border_width ?width ?height;
305  let mathview = GObj.pack_return (new proof_viewer w) ~packing ~show in
306  begin
307     match font_size with
308     | Some size -> mathview#set_font_size size
309     | None      -> ()
310   end;
311   begin
312     match font_manager with
313     | Some manager -> mathview#set_font_manager_type ~fm_type:manager
314     | None         -> ()
315   end;
316   mathview
317 ;;
318
319 let _ =
320  Cexpr2pres_hashtbl.init Cexpr2pres.cexpr2pres Cexpr2pres.cexpr2pres_charcount
321 ;;