1 (******************************************************************************)
5 (* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
8 (* This is a simple gtk interface to the Coq-like pretty printer cicPp for *)
9 (* cic terms exported in xml. It uses directly the modules cicPp and *)
10 (* cicCcache and indirectly all the other modules (cicParser, cicParser2, *)
11 (* cicParser3, getter). *)
12 (* The syntax is "gtkInterface[.opt] filename1 ... filenamen" where *)
13 (* filenamei is the path-name of an xml file describing a cic term. *)
14 (* The terms are loaded in cache and then pretty-printed one at a time and *)
15 (* only once, when the user wants to look at it: if the user wants to look at *)
16 (* a term again, then the pretty-printed term is showed again, but not *)
19 (******************************************************************************)
21 (* DEFINITION OF THE URI TREE AND USEFUL FUNCTIONS ON IT *)
24 Dir of string * item list ref
25 | File of string * UriManager.uri
29 let theoryuritree = ref []
34 | File (name,_) -> name
40 | File (_,uri) -> Some uri
43 (* STUFF TO BUILD THE URI TREE *)
46 exception DuplicatedUri
47 exception ConflictingUris
49 let insert_in_uri_tree uri =
54 let _ = List.find (fun item -> name = get_name item) !l in
57 Not_found -> l := (File (name,uri))::!l
61 match List.find (fun item -> name = get_name item) !l with
62 Dir (_,children) -> aux children tl
63 | File _ -> raise ConflictingUris
66 let children = ref [] in
67 l := (Dir (name,children))::!l ;
70 | [] -> raise EmptyUri
75 (* Imperative procedure that builds the two uri trees *)
76 let build_uri_tree () =
77 let dbh = Dbm.opendbm Configuration.uris_dbm [Dbm.Dbm_rdonly] 0 in
80 let cicregexp = Str.regexp "cic:"
81 and theoryregexp = Str.regexp "theory:" in
82 if Str.string_match cicregexp uri 0 then
83 let s = Str.replace_first cicregexp "" uri in
84 let l = Str.split (Str.regexp "/") s in
85 insert_in_uri_tree (UriManager.uri_of_string uri) uritree l
86 else if Str.string_match theoryregexp uri 0 then
87 let s = Str.replace_first theoryregexp "" uri in
88 let l = Str.split (Str.regexp "/") s in
89 insert_in_uri_tree (UriManager.uri_of_string uri) theoryuritree l
94 (* GLOBAL REFERENCES (USED BY CALLBACKS) *)
96 let annotated_obj = ref None;; (* reference to a couple option where *)
97 (* the first component is the current *)
98 (* annotated object and the second is *)
99 (* the map from ids to annotated targets *)
100 let ann = ref (ref None);; (* current annotation *)
101 let radio_some_status = ref false;; (* is the radio_some button selected? *)
103 let theory_visited_uris = ref [];;
104 let theory_to_visit_uris = ref [];;
105 let visited_uris = ref [];;
106 let to_visit_uris = ref [];;
110 exception NoCurrentUri;;
111 exception NoNextOrPrevUri;;
113 let theory_get_current_uri () =
114 match !theory_visited_uris with
115 [] -> raise NoCurrentUri
119 let get_current_uri () =
120 match !visited_uris with
121 [] -> raise NoCurrentUri
125 let get_annotated_obj () =
126 match !annotated_obj with
128 let (annobj, ids_to_targets,_) =
129 (CicCache.get_annobj (get_current_uri ()))
131 annotated_obj := Some (annobj, ids_to_targets) ;
132 (annobj, ids_to_targets)
133 | Some annobj -> annobj
136 let filename_of_uri uri =
140 let theory_update_output rendering_window uri =
141 rendering_window#label#set_text (UriManager.string_of_uri uri) ;
142 ignore (rendering_window#errors#delete_text 0 rendering_window#errors#length) ;
143 let mmlfile = XsltProcessor.process uri true "theory" in
144 rendering_window#output#load mmlfile
147 let update_output rendering_window uri =
148 rendering_window#label#set_text (UriManager.string_of_uri uri) ;
149 ignore (rendering_window#errors#delete_text 0 rendering_window#errors#length) ;
150 let mmlfile = XsltProcessor.process uri true "cic" in
151 rendering_window#output#load mmlfile
154 let theory_next rendering_window () =
155 match !theory_to_visit_uris with
156 [] -> raise NoNextOrPrevUri
158 theory_to_visit_uris := tl ;
159 theory_visited_uris := uri::!theory_visited_uris ;
160 theory_update_output rendering_window uri ;
161 rendering_window#prevb#misc#set_sensitive true ;
163 rendering_window#nextb#misc#set_sensitive false
166 let next rendering_window () =
167 match !to_visit_uris with
168 [] -> raise NoNextOrPrevUri
170 to_visit_uris := tl ;
171 visited_uris := uri::!visited_uris ;
172 annotated_obj := None ;
173 update_output rendering_window uri ;
174 rendering_window#prevb#misc#set_sensitive true ;
176 rendering_window#nextb#misc#set_sensitive false
179 let theory_prev rendering_window () =
180 match !theory_visited_uris with
181 [] -> raise NoCurrentUri
182 | [_] -> raise NoNextOrPrevUri
183 | uri::(uri'::tl as newvu) ->
184 theory_visited_uris := newvu ;
185 theory_to_visit_uris := uri::!theory_to_visit_uris ;
186 theory_update_output rendering_window uri' ;
187 rendering_window#nextb#misc#set_sensitive true ;
189 rendering_window#prevb#misc#set_sensitive false
192 let prev rendering_window () =
193 match !visited_uris with
194 [] -> raise NoCurrentUri
195 | [_] -> raise NoNextOrPrevUri
196 | uri::(uri'::tl as newvu) ->
197 visited_uris := newvu ;
198 to_visit_uris := uri::!to_visit_uris ;
199 annotated_obj := None ;
200 update_output rendering_window uri' ;
201 rendering_window#nextb#misc#set_sensitive true ;
203 rendering_window#prevb#misc#set_sensitive false
206 (* called when an hyperlink is clicked *)
207 let jump rendering_window (node : Ominidom.o_mDOMNode) =
208 let module O = Ominidom in
209 match (node#get_attribute (O.o_mDOMString_of_string "href")) with
211 let s = str#get_string in
212 let uri = UriManager.uri_of_string s in
213 rendering_window#show () ;
214 rendering_window#prevb#misc#set_sensitive true ;
215 rendering_window#nextb#misc#set_sensitive false ;
216 visited_uris := uri::!visited_uris ;
217 to_visit_uris := [] ;
218 annotated_obj := None ;
219 update_output rendering_window uri
220 | None -> assert false
223 let choose_selection rendering_window (node : Ominidom.o_mDOMNode option) =
224 let module O = Ominidom in
226 match node#get_attribute (O.o_mDOMString_of_string "xref") with
227 Some _ -> rendering_window#output#set_selection (Some node)
228 | None -> aux (node#get_parent)
232 | None -> rendering_window#output#set_selection None
236 let theory_selection_changed rendering_window uri () =
240 if !theory_visited_uris <> [] then
241 rendering_window#prevb#misc#set_sensitive true ;
242 rendering_window#nextb#misc#set_sensitive false ;
243 theory_visited_uris := uri'::!theory_visited_uris ;
244 theory_to_visit_uris := [] ;
245 rendering_window#show () ;
246 theory_update_output rendering_window uri'
249 let selection_changed rendering_window uri () =
253 if !visited_uris <> [] then
254 rendering_window#prevb#misc#set_sensitive true ;
255 rendering_window#nextb#misc#set_sensitive false ;
256 visited_uris := uri'::!visited_uris ;
257 to_visit_uris := [] ;
258 annotated_obj := None ;
259 rendering_window#show () ;
260 update_output rendering_window uri'
263 (* CSC: unificare con la creazione la prima volta *)
264 let rec updateb_pressed theory_rendering_window rendering_window
265 (sw1, sw ,(hbox : GPack.box)) mktree ()
268 (* let's empty the uri trees and rebuild them *)
270 theoryuritree := [] ;
272 hbox#remove !sw1#coerce ;
273 hbox#remove !sw#coerce ;
276 GBin.scrolled_window ~width:250 ~height:600
277 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
279 GTree.tree ~selection_mode:`BROWSE ~packing:sw3#add_with_viewport () in
280 let tree_item1 = GTree.tree_item ~label:"theory:/" ~packing:tree1#append () in
282 ignore(tree_item1#connect#select
283 (theory_selection_changed theory_rendering_window None)) ;
284 mktree theory_selection_changed theory_rendering_window tree_item1
285 (Dir ("theory:/",theoryuritree)) ;
288 GBin.scrolled_window ~width:250 ~height:600
289 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
291 GTree.tree ~selection_mode:`BROWSE ~packing:sw2#add_with_viewport () in
292 let tree_item = GTree.tree_item ~label:"cic:/" ~packing:tree#append () in
294 ignore(tree_item#connect#select (selection_changed rendering_window None)) ;
295 mktree selection_changed rendering_window tree_item (Dir ("cic:/",uritree))
298 let theory_check rendering_window () =
301 TheoryTypeChecker.typecheck (theory_get_current_uri ());
302 "Type Checking was successful"
304 TheoryTypeChecker.NotWellTyped s ->
305 "Type Checking was NOT successful:\n\t" ^ s
307 (* next "cast" can't got rid of, but I don't know why *)
308 let errors = (rendering_window#errors : GEdit.text) in
309 let _ = errors#delete_text 0 errors#length in
313 let check rendering_window () =
316 CicTypeChecker.typecheck (get_current_uri ());
317 "Type Checking was successful"
319 CicTypeChecker.NotWellTyped s -> "Type Checking was NOT successful:\n\t" ^ s
321 (* next "cast" can't got rid of, but I don't know why *)
322 let errors = (rendering_window#errors : GEdit.text) in
323 let _ = errors#delete_text 0 errors#length in
327 let annotateb_pressed rendering_window annotation_window () =
328 let module O = Ominidom in
329 match rendering_window#output#get_selection with
332 match (node#get_attribute (O.o_mDOMString_of_string "xref")) with
334 let annobj = get_annotated_obj ()
335 (* next "cast" can't got rid of, but I don't know why *)
336 and annotation = (annotation_window#annotation : GEdit.text) in
337 ann := CicXPath.get_annotation annobj (xpath#get_string) ;
338 CicAnnotationHinter.create_hints annotation_window annobj (xpath#get_string) ;
339 annotation#delete_text 0 annotation#length ;
343 annotation#misc#set_sensitive false ;
344 annotation_window#radio_none#set_active true ;
345 radio_some_status := false
347 annotation#insert ann' ;
348 annotation#misc#set_sensitive true ;
349 annotation_window#radio_some#set_active true ;
350 radio_some_status := true
352 GMain.Grab.add (annotation_window#window_to_annotate#coerce) ;
353 annotation_window#show () ;
355 (* next "cast" can't got rid of, but I don't know why *)
356 let errors = (rendering_window#errors : GEdit.text) in
357 errors#insert ("\nNo xref found\n")
359 | None -> (rendering_window#errors : GEdit.text)#insert "\nNo selection!\n"
362 (* called when the annotation is confirmed *)
363 let save_annotation annotation =
364 if !radio_some_status then
365 !ann := Some (annotation#get_chars 0 annotation#length)
368 match !annotated_obj with
371 let uri = get_current_uri () in
372 let annxml = Annotation2Xml.pp_annotation annobj uri in
373 Xml.pp annxml (Some (fst (Getter.get_ann_file_name_and_uri uri)))
376 let parse_no_cache uri =
377 let module U = UriManager in
378 XsltProcessor.process uri false "cic"
382 (* STUFF TO BUILD THE GTK INTERFACE *)
384 (* Stuff to build the tree window *)
386 (* selection_changed is actually selection_changed or theory_selection_changed*)
387 let mktree selection_changed rendering_window =
388 let rec aux treeitem =
390 Dir (dirname, content) ->
391 let subtree = GTree.tree () in
392 treeitem#set_subtree subtree ;
395 let label = get_name ti
396 and uri = get_uri ti in
397 let treeitem2 = GTree.tree_item ~label:label () in
398 subtree#append treeitem2 ;
399 ignore(treeitem2#connect#select
400 (selection_changed rendering_window uri)) ;
402 ) (List.sort compare !content)
408 (* Stuff for the widget settings *)
410 let export_to_postscript (output : GMathView.math_view) () =
411 output#export_to_postscript ~filename:"output.ps" ();
414 let activate_t1 output button_set_anti_aliasing button_set_kerning
415 button_export_to_postscript button_t1 ()
417 let is_set = button_t1#active in
418 output#set_font_manager_type
419 (if is_set then `font_manager_t1 else `font_manager_gtk) ;
422 button_set_anti_aliasing#misc#set_sensitive true ;
423 button_set_kerning#misc#set_sensitive true ;
424 button_export_to_postscript#misc#set_sensitive true ;
428 button_set_anti_aliasing#misc#set_sensitive false ;
429 button_set_kerning#misc#set_sensitive false ;
430 button_export_to_postscript#misc#set_sensitive false ;
434 let set_anti_aliasing output button_set_anti_aliasing () =
435 output#set_anti_aliasing button_set_anti_aliasing#active
438 let set_kerning output button_set_kerning () =
439 output#set_kerning button_set_kerning#active
442 let changefont output font_size_spinb () =
443 output#set_font_size font_size_spinb#value_as_int
446 let set_log_verbosity output log_verbosity_spinb () =
447 output#set_log_verbosity log_verbosity_spinb#value_as_int
450 class settings_window output sw button_export_to_postscript jump_callback
451 selection_changed_callback
453 let settings_window = GWindow.window ~title:"GtkMathView settings" () in
455 GPack.vbox ~packing:settings_window#add () in
458 ~rows:1 ~columns:3 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
459 ~border_width:5 ~packing:vbox#add () in
461 GButton.toggle_button ~label:"activate t1 fonts"
462 ~packing:(table#attach ~left:0 ~top:0) () in
463 let button_set_anti_aliasing =
464 GButton.toggle_button ~label:"set_anti_aliasing"
465 ~packing:(table#attach ~left:1 ~top:0) () in
466 let button_set_kerning =
467 GButton.toggle_button ~label:"set_kerning"
468 ~packing:(table#attach ~left:2 ~top:0) () in
471 ~rows:2 ~columns:2 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
472 ~border_width:5 ~packing:vbox#add () in
473 let font_size_label =
474 GMisc.label ~text:"font size:"
475 ~packing:(table#attach ~left:0 ~top:0 ~expand:`NONE) () in
476 let font_size_spinb =
478 GData.adjustment ~value:14.0 ~lower:5.0 ~upper:50.0 ~step_incr:1.0 ()
481 ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:0 ~fill:`NONE) () in
482 let log_verbosity_label =
483 GMisc.label ~text:"log verbosity:"
484 ~packing:(table#attach ~left:0 ~top:1) () in
485 let log_verbosity_spinb =
487 GData.adjustment ~value:0.0 ~lower:0.0 ~upper:3.0 ~step_incr:1.0 ()
490 ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:1) () in
492 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
494 GButton.button ~label:"Close"
495 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
497 method show = settings_window#show
499 button_set_anti_aliasing#misc#set_sensitive false ;
500 button_set_kerning#misc#set_sensitive false ;
501 (* Signals connection *)
502 ignore(button_t1#connect#clicked
503 (activate_t1 output button_set_anti_aliasing button_set_kerning
504 button_export_to_postscript button_t1)) ;
505 ignore(font_size_spinb#connect#changed (changefont output font_size_spinb)) ;
506 ignore(button_set_anti_aliasing#connect#toggled
507 (set_anti_aliasing output button_set_anti_aliasing));
508 ignore(button_set_kerning#connect#toggled
509 (set_kerning output button_set_kerning)) ;
510 ignore(log_verbosity_spinb#connect#changed
511 (set_log_verbosity output log_verbosity_spinb)) ;
512 ignore(closeb#connect#clicked settings_window#misc#hide)
517 class annotation_window output label =
518 let window_to_annotate =
519 GWindow.window ~title:"Annotating environment" ~border_width:2 () in
521 GPack.hbox ~packing:window_to_annotate#add () in
523 GPack.vbox ~packing:(hbox1#pack ~padding:5) () in
525 GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
526 let radio_some = GButton.radio_button ~label:"Annotation below"
527 ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
528 let radio_none = GButton.radio_button ~label:"No annotation"
529 ~group:radio_some#group
530 ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5)
532 let annotation = GEdit.text ~editable:true ~width:400 ~height:180
533 ~packing:(vbox1#pack ~padding:5) () in
535 GPack.table ~rows:3 ~columns:3 ~packing:(vbox1#pack ~padding:5) () in
536 let annotation_hints =
539 GButton.button ~label:("Hint " ^ string_of_int i)
540 ~packing:(table#attach ~left:(i mod 3) ~top:(i / 3)) ()
543 GPack.vbox ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
545 GButton.button ~label:"O.K."
546 ~packing:(vbox2#pack ~expand:false ~fill:false ~padding:5) () in
548 GButton.button ~label:"Abort"
549 ~packing:(vbox2#pack ~expand:false ~fill:false ~padding:5) () in
551 method window_to_annotate = window_to_annotate
552 method annotation = annotation
553 method radio_some = radio_some
554 method radio_none = radio_none
555 method annotation_hints = annotation_hints
556 method output = (output : GMathView.math_view)
557 method show () = window_to_annotate#show ()
559 (* signal handlers here *)
560 ignore (window_to_annotate#event#connect#delete
562 window_to_annotate#misc#hide () ;
563 GMain.Grab.remove (window_to_annotate#coerce) ;
566 ignore (confirmb#connect#clicked
568 window_to_annotate#misc#hide () ;
569 save_annotation annotation ;
570 GMain.Grab.remove (window_to_annotate#coerce) ;
571 let new_current_uri =
572 (snd (Getter.get_ann_file_name_and_uri (get_current_uri ())))
574 visited_uris := new_current_uri::(List.tl !visited_uris) ;
575 label#set_text (UriManager.string_of_uri new_current_uri) ;
576 let mmlfile = parse_no_cache new_current_uri in
579 ignore (abortb#connect#clicked
581 window_to_annotate#misc#hide () ;
582 GMain.Grab.remove (window_to_annotate#coerce)
584 ignore (radio_some#connect#clicked
585 (fun () -> annotation#misc#set_sensitive true ; radio_some_status := true)) ;
586 ignore (radio_none #connect#clicked
588 annotation#misc#set_sensitive false;
589 radio_some_status := false)
593 class rendering_window annotation_window output (label : GMisc.label) =
595 GWindow.window ~title:"MathML viewer" ~border_width:2 () in
597 GPack.vbox ~packing:window#add () in
598 let _ = vbox#pack ~expand:false ~fill:false ~padding:5 label#coerce in
600 GPack.paned `HORIZONTAL ~packing:(vbox#pack ~expand:true ~padding:5) () in
601 let scrolled_window0 =
602 GBin.scrolled_window ~border_width:10 ~packing:paned#add1 () in
603 let _ = scrolled_window0#add output#coerce in
604 let scrolled_window =
606 ~border_width:10 ~packing:paned#add2 ~width:240 ~height:100 () in
607 let errors = GEdit.text ~packing:scrolled_window#add_with_viewport () in
609 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
611 GButton.button ~label:"Prev"
612 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
614 GButton.button ~label:"Next"
615 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
617 GButton.button ~label:"Check"
618 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
620 GButton.button ~label:"Annotate"
621 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
623 GButton.button ~label:"Settings"
624 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
625 let button_export_to_postscript =
626 GButton.button ~label:"export_to_postscript"
627 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
629 GButton.button ~label:"Close"
630 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
635 method output = (output : GMathView.math_view)
636 method errors = errors
637 method show () = window#show ()
639 nextb#misc#set_sensitive false ;
640 prevb#misc#set_sensitive false ;
641 button_export_to_postscript#misc#set_sensitive false ;
643 (* signal handlers here *)
644 ignore(output#connect#jump (jump self)) ;
645 ignore(output#connect#selection_changed (choose_selection self)) ;
646 ignore(nextb#connect#clicked (next self)) ;
647 ignore(prevb#connect#clicked (prev self)) ;
648 ignore(checkb#connect#clicked (check self)) ;
649 ignore(closeb#connect#clicked window#misc#hide) ;
650 ignore(annotateb#connect#clicked (annotateb_pressed self annotation_window)) ;
651 let settings_window = new settings_window output scrolled_window0
652 button_export_to_postscript (jump self) (choose_selection self) in
653 ignore(settingsb#connect#clicked settings_window#show) ;
654 ignore(button_export_to_postscript#connect#clicked (export_to_postscript output)) ;
655 ignore(window#event#connect#delete (fun _ -> window#misc#hide () ; true ))
658 class theory_rendering_window rendering_window =
660 GWindow.window ~title:"MathML theory viewer" ~border_width:2 () in
662 GPack.vbox ~packing:window#add () in
664 GMisc.label ~text:"???"
665 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
667 GPack.paned `HORIZONTAL ~packing:(vbox#pack ~expand:true ~padding:5) () in
668 let scrolled_window0 =
669 GBin.scrolled_window ~border_width:10 ~packing:paned#add1 () in
671 GMathView.math_view ~width:400 ~height:380 ~packing:scrolled_window0#add () in
672 let scrolled_window =
674 ~border_width:10 ~packing:paned#add2 ~width:240 ~height:100 () in
675 let errors = GEdit.text ~packing:scrolled_window#add_with_viewport () in
677 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
679 GButton.button ~label:"Prev"
680 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
682 GButton.button ~label:"Next"
683 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
685 GButton.button ~label:"Check"
686 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
688 GButton.button ~label:"Settings"
689 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
690 let button_export_to_postscript =
691 GButton.button ~label:"export_to_postscript"
692 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
694 GButton.button ~label:"Close"
695 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
700 method output = (output : GMathView.math_view)
701 method errors = errors
702 method show () = window#show ()
704 nextb#misc#set_sensitive false ;
705 prevb#misc#set_sensitive false ;
706 button_export_to_postscript#misc#set_sensitive false ;
708 (* signal handlers here *)
709 ignore(output#connect#jump (jump rendering_window)) ;
710 ignore(output#connect#selection_changed (choose_selection self)) ;
711 ignore(nextb#connect#clicked (theory_next self)) ;
712 ignore(prevb#connect#clicked (theory_prev self)) ;
713 ignore(checkb#connect#clicked (theory_check self)) ;
714 let settings_window = new settings_window output scrolled_window0
715 button_export_to_postscript (jump rendering_window)(choose_selection self) in
716 ignore(settingsb#connect#clicked settings_window#show) ;
717 ignore(button_export_to_postscript#connect#clicked (export_to_postscript output)) ;
718 ignore(closeb#connect#clicked window#misc#hide) ;
719 ignore(window#event#connect#delete (fun _ -> window#misc#hide () ; true ))
722 (* CSC: fare in modo che i due alberi vengano svuotati invece che distrutti *)
723 class selection_window theory_rendering_window rendering_window =
724 let label = "cic:/" in
725 let theorylabel = "theory:/" in
726 let win = GWindow.window ~title:"Known uris" ~border_width:2 () in
727 let vbox = GPack.vbox ~packing:win#add () in
728 let hbox1 = GPack.hbox ~packing:(vbox#pack ~padding:5) () in
729 let sw1 = GBin.scrolled_window ~width:250 ~height:600
730 ~packing:(hbox1#pack ~padding:5) () in
732 GTree.tree ~selection_mode:`BROWSE ~packing:sw1#add_with_viewport () in
734 GTree.tree_item ~label:theorylabel ~packing:tree1#append () in
735 let sw = GBin.scrolled_window ~width:250 ~height:600
736 ~packing:(hbox1#pack ~padding:5) () in
738 GTree.tree ~selection_mode:`BROWSE ~packing:sw#add_with_viewport () in
740 GTree.tree_item ~label:label ~packing:tree#append () in
742 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
744 GButton.button ~label:"Update"
745 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
747 GButton.button ~label:"Quit"
748 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
750 method show () = win#show ()
752 mktree theory_selection_changed theory_rendering_window tree_item1
753 (Dir ("theory:/",theoryuritree));
754 mktree selection_changed rendering_window tree_item
755 (Dir ("cic:/",uritree));
757 (* signal handlers here *)
758 ignore (tree_item1#connect#select
759 ~callback:(theory_selection_changed theory_rendering_window None)) ;
760 ignore (tree_item#connect#select
761 ~callback:(selection_changed rendering_window None)) ;
762 ignore (win#connect#destroy ~callback:GMain.Main.quit) ;
763 ignore (quitb#connect#clicked GMain.Main.quit) ;
764 ignore(updateb#connect#clicked (updateb_pressed
765 theory_rendering_window rendering_window (ref sw1, ref sw, hbox1) mktree))
773 let output = GMathView.math_view ~width:400 ~height:380 ()
774 and label = GMisc.label ~text:"???" () in
775 let annotation_window = new annotation_window output label in
776 let rendering_window = new rendering_window annotation_window output label in
777 let theory_rendering_window = new theory_rendering_window rendering_window in
778 let selection_window =
779 new selection_window theory_rendering_window rendering_window
781 selection_window#show () ;