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 []
31 (* Brutti, per via del widget che non e' imperativo *)
32 let loaded_uri = ref "";;
33 let theory_loaded_uri = ref "";;
38 | File (name,_) -> name
44 | File (_,uri) -> Some uri
47 (* STUFF TO BUILD THE URI TREE *)
50 exception DuplicatedUri
51 exception ConflictingUris
53 let insert_in_uri_tree uri =
58 let _ = List.find (fun item -> name = get_name item) !l in
61 Not_found -> l := (File (name,uri))::!l
65 match List.find (fun item -> name = get_name item) !l with
66 Dir (_,children) -> aux children tl
67 | File _ -> raise ConflictingUris
70 let children = ref [] in
71 l := (Dir (name,children))::!l ;
74 | [] -> raise EmptyUri
79 (* Imperative procedure that builds the two uri trees *)
80 let build_uri_tree () =
81 let dbh = Dbm.opendbm Configuration.uris_dbm [Dbm.Dbm_rdonly] 0 in
84 let cicregexp = Str.regexp "cic:"
85 and theoryregexp = Str.regexp "theory:" in
86 if Str.string_match cicregexp uri 0 then
87 let s = Str.replace_first cicregexp "" uri in
88 let l = Str.split (Str.regexp "/") s in
89 insert_in_uri_tree (UriManager.uri_of_string uri) uritree l
90 else if Str.string_match theoryregexp uri 0 then
91 let s = Str.replace_first theoryregexp "" uri in
92 let l = Str.split (Str.regexp "/") s in
93 insert_in_uri_tree (UriManager.uri_of_string uri) theoryuritree l
98 (* GLOBAL REFERENCES (USED BY CALLBACKS) *)
100 let annotated_obj = ref None;; (* reference to a couple option where *)
101 (* the first component is the current *)
102 (* annotated object and the second is *)
103 (* the map from ids to annotated targets *)
104 let ann = ref (ref None);; (* current annotation *)
105 let radio_some_status = ref false;; (* is the radio_some button selected? *)
107 let theory_visited_uris = ref [];;
108 let theory_to_visit_uris = ref [];;
109 let visited_uris = ref [];;
110 let to_visit_uris = ref [];;
114 exception NoCurrentUri;;
115 exception NoNextOrPrevUri;;
116 exception GtkInterfaceInternalError;;
118 let theory_get_current_uri () =
119 match !theory_visited_uris with
120 [] -> raise NoCurrentUri
124 let get_current_uri () =
125 match !visited_uris with
126 [] -> raise NoCurrentUri
130 let get_annotated_obj () =
131 match !annotated_obj with
133 let (annobj, ids_to_targets,_) =
134 (CicCache.get_annobj (get_current_uri ()))
136 annotated_obj := Some (annobj, ids_to_targets) ;
137 (annobj, ids_to_targets)
138 | Some annobj -> annobj
141 let filename_of_uri uri =
145 let theory_update_output rendering_window uri =
146 rendering_window#label#set_text (UriManager.string_of_uri uri) ;
147 ignore (rendering_window#errors#delete_text 0 rendering_window#errors#length) ;
148 let mmlfile = XsltProcessor.process uri true "theory" in
149 theory_loaded_uri := mmlfile ;
150 !(rendering_window#output)#load mmlfile
153 let update_output rendering_window uri =
154 rendering_window#label#set_text (UriManager.string_of_uri uri) ;
155 ignore (rendering_window#errors#delete_text 0 rendering_window#errors#length) ;
156 let mmlfile = XsltProcessor.process uri true "cic" in
157 loaded_uri := mmlfile ;
158 !(rendering_window#output)#load mmlfile
161 let theory_next rendering_window () =
162 match !theory_to_visit_uris with
163 [] -> raise NoNextOrPrevUri
165 theory_to_visit_uris := tl ;
166 theory_visited_uris := uri::!theory_visited_uris ;
167 theory_update_output rendering_window uri ;
168 rendering_window#prevb#misc#set_sensitive true ;
170 rendering_window#nextb#misc#set_sensitive false
173 let next rendering_window () =
174 match !to_visit_uris with
175 [] -> raise NoNextOrPrevUri
177 to_visit_uris := tl ;
178 visited_uris := uri::!visited_uris ;
179 annotated_obj := None ;
180 update_output rendering_window uri ;
181 rendering_window#prevb#misc#set_sensitive true ;
183 rendering_window#nextb#misc#set_sensitive false
186 let theory_prev rendering_window () =
187 match !theory_visited_uris with
188 [] -> raise NoCurrentUri
189 | [_] -> raise NoNextOrPrevUri
190 | uri::(uri'::tl as newvu) ->
191 theory_visited_uris := newvu ;
192 theory_to_visit_uris := uri::!theory_to_visit_uris ;
193 theory_update_output rendering_window uri' ;
194 rendering_window#nextb#misc#set_sensitive true ;
196 rendering_window#prevb#misc#set_sensitive false
199 let prev rendering_window () =
200 match !visited_uris with
201 [] -> raise NoCurrentUri
202 | [_] -> raise NoNextOrPrevUri
203 | uri::(uri'::tl as newvu) ->
204 visited_uris := newvu ;
205 to_visit_uris := uri::!to_visit_uris ;
206 annotated_obj := None ;
207 update_output rendering_window uri' ;
208 rendering_window#nextb#misc#set_sensitive true ;
210 rendering_window#prevb#misc#set_sensitive false
213 (* called when an hyperlink is clicked *)
214 let jump rendering_window node =
215 let module M = Minidom in
217 match M.node_get_attribute node (M.mDOMString_of_string "href") with
219 | Some s -> M.string_of_mDOMString s
221 let uri = UriManager.uri_of_string s in
222 rendering_window#show () ;
223 rendering_window#prevb#misc#set_sensitive true ;
224 rendering_window#nextb#misc#set_sensitive false ;
225 visited_uris := uri::!visited_uris ;
226 to_visit_uris := [] ;
227 annotated_obj := None ;
228 update_output rendering_window uri
231 let choose_selection rendering_window node =
232 let module M = Minidom in
233 let rec aux ~first_time node =
234 match M.node_get_attribute node (M.mDOMString_of_string "xref") with
237 match M.node_get_parent node with
239 | Some parent -> parent
241 aux ~first_time:false parent
243 if not first_time then
244 !(rendering_window#output)#set_selection (Some node)
247 None -> () (* No element selected *)
248 | Some node -> aux ~first_time:true node
252 let theory_selection_changed rendering_window uri () =
256 if !theory_visited_uris <> [] then
257 rendering_window#prevb#misc#set_sensitive true ;
258 rendering_window#nextb#misc#set_sensitive false ;
259 theory_visited_uris := uri'::!theory_visited_uris ;
260 theory_to_visit_uris := [] ;
261 rendering_window#show () ;
262 theory_update_output rendering_window uri'
265 let selection_changed rendering_window uri () =
269 if !visited_uris <> [] then
270 rendering_window#prevb#misc#set_sensitive true ;
271 rendering_window#nextb#misc#set_sensitive false ;
272 visited_uris := uri'::!visited_uris ;
273 to_visit_uris := [] ;
274 annotated_obj := None ;
275 rendering_window#show () ;
276 update_output rendering_window uri'
279 (* CSC: unificare con la creazione la prima volta *)
280 let rec updateb_pressed theory_rendering_window rendering_window
281 (sw1, sw ,(hbox : GPack.box)) mktree ()
284 (* let's empty the uri trees and rebuild them *)
286 theoryuritree := [] ;
288 hbox#remove !sw1#coerce ;
289 hbox#remove !sw#coerce ;
292 GBin.scrolled_window ~width:250 ~height:600
293 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
295 GTree.tree ~selection_mode:`BROWSE ~packing:sw3#add_with_viewport () in
296 let tree_item1 = GTree.tree_item ~label:"theory:/" ~packing:tree1#append () in
298 ignore(tree_item1#connect#select
299 (theory_selection_changed theory_rendering_window None)) ;
300 mktree theory_selection_changed theory_rendering_window tree_item1
301 (Dir ("theory:/",theoryuritree)) ;
304 GBin.scrolled_window ~width:250 ~height:600
305 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
307 GTree.tree ~selection_mode:`BROWSE ~packing:sw2#add_with_viewport () in
308 let tree_item = GTree.tree_item ~label:"cic:/" ~packing:tree#append () in
310 ignore(tree_item#connect#select (selection_changed rendering_window None)) ;
311 mktree selection_changed rendering_window tree_item (Dir ("cic:/",uritree))
314 let theory_check rendering_window () =
317 TheoryTypeChecker.typecheck (theory_get_current_uri ());
318 "Type Checking was successful"
320 TheoryTypeChecker.NotWellTyped s ->
321 "Type Checking was NOT successful:\n\t" ^ s
323 (* next "cast" can't got rid of, but I don't know why *)
324 let errors = (rendering_window#errors : GEdit.text) in
325 let _ = errors#delete_text 0 errors#length in
329 let check rendering_window () =
332 CicTypeChecker.typecheck (get_current_uri ());
333 "Type Checking was successful"
335 CicTypeChecker.NotWellTyped s -> "Type Checking was NOT successful:\n\t" ^ s
337 (* next "cast" can't got rid of, but I don't know why *)
338 let errors = (rendering_window#errors : GEdit.text) in
339 let _ = errors#delete_text 0 errors#length in
343 let annotateb_pressed rendering_window annotation_window () =
344 let module M = Minidom in
345 match !(rendering_window#output)#get_selection with
346 None -> (rendering_window#errors : GEdit.text)#insert "\nNo selection!\n"
349 match M.node_get_attribute node (M.mDOMString_of_string "xref") with
351 | Some xpath -> M.string_of_mDOMString xpath
354 let annobj = get_annotated_obj ()
355 (* next "cast" can't got rid of, but I don't know why *)
356 and annotation = (annotation_window#annotation : GEdit.text) in
357 ann := CicXPath.get_annotation annobj xpath ;
358 CicAnnotationHinter.create_hints annotation_window annobj xpath ;
359 annotation#delete_text 0 annotation#length ;
363 annotation#misc#set_sensitive false ;
364 annotation_window#radio_none#set_active true ;
365 radio_some_status := false
367 annotation#insert ann' ;
368 annotation#misc#set_sensitive true ;
369 annotation_window#radio_some#set_active true ;
370 radio_some_status := true
372 GMain.Grab.add (annotation_window#window_to_annotate#coerce) ;
373 annotation_window#show () ;
376 (* next "cast" can't got rid of, but I don't know why *)
377 let errors = (rendering_window#errors : GEdit.text) in
378 errors#insert ("\n" ^ Printexc.to_string e ^ "\n")
381 (* called when the annotation is confirmed *)
382 let save_annotation annotation =
383 if !radio_some_status then
384 !ann := Some (annotation#get_chars 0 annotation#length)
387 match !annotated_obj with
388 None -> raise GtkInterfaceInternalError
390 let uri = get_current_uri () in
391 let annxml = Annotation2Xml.pp_annotation annobj uri in
392 Xml.pp annxml (Some (fst (Getter.get_ann_file_name_and_uri uri)))
395 let parse_no_cache uri =
396 let module U = UriManager in
397 XsltProcessor.process uri false "cic"
401 (* STUFF TO BUILD THE GTK INTERFACE *)
403 (* Stuff to build the tree window *)
405 (* selection_changed is actually selection_changed or theory_selection_changed*)
406 let mktree selection_changed rendering_window =
407 let rec aux treeitem =
409 Dir (dirname, content) ->
410 let subtree = GTree.tree () in
411 treeitem#set_subtree subtree ;
414 let label = get_name ti
415 and uri = get_uri ti in
416 let treeitem2 = GTree.tree_item ~label:label () in
417 subtree#append treeitem2 ;
418 ignore(treeitem2#connect#select
419 (selection_changed rendering_window uri)) ;
421 ) (List.sort compare !content)
427 (* Stuff for the widget settings *)
429 let export_to_postscript output () =
430 !output#export_to_postscript "output.ps" ;
433 let activate_t1 output sw is_set jump_callback selection_changed_callback
436 is_set := not !is_set ;
437 sw#remove !output#coerce ;
439 (GMathView.math_view ~packing:sw#add ~width:400 ~height:380
440 ~use_t1_lib:!is_set ()) ;
441 !output#load !last_uri ;
442 ignore(!output#connect#jump jump_callback) ;
443 ignore(!output#connect#selection_changed selection_changed_callback) ;
446 let set_anti_aliasing output is_set () =
447 is_set := not !is_set ;
448 !output#set_anti_aliasing !is_set
451 let set_kerning output is_set () =
452 is_set := not !is_set ;
453 !output#set_kerning !is_set
456 let changefont output font_size_spinb () =
457 !output#set_font_size font_size_spinb#value_as_int
460 let set_log_verbosity output log_verbosity_spinb () =
461 !output#set_log_verbosity log_verbosity_spinb#value_as_int
464 class settings_window output sw jump_callback selection_changed_callback
467 let settings_window = GWindow.window ~title:"GtkMathView settings" () in
468 let table = GPack.table ~rows:5 ~columns:5 ~packing:settings_window#add () in
470 GButton.toggle_button ~label:"activate t1 fonts"
471 ~packing:(table#attach ~left:0 ~top:0) () in
472 let font_size_spinb =
474 GData.adjustment ~value:14.0 ~lower:5.0 ~upper:50.0 ~step_incr:1.0 ()
477 ~adjustment:sadj ~packing:(table#attach ~left:4 ~top:2) () in
478 let button_set_anti_aliasing = GButton.toggle_button ~label:"set_anti_aliasing" ~packing:(table#attach ~left:1 ~top:3) () in
479 let button_set_kerning =
480 GButton.toggle_button ~label:"set_kerning"
481 ~packing:(table#attach ~left:3 ~top:3) () in
482 let log_verbosity_spinb =
484 GData.adjustment ~value:0.0 ~lower:0.0 ~upper:3.0 ~step_incr:1.0 ()
487 ~adjustment:sadj ~packing:(table#attach ~left:2 ~top:2) () in
489 method show = settings_window#show
491 (* Signals connection *)
492 let is_set_use_t1_lib = ref false in
493 ignore(button_t1#connect#clicked
494 (activate_t1 output sw is_set_use_t1_lib jump_callback
495 selection_changed_callback last_uri)) ;
496 ignore(font_size_spinb#connect#changed (changefont output font_size_spinb)) ;
497 let is_set_anti_aliasing = ref false in
498 ignore(button_set_anti_aliasing#connect#toggled
499 (set_anti_aliasing output is_set_anti_aliasing));
500 let is_set_kerning = ref false in
501 ignore(button_set_kerning#connect#toggled
502 (set_kerning output is_set_kerning)) ;
503 ignore(log_verbosity_spinb#connect#changed
504 (set_log_verbosity output log_verbosity_spinb))
509 class annotation_window output label =
510 let window_to_annotate =
511 GWindow.window ~title:"Annotating environment" ~border_width:2 () in
513 GPack.hbox ~packing:window_to_annotate#add () in
515 GPack.vbox ~packing:(hbox1#pack ~padding:5) () in
517 GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
518 let radio_some = GButton.radio_button ~label:"Annotation below"
519 ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
520 let radio_none = GButton.radio_button ~label:"No annotation"
521 ~group:radio_some#group
522 ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5)
524 let annotation = GEdit.text ~editable:true ~width:400 ~height:180
525 ~packing:(vbox1#pack ~padding:5) () in
527 GPack.table ~rows:3 ~columns:3 ~packing:(vbox1#pack ~padding:5) () in
528 let annotation_hints =
531 GButton.button ~label:("Hint " ^ string_of_int i)
532 ~packing:(table#attach ~left:(i mod 3) ~top:(i / 3)) ()
535 GPack.vbox ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
537 GButton.button ~label:"O.K."
538 ~packing:(vbox2#pack ~expand:false ~fill:false ~padding:5) () in
540 GButton.button ~label:"Abort"
541 ~packing:(vbox2#pack ~expand:false ~fill:false ~padding:5) () in
543 method window_to_annotate = window_to_annotate
544 method annotation = annotation
545 method radio_some = radio_some
546 method radio_none = radio_none
547 method annotation_hints = annotation_hints
548 method output = (output : GMathView.math_view ref)
549 method show () = window_to_annotate#show ()
551 (* signal handlers here *)
552 ignore (window_to_annotate#event#connect#delete
554 window_to_annotate#misc#hide () ;
555 GMain.Grab.remove (window_to_annotate#coerce) ;
558 ignore (confirmb#connect#clicked
560 window_to_annotate#misc#hide () ;
561 save_annotation annotation ;
562 GMain.Grab.remove (window_to_annotate#coerce) ;
563 let new_current_uri =
564 (snd (Getter.get_ann_file_name_and_uri (get_current_uri ())))
566 visited_uris := new_current_uri::(List.tl !visited_uris) ;
567 label#set_text (UriManager.string_of_uri new_current_uri) ;
568 let mmlfile = parse_no_cache new_current_uri in
569 loaded_uri := mmlfile ;
572 ignore (abortb#connect#clicked
574 window_to_annotate#misc#hide () ;
575 GMain.Grab.remove (window_to_annotate#coerce)
577 ignore (radio_some#connect#clicked
578 (fun () -> annotation#misc#set_sensitive true ; radio_some_status := true)) ;
579 ignore (radio_none #connect#clicked
581 annotation#misc#set_sensitive false;
582 radio_some_status := false)
586 class rendering_window annotation_window output (label : GMisc.label) =
588 GWindow.window ~title:"MathML viewer" ~border_width:2 () in
590 GPack.vbox ~packing:window#add () in
591 let _ = vbox#pack ~expand:false ~fill:false ~padding:5 label#coerce in
593 GPack.paned `HORIZONTAL ~packing:(vbox#pack ~padding:5) () in
594 let scrolled_window0 =
595 GBin.scrolled_window ~border_width:10 ~packing:paned#add1 () in
596 let _ = scrolled_window0#add !output#coerce in
597 let scrolled_window =
599 ~border_width:10 ~packing:paned#add2 ~width:240 ~height:100 () in
600 let errors = GEdit.text ~packing:scrolled_window#add_with_viewport () in
602 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
604 GButton.button ~label:"Prev"
605 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
607 GButton.button ~label:"Next"
608 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
610 GButton.button ~label:"Check"
611 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
613 GButton.button ~label:"Annotate"
614 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
616 GButton.button ~label:"Settings"
617 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
618 let button_export_to_postscript =
619 GButton.button ~label:"export_to_postscript"
620 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
622 GButton.button ~label:"Close"
623 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
628 method output = (output : GMathView.math_view ref)
629 method errors = errors
630 method show () = window#show ()
632 nextb#misc#set_sensitive false ;
633 prevb#misc#set_sensitive false ;
635 (* signal handlers here *)
636 ignore(!output#connect#jump (jump self)) ;
637 ignore(!output#connect#selection_changed (choose_selection self)) ;
638 ignore(nextb#connect#clicked (next self)) ;
639 ignore(prevb#connect#clicked (prev self)) ;
640 ignore(checkb#connect#clicked (check self)) ;
641 ignore(closeb#connect#clicked window#misc#hide) ;
642 ignore(annotateb#connect#clicked (annotateb_pressed self annotation_window)) ;
643 let settings_window = new settings_window output scrolled_window0
644 (jump self) (choose_selection self) loaded_uri in
645 ignore(settingsb#connect#clicked settings_window#show) ;
646 ignore(button_export_to_postscript#connect#clicked (export_to_postscript output)) ;
647 ignore(window#event#connect#delete (fun _ -> window#misc#hide () ; true ))
650 class theory_rendering_window rendering_window =
652 GWindow.window ~title:"MathML theory viewer" ~border_width:2 () in
654 GPack.vbox ~packing:window#add () in
656 GMisc.label ~text:"???"
657 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
659 GPack.paned `HORIZONTAL ~packing:(vbox#pack ~padding:5) () in
660 let scrolled_window0 =
661 GBin.scrolled_window ~border_width:10 ~packing:paned#add1 () in
663 ref (GMathView.math_view ~use_t1_lib:false ~width:400 ~height:380
664 ~packing:scrolled_window0#add ()) in
665 let scrolled_window =
667 ~border_width:10 ~packing:paned#add2 ~width:240 ~height:100 () in
668 let errors = GEdit.text ~packing:scrolled_window#add_with_viewport () in
670 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
672 GButton.button ~label:"Prev"
673 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
675 GButton.button ~label:"Next"
676 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
678 GButton.button ~label:"Check"
679 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
681 GButton.button ~label:"Settings"
682 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
683 let button_export_to_postscript =
684 GButton.button ~label:"export_to_postscript"
685 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
687 GButton.button ~label:"Close"
688 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
693 method output = (output : GMathView.math_view ref)
694 method errors = errors
695 method show () = window#show ()
697 nextb#misc#set_sensitive false ;
698 prevb#misc#set_sensitive false ;
700 (* signal handlers here *)
701 ignore(!output#connect#jump (jump rendering_window)) ;
702 ignore(!output#connect#selection_changed (choose_selection self)) ;
703 ignore(nextb#connect#clicked (theory_next self)) ;
704 ignore(prevb#connect#clicked (theory_prev self)) ;
705 ignore(checkb#connect#clicked (theory_check self)) ;
706 let settings_window = new settings_window output scrolled_window0
707 (jump rendering_window) (choose_selection self) theory_loaded_uri in
708 ignore(settingsb#connect#clicked settings_window#show) ;
709 ignore(button_export_to_postscript#connect#clicked (export_to_postscript output)) ;
710 ignore(closeb#connect#clicked window#misc#hide) ;
711 ignore(window#event#connect#delete (fun _ -> window#misc#hide () ; true ))
714 (* CSC: fare in modo che i due alberi vengano svuotati invece che distrutti *)
715 class selection_window theory_rendering_window rendering_window =
716 let label = "cic:/" in
717 let theorylabel = "theory:/" in
718 let win = GWindow.window ~title:"Known uris" ~border_width:2 () in
719 let vbox = GPack.vbox ~packing:win#add () in
720 let hbox1 = GPack.hbox ~packing:(vbox#pack ~padding:5) () in
721 let sw1 = GBin.scrolled_window ~width:250 ~height:600
722 ~packing:(hbox1#pack ~padding:5) () in
724 GTree.tree ~selection_mode:`BROWSE ~packing:sw1#add_with_viewport () in
726 GTree.tree_item ~label:theorylabel ~packing:tree1#append () in
727 let sw = GBin.scrolled_window ~width:250 ~height:600
728 ~packing:(hbox1#pack ~padding:5) () in
730 GTree.tree ~selection_mode:`BROWSE ~packing:sw#add_with_viewport () in
732 GTree.tree_item ~label:label ~packing:tree#append () in
734 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
736 GButton.button ~label:"Update"
737 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
739 GButton.button ~label:"Quit"
740 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
742 method show () = win#show ()
744 mktree theory_selection_changed theory_rendering_window tree_item1
745 (Dir ("theory:/",theoryuritree));
746 mktree selection_changed rendering_window tree_item
747 (Dir ("cic:/",uritree));
749 (* signal handlers here *)
750 ignore (tree_item1#connect#select
751 ~callback:(theory_selection_changed theory_rendering_window None)) ;
752 ignore (tree_item#connect#select
753 ~callback:(selection_changed rendering_window None)) ;
754 ignore (win#connect#destroy ~callback:GMain.Main.quit) ;
755 ignore (quitb#connect#clicked GMain.Main.quit) ;
756 ignore(updateb#connect#clicked (updateb_pressed
757 theory_rendering_window rendering_window (ref sw1, ref sw, hbox1) mktree))
766 ref (GMathView.math_view ~use_t1_lib:false ~width:400 ~height:380 ())
767 and label = GMisc.label ~text:"???" () in
768 let annotation_window = new annotation_window output label in
769 let rendering_window = new rendering_window annotation_window output label in
770 let theory_rendering_window = new theory_rendering_window rendering_window in
771 let selection_window =
772 new selection_window theory_rendering_window rendering_window
774 selection_window#show () ;