1 (* Copyright (C) 2000, HELM Team.
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.
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.
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.
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,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
26 (******************************************************************************)
30 (* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
33 (* This is a simple gtk interface to the Coq-like pretty printer cicPp for *)
34 (* cic terms exported in xml. It uses directly the modules cicPp and *)
35 (* cicCcache and indirectly all the other modules (cicParser, cicParser2, *)
36 (* cicParser3, getter). *)
37 (* The syntax is "gtkInterface[.opt] filename1 ... filenamen" where *)
38 (* filenamei is the path-name of an xml file describing a cic term. *)
39 (* The terms are loaded in cache and then pretty-printed one at a time and *)
40 (* only once, when the user wants to look at it: if the user wants to look at *)
41 (* a term again, then the pretty-printed term is showed again, but not *)
44 (******************************************************************************)
46 (* DEFINITION OF THE URI TREE AND USEFUL FUNCTIONS ON IT *)
49 Dir of string * item list ref
50 | File of string * UriManager.uri
54 let theoryuritree = ref []
59 | File (name,_) -> name
65 | File (_,uri) -> Some uri
68 (* STUFF TO BUILD THE URI TREE *)
71 exception DuplicatedUri
72 exception ConflictingUris
74 let insert_in_uri_tree uri =
79 let _ = List.find (fun item -> name = get_name item) !l in
82 Not_found -> l := (File (name,uri))::!l
86 match List.find (fun item -> name = get_name item) !l with
87 Dir (_,children) -> aux children tl
88 | File _ -> raise ConflictingUris
91 let children = ref [] in
92 l := (Dir (name,children))::!l ;
95 | [] -> raise EmptyUri
100 (* Imperative procedure that builds the two uri trees *)
101 let build_uri_tree () =
102 let dbh = Dbm.opendbm Configuration.uris_dbm [Dbm.Dbm_rdonly] 0 in
105 let cicregexp = Str.regexp "cic:"
106 and theoryregexp = Str.regexp "theory:" in
107 if Str.string_match cicregexp uri 0 then
108 let s = Str.replace_first cicregexp "" uri in
109 let l = Str.split (Str.regexp "/") s in
110 insert_in_uri_tree (UriManager.uri_of_string uri) uritree l
111 else if Str.string_match theoryregexp uri 0 then
112 let s = Str.replace_first theoryregexp "" uri in
113 let l = Str.split (Str.regexp "/") s in
114 insert_in_uri_tree (UriManager.uri_of_string uri) theoryuritree l
119 (* GLOBAL REFERENCES (USED BY CALLBACKS) *)
121 let annotated_obj = ref None;; (* reference to a couple option where *)
122 (* the first component is the current *)
123 (* annotated object and the second is *)
124 (* the map from ids to annotated targets *)
125 let ann = ref (ref None);; (* current annotation *)
126 let radio_some_status = ref false;; (* is the radio_some button selected? *)
128 let theory_visited_uris = ref [];;
129 let theory_to_visit_uris = ref [];;
130 let visited_uris = ref [];;
131 let to_visit_uris = ref [];;
135 exception NoCurrentUri;;
136 exception NoNextOrPrevUri;;
138 let theory_get_current_uri () =
139 match !theory_visited_uris with
140 [] -> raise NoCurrentUri
144 let get_current_uri () =
145 match !visited_uris with
146 [] -> raise NoCurrentUri
150 let get_annotated_obj () =
151 match !annotated_obj with
153 let (annobj, ids_to_targets,_) =
154 (CicCache.get_annobj (get_current_uri ()))
156 annotated_obj := Some (annobj, ids_to_targets) ;
157 (annobj, ids_to_targets)
158 | Some annobj -> annobj
161 let filename_of_uri uri =
165 let theory_update_output rendering_window uri =
166 rendering_window#label#set_text (UriManager.string_of_uri uri) ;
167 ignore (rendering_window#errors#delete_text 0 rendering_window#errors#length) ;
168 let mmlfile = XsltProcessor.process uri true "theory" in
169 rendering_window#output#load mmlfile
172 let update_output rendering_window uri =
173 rendering_window#label#set_text (UriManager.string_of_uri uri) ;
174 ignore (rendering_window#errors#delete_text 0 rendering_window#errors#length) ;
175 let mmlfile = XsltProcessor.process uri true "cic" in
176 rendering_window#output#load mmlfile
179 let theory_next rendering_window () =
180 match !theory_to_visit_uris with
181 [] -> raise NoNextOrPrevUri
183 theory_to_visit_uris := tl ;
184 theory_visited_uris := uri::!theory_visited_uris ;
185 theory_update_output rendering_window uri ;
186 rendering_window#prevb#misc#set_sensitive true ;
188 rendering_window#nextb#misc#set_sensitive false
191 let next rendering_window () =
192 match !to_visit_uris with
193 [] -> raise NoNextOrPrevUri
195 to_visit_uris := tl ;
196 visited_uris := uri::!visited_uris ;
197 annotated_obj := None ;
198 update_output rendering_window uri ;
199 rendering_window#prevb#misc#set_sensitive true ;
201 rendering_window#nextb#misc#set_sensitive false
204 let theory_prev rendering_window () =
205 match !theory_visited_uris with
206 [] -> raise NoCurrentUri
207 | [_] -> raise NoNextOrPrevUri
208 | uri::(uri'::tl as newvu) ->
209 theory_visited_uris := newvu ;
210 theory_to_visit_uris := uri::!theory_to_visit_uris ;
211 theory_update_output rendering_window uri' ;
212 rendering_window#nextb#misc#set_sensitive true ;
214 rendering_window#prevb#misc#set_sensitive false
217 let prev rendering_window () =
218 match !visited_uris with
219 [] -> raise NoCurrentUri
220 | [_] -> raise NoNextOrPrevUri
221 | uri::(uri'::tl as newvu) ->
222 visited_uris := newvu ;
223 to_visit_uris := uri::!to_visit_uris ;
224 annotated_obj := None ;
225 update_output rendering_window uri' ;
226 rendering_window#nextb#misc#set_sensitive true ;
228 rendering_window#prevb#misc#set_sensitive false
231 (* called when an hyperlink is clicked *)
232 let jump rendering_window (node : Ominidom.o_mDOMNode) =
233 let module O = Ominidom in
234 match (node#get_attribute (O.o_mDOMString_of_string "href")) with
236 let s = str#get_string in
237 let uri = UriManager.uri_of_string s in
238 rendering_window#show () ;
239 rendering_window#prevb#misc#set_sensitive true ;
240 rendering_window#nextb#misc#set_sensitive false ;
241 visited_uris := uri::!visited_uris ;
242 to_visit_uris := [] ;
243 annotated_obj := None ;
244 update_output rendering_window uri
245 | None -> assert false
248 let choose_selection rendering_window (node : Ominidom.o_mDOMNode option) =
249 let module O = Ominidom in
251 match node#get_attribute (O.o_mDOMString_of_string "xref") with
252 Some _ -> rendering_window#output#set_selection (Some node)
253 | None -> aux (node#get_parent)
257 | None -> rendering_window#output#set_selection None
261 let theory_selection_changed rendering_window uri () =
265 if !theory_visited_uris <> [] then
266 rendering_window#prevb#misc#set_sensitive true ;
267 rendering_window#nextb#misc#set_sensitive false ;
268 theory_visited_uris := uri'::!theory_visited_uris ;
269 theory_to_visit_uris := [] ;
270 rendering_window#show () ;
271 theory_update_output rendering_window uri'
274 let selection_changed rendering_window uri () =
278 if !visited_uris <> [] then
279 rendering_window#prevb#misc#set_sensitive true ;
280 rendering_window#nextb#misc#set_sensitive false ;
281 visited_uris := uri'::!visited_uris ;
282 to_visit_uris := [] ;
283 annotated_obj := None ;
284 rendering_window#show () ;
285 update_output rendering_window uri'
288 let create_gtk_trees (hbox : GPack.box) rendering_window theory_rendering_window mktree =
290 GBin.scrolled_window ~width:250 ~height:600
291 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
293 GTree.tree ~selection_mode:`BROWSE ~packing:sw3#add_with_viewport () in
294 let tree_item1 = GTree.tree_item ~label:"theory:/" ~packing:tree1#append () in
297 GBin.scrolled_window ~width:250 ~height:600
298 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
300 GTree.tree ~selection_mode:`BROWSE ~packing:sw2#add_with_viewport () in
301 let tree_item = GTree.tree_item ~label:"cic:/" ~packing:tree#append () in
303 ignore(tree_item#connect#select (selection_changed rendering_window None)) ;
304 mktree selection_changed rendering_window tree_item (Dir ("cic:/",uritree)) ;
306 ignore(tree_item1#connect#select
307 (theory_selection_changed theory_rendering_window None)) ;
308 mktree theory_selection_changed theory_rendering_window tree_item1
309 (Dir ("theory:/",theoryuritree)) ;
313 let updateb_pressed theory_rendering_window rendering_window
314 (sw1, sw ,(hbox : GPack.box)) mktree ()
317 (* let's empty the uri trees and rebuild them *)
319 theoryuritree := [] ;
321 hbox#remove !sw1#coerce ;
322 hbox#remove !sw#coerce ;
324 create_gtk_trees hbox rendering_window theory_rendering_window mktree
330 let theory_check rendering_window () =
333 TheoryTypeChecker.typecheck (theory_get_current_uri ());
334 "Type Checking was successful"
336 TheoryTypeChecker.NotWellTyped s ->
337 "Type Checking was NOT successful:\n\t" ^ s
339 (* next "cast" can't got rid of, but I don't know why *)
340 let errors = (rendering_window#errors : GEdit.text) in
341 let _ = errors#delete_text 0 errors#length in
345 let check rendering_window () =
348 CicTypeChecker.typecheck (get_current_uri ());
349 "Type Checking was successful"
351 CicTypeChecker.NotWellTyped s -> "Type Checking was NOT successful:\n\t" ^ s
353 (* next "cast" can't got rid of, but I don't know why *)
354 let errors = (rendering_window#errors : GEdit.text) in
355 let _ = errors#delete_text 0 errors#length in
359 let annotateb_pressed rendering_window annotation_window () =
360 let module O = Ominidom in
361 match rendering_window#output#get_selection with
364 match (node#get_attribute (O.o_mDOMString_of_string "xref")) with
366 let annobj = get_annotated_obj ()
367 (* next "cast" can't got rid of, but I don't know why *)
368 and annotation = (annotation_window#annotation : GEdit.text) in
369 ann := CicXPath.get_annotation annobj (xpath#get_string) ;
370 CicAnnotationHinter.create_hints annotation_window annobj (xpath#get_string) ;
371 annotation#delete_text 0 annotation#length ;
375 annotation#misc#set_sensitive false ;
376 annotation_window#radio_none#set_active true ;
377 radio_some_status := false
379 annotation#insert ann' ;
380 annotation#misc#set_sensitive true ;
381 annotation_window#radio_some#set_active true ;
382 radio_some_status := true
384 GMain.Grab.add (annotation_window#window_to_annotate#coerce) ;
385 annotation_window#show () ;
387 (* next "cast" can't got rid of, but I don't know why *)
388 let errors = (rendering_window#errors : GEdit.text) in
389 errors#insert ("\nNo xref found\n")
391 | None -> (rendering_window#errors : GEdit.text)#insert "\nNo selection!\n"
394 (* called when the annotation is confirmed *)
395 let save_annotation annotation =
396 if !radio_some_status then
397 !ann := Some (annotation#get_chars 0 annotation#length)
400 match !annotated_obj with
403 let uri = get_current_uri () in
404 let annxml = Annotation2Xml.pp_annotation annobj uri in
405 Xml.pp annxml (Some (fst (Getter.get_ann_file_name_and_uri uri)))
408 let parse_no_cache uri =
409 let module U = UriManager in
410 XsltProcessor.process uri false "cic"
414 (* STUFF TO BUILD THE GTK INTERFACE *)
416 (* Stuff to build the tree window *)
418 (* selection_changed is actually selection_changed or theory_selection_changed*)
419 let mktree selection_changed rendering_window =
420 let rec aux treeitem =
422 Dir (dirname, content) ->
423 let subtree = GTree.tree () in
424 treeitem#set_subtree subtree ;
428 let label = get_name ti
429 and uri = get_uri ti in
430 let treeitem2 = GTree.tree_item ~label:label () in
431 subtree#append treeitem2 ;
432 ignore(treeitem2#connect#select
433 (selection_changed rendering_window uri)) ;
434 (* Almost lazy function *)
435 (fun () -> aux treeitem2 ti)
436 ) (List.sort compare !content)
438 let lazy_expand_sons = lazy (List.iter (fun f -> f ()) expand_sons) in
439 ignore(treeitem#connect#expand
440 (fun () -> Lazy.force lazy_expand_sons)) ;
446 (* Stuff for the widget settings *)
448 let export_to_postscript (output : GMathView.math_view) () =
449 output#export_to_postscript ~filename:"output.ps" ();
452 let activate_t1 output button_set_anti_aliasing button_set_kerning
453 button_export_to_postscript button_t1 ()
455 let is_set = button_t1#active in
456 output#set_font_manager_type
457 (if is_set then `font_manager_t1 else `font_manager_gtk) ;
460 button_set_anti_aliasing#misc#set_sensitive true ;
461 button_set_kerning#misc#set_sensitive true ;
462 button_export_to_postscript#misc#set_sensitive true ;
466 button_set_anti_aliasing#misc#set_sensitive false ;
467 button_set_kerning#misc#set_sensitive false ;
468 button_export_to_postscript#misc#set_sensitive false ;
472 let set_anti_aliasing output button_set_anti_aliasing () =
473 output#set_anti_aliasing button_set_anti_aliasing#active
476 let set_kerning output button_set_kerning () =
477 output#set_kerning button_set_kerning#active
480 let changefont output font_size_spinb () =
481 output#set_font_size font_size_spinb#value_as_int
484 let set_log_verbosity output log_verbosity_spinb () =
485 output#set_log_verbosity log_verbosity_spinb#value_as_int
488 class settings_window output sw button_export_to_postscript jump_callback
489 selection_changed_callback
491 let settings_window = GWindow.window ~title:"GtkMathView settings" () in
493 GPack.vbox ~packing:settings_window#add () in
496 ~rows:1 ~columns:3 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
497 ~border_width:5 ~packing:vbox#add () in
499 GButton.toggle_button ~label:"activate t1 fonts"
500 ~packing:(table#attach ~left:0 ~top:0) () in
501 let button_set_anti_aliasing =
502 GButton.toggle_button ~label:"set_anti_aliasing"
503 ~packing:(table#attach ~left:1 ~top:0) () in
504 let button_set_kerning =
505 GButton.toggle_button ~label:"set_kerning"
506 ~packing:(table#attach ~left:2 ~top:0) () in
509 ~rows:2 ~columns:2 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
510 ~border_width:5 ~packing:vbox#add () in
511 let font_size_label =
512 GMisc.label ~text:"font size:"
513 ~packing:(table#attach ~left:0 ~top:0 ~expand:`NONE) () in
514 let font_size_spinb =
516 GData.adjustment ~value:14.0 ~lower:5.0 ~upper:50.0 ~step_incr:1.0 ()
519 ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:0 ~fill:`NONE) () in
520 let log_verbosity_label =
521 GMisc.label ~text:"log verbosity:"
522 ~packing:(table#attach ~left:0 ~top:1) () in
523 let log_verbosity_spinb =
525 GData.adjustment ~value:0.0 ~lower:0.0 ~upper:3.0 ~step_incr:1.0 ()
528 ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:1) () in
530 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
532 GButton.button ~label:"Close"
533 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
535 method show = settings_window#show
537 button_set_anti_aliasing#misc#set_sensitive false ;
538 button_set_kerning#misc#set_sensitive false ;
539 (* Signals connection *)
540 ignore(button_t1#connect#clicked
541 (activate_t1 output button_set_anti_aliasing button_set_kerning
542 button_export_to_postscript button_t1)) ;
543 ignore(font_size_spinb#connect#changed (changefont output font_size_spinb)) ;
544 ignore(button_set_anti_aliasing#connect#toggled
545 (set_anti_aliasing output button_set_anti_aliasing));
546 ignore(button_set_kerning#connect#toggled
547 (set_kerning output button_set_kerning)) ;
548 ignore(log_verbosity_spinb#connect#changed
549 (set_log_verbosity output log_verbosity_spinb)) ;
550 ignore(closeb#connect#clicked settings_window#misc#hide)
555 class annotation_window output label =
556 let window_to_annotate =
557 GWindow.window ~title:"Annotating environment" ~border_width:2 () in
559 GPack.hbox ~packing:window_to_annotate#add () in
561 GPack.vbox ~packing:(hbox1#pack ~padding:5) () in
563 GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
564 let radio_some = GButton.radio_button ~label:"Annotation below"
565 ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
566 let radio_none = GButton.radio_button ~label:"No annotation"
567 ~group:radio_some#group
568 ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5)
570 let annotation = GEdit.text ~editable:true ~width:400 ~height:180
571 ~packing:(vbox1#pack ~padding:5) () in
573 GPack.table ~rows:3 ~columns:3 ~packing:(vbox1#pack ~padding:5) () in
574 let annotation_hints =
577 GButton.button ~label:("Hint " ^ string_of_int i)
578 ~packing:(table#attach ~left:(i mod 3) ~top:(i / 3)) ()
581 GPack.vbox ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
583 GButton.button ~label:"O.K."
584 ~packing:(vbox2#pack ~expand:false ~fill:false ~padding:5) () in
586 GButton.button ~label:"Abort"
587 ~packing:(vbox2#pack ~expand:false ~fill:false ~padding:5) () in
589 method window_to_annotate = window_to_annotate
590 method annotation = annotation
591 method radio_some = radio_some
592 method radio_none = radio_none
593 method annotation_hints = annotation_hints
594 method output = (output : GMathView.math_view)
595 method show () = window_to_annotate#show ()
597 (* signal handlers here *)
598 ignore (window_to_annotate#event#connect#delete
600 window_to_annotate#misc#hide () ;
601 GMain.Grab.remove (window_to_annotate#coerce) ;
604 ignore (confirmb#connect#clicked
606 window_to_annotate#misc#hide () ;
607 save_annotation annotation ;
608 GMain.Grab.remove (window_to_annotate#coerce) ;
609 let new_current_uri =
610 (snd (Getter.get_ann_file_name_and_uri (get_current_uri ())))
612 visited_uris := new_current_uri::(List.tl !visited_uris) ;
613 label#set_text (UriManager.string_of_uri new_current_uri) ;
614 let mmlfile = parse_no_cache new_current_uri in
617 ignore (abortb#connect#clicked
619 window_to_annotate#misc#hide () ;
620 GMain.Grab.remove (window_to_annotate#coerce)
622 ignore (radio_some#connect#clicked
623 (fun () -> annotation#misc#set_sensitive true ; radio_some_status := true)) ;
624 ignore (radio_none #connect#clicked
626 annotation#misc#set_sensitive false;
627 radio_some_status := false)
631 class rendering_window annotation_window output (label : GMisc.label) =
633 GWindow.window ~title:"MathML viewer" ~border_width:2 () in
635 GPack.vbox ~packing:window#add () in
636 let _ = vbox#pack ~expand:false ~fill:false ~padding:5 label#coerce in
638 GPack.paned `HORIZONTAL ~packing:(vbox#pack ~expand:true ~padding:5) () in
639 let scrolled_window0 =
640 GBin.scrolled_window ~border_width:10 ~packing:paned#add1 () in
641 let _ = scrolled_window0#add output#coerce in
642 let scrolled_window =
644 ~border_width:10 ~packing:paned#add2 ~width:240 ~height:100 () in
645 let errors = GEdit.text ~packing:scrolled_window#add_with_viewport () in
647 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
649 GButton.button ~label:"Prev"
650 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
652 GButton.button ~label:"Next"
653 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
655 GButton.button ~label:"Check"
656 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
658 GButton.button ~label:"Annotate"
659 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
661 GButton.button ~label:"Settings"
662 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
663 let button_export_to_postscript =
664 GButton.button ~label:"export_to_postscript"
665 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
667 GButton.button ~label:"Close"
668 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
673 method output = (output : GMathView.math_view)
674 method errors = errors
675 method show () = window#show ()
677 nextb#misc#set_sensitive false ;
678 prevb#misc#set_sensitive false ;
679 button_export_to_postscript#misc#set_sensitive false ;
681 (* signal handlers here *)
682 ignore(output#connect#jump (jump self)) ;
683 ignore(output#connect#selection_changed (choose_selection self)) ;
684 ignore(nextb#connect#clicked (next self)) ;
685 ignore(prevb#connect#clicked (prev self)) ;
686 (* LUCA: check disabled while compression is not fully implemented *)
687 (* ignore(checkb#connect#clicked (check self)) ; *)
688 checkb#misc#set_sensitive false ;
689 ignore(closeb#connect#clicked window#misc#hide) ;
690 ignore(annotateb#connect#clicked (annotateb_pressed self annotation_window)) ;
691 let settings_window = new settings_window output scrolled_window0
692 button_export_to_postscript (jump self) (choose_selection self) in
693 ignore(settingsb#connect#clicked settings_window#show) ;
694 ignore(button_export_to_postscript#connect#clicked (export_to_postscript output)) ;
695 ignore(window#event#connect#delete (fun _ -> window#misc#hide () ; true ))
698 class theory_rendering_window rendering_window =
700 GWindow.window ~title:"MathML theory viewer" ~border_width:2 () in
702 GPack.vbox ~packing:window#add () in
704 GMisc.label ~text:"???"
705 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
707 GPack.paned `HORIZONTAL ~packing:(vbox#pack ~expand:true ~padding:5) () in
708 let scrolled_window0 =
709 GBin.scrolled_window ~border_width:10 ~packing:paned#add1 () in
711 GMathView.math_view ~width:400 ~height:380 ~packing:scrolled_window0#add () in
712 let scrolled_window =
714 ~border_width:10 ~packing:paned#add2 ~width:240 ~height:100 () in
715 let errors = GEdit.text ~packing:scrolled_window#add_with_viewport () in
717 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
719 GButton.button ~label:"Prev"
720 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
722 GButton.button ~label:"Next"
723 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
725 GButton.button ~label:"Check"
726 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
728 GButton.button ~label:"Settings"
729 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
730 let button_export_to_postscript =
731 GButton.button ~label:"export_to_postscript"
732 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
734 GButton.button ~label:"Close"
735 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
740 method output = (output : GMathView.math_view)
741 method errors = errors
742 method show () = window#show ()
744 nextb#misc#set_sensitive false ;
745 prevb#misc#set_sensitive false ;
746 button_export_to_postscript#misc#set_sensitive false ;
748 (* signal handlers here *)
749 ignore(output#connect#jump (jump rendering_window)) ;
750 ignore(output#connect#selection_changed (choose_selection self)) ;
751 ignore(nextb#connect#clicked (theory_next self)) ;
752 ignore(prevb#connect#clicked (theory_prev self)) ;
753 ignore(checkb#connect#clicked (theory_check self)) ;
754 let settings_window = new settings_window output scrolled_window0
755 button_export_to_postscript (jump rendering_window)(choose_selection self) in
756 ignore(settingsb#connect#clicked settings_window#show) ;
757 ignore(button_export_to_postscript#connect#clicked (export_to_postscript output)) ;
758 ignore(closeb#connect#clicked window#misc#hide) ;
759 ignore(window#event#connect#delete (fun _ -> window#misc#hide () ; true ))
762 (* CSC: fare in modo che i due alberi vengano svuotati invece che distrutti *)
763 class selection_window theory_rendering_window rendering_window =
764 let label = "cic:/" in
765 let theorylabel = "theory:/" in
766 let win = GWindow.window ~title:"Known uris" ~border_width:2 () in
767 let vbox = GPack.vbox ~packing:win#add () in
768 let hbox1 = GPack.hbox ~packing:(vbox#pack ~padding:5) () in
770 create_gtk_trees hbox1 rendering_window theory_rendering_window mktree
773 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
775 GButton.button ~label:"Update"
776 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
778 GButton.button ~label:"Quit"
779 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
781 method show () = win#show ()
783 (* signal handlers here *)
784 ignore (win#connect#destroy ~callback:GMain.Main.quit) ;
785 ignore (quitb#connect#clicked GMain.Main.quit) ;
786 ignore(updateb#connect#clicked (updateb_pressed
787 theory_rendering_window rendering_window (ref sw1, ref sw, hbox1) mktree))
795 let output = GMathView.math_view ~width:400 ~height:380 ()
796 and label = GMisc.label ~text:"???" () in
797 let annotation_window = new annotation_window output label in
798 let rendering_window = new rendering_window annotation_window output label in
799 let theory_rendering_window = new theory_rendering_window rendering_window in
800 let selection_window =
801 new selection_window theory_rendering_window rendering_window
803 selection_window#show () ;