]> matita.cs.unibo.it Git - helm.git/blob - helm/interface/mmlinterface.ml
Requires and Provides now fixed
[helm.git] / helm / interface / mmlinterface.ml
1 (******************************************************************************)
2 (*                                                                            *)
3 (*                               PROJECT HELM                                 *)
4 (*                                                                            *)
5 (*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
6 (*                                 24/01/2000                                 *)
7 (*                                                                            *)
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        *)
17 (* recomputed                                                                 *)
18 (*                                                                            *)
19 (******************************************************************************)
20
21 (* DEFINITION OF THE URI TREE AND USEFUL FUNCTIONS ON IT *)
22
23 type item =
24    Dir of string * item list ref
25  | File of string * UriManager.uri
26 ;;
27
28 let uritree = ref []
29 let theoryuritree = ref []
30
31 let get_name =
32  function
33     Dir (name,_) -> name
34   | File (name,_) -> name
35 ;;
36
37 let get_uri =
38  function
39     Dir _ -> None
40   | File (_,uri) -> Some uri
41 ;;
42
43 (* STUFF TO BUILD THE URI TREE *)
44
45 exception EmptyUri
46 exception DuplicatedUri
47 exception ConflictingUris
48
49 let insert_in_uri_tree uri =
50  let rec aux l =
51   function
52      [name] ->
53       (try
54         let _ = List.find (fun item -> name = get_name item) !l in
55          raise DuplicatedUri
56        with
57         Not_found -> l := (File (name,uri))::!l
58       )
59    | name::tl ->
60       (try
61         match List.find (fun item -> name = get_name item) !l with
62            Dir (_,children) -> aux children tl
63          | File _ -> raise ConflictingUris
64        with
65         Not_found ->
66          let children = ref [] in
67           l := (Dir (name,children))::!l ;
68           aux children tl
69       )
70    | [] -> raise EmptyUri
71  in
72   aux
73 ;;
74
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
78    Dbm.iter 
79     (fun uri _ ->
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
90     ) dbh ;
91    Dbm.close dbh
92 ;;
93
94 (* GLOBAL REFERENCES (USED BY CALLBACKS) *)
95
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? *)
102
103 let theory_visited_uris = ref [];;
104 let theory_to_visit_uris = ref [];;
105 let visited_uris = ref [];;
106 let to_visit_uris = ref [];;
107
108 (* CALLBACKS *)
109
110 exception NoCurrentUri;;
111 exception NoNextOrPrevUri;;
112
113 let theory_get_current_uri () =
114  match !theory_visited_uris with
115     [] -> raise NoCurrentUri
116   | uri::_ -> uri
117 ;;
118
119 let get_current_uri () =
120  match !visited_uris with
121     [] -> raise NoCurrentUri
122   | uri::_ -> uri
123 ;;
124
125 let get_annotated_obj () =
126  match !annotated_obj with
127     None   ->
128      let (annobj, ids_to_targets,_) =
129       (CicCache.get_annobj (get_current_uri ()))
130      in
131       annotated_obj := Some (annobj, ids_to_targets) ;
132       (annobj, ids_to_targets)
133   | Some annobj -> annobj
134 ;;
135
136 let filename_of_uri uri =
137  Getter.get uri
138 ;;
139
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
145 ;;
146
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
152 ;;
153
154 let theory_next rendering_window () =
155  match !theory_to_visit_uris with
156     [] -> raise NoNextOrPrevUri
157   | uri::tl ->
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 ;
162      if tl = [] then
163       rendering_window#nextb#misc#set_sensitive false
164 ;;
165
166 let next rendering_window () =
167  match !to_visit_uris with
168     [] -> raise NoNextOrPrevUri
169   | uri::tl ->
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 ;
175      if tl = [] then
176       rendering_window#nextb#misc#set_sensitive false
177 ;;
178
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 ;
188      if tl = [] then
189       rendering_window#prevb#misc#set_sensitive false
190 ;;
191
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 ;
202      if tl = [] then
203       rendering_window#prevb#misc#set_sensitive false
204 ;;
205
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
210     Some str ->
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
221 ;;
222
223 let choose_selection rendering_window (node : Ominidom.o_mDOMNode option) =
224  let module O = Ominidom in
225   let rec aux node =
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)
229   in
230    match node with
231      Some x -> aux x
232    | None   -> rendering_window#output#set_selection None
233 ;;
234
235
236 let theory_selection_changed rendering_window uri () =
237  match uri with
238     None -> ()
239   | Some 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'
247 ;;
248
249 let selection_changed rendering_window uri () =
250  match uri with
251     None -> ()
252   | Some 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'
261 ;;
262
263 let create_gtk_trees (hbox : GPack.box) rendering_window theory_rendering_window mktree =
264  let sw3 =
265   GBin.scrolled_window ~width:250 ~height:600
266    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
267  let tree1 =
268   GTree.tree ~selection_mode:`BROWSE ~packing:sw3#add_with_viewport () in
269  let tree_item1 = GTree.tree_item ~label:"theory:/" ~packing:tree1#append () in
270
271  let sw2 =
272   GBin.scrolled_window ~width:250 ~height:600
273    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
274  let tree =
275   GTree.tree ~selection_mode:`BROWSE ~packing:sw2#add_with_viewport () in
276  let tree_item = GTree.tree_item ~label:"cic:/" ~packing:tree#append () in
277
278   ignore(tree_item#connect#select (selection_changed rendering_window None)) ;
279   mktree selection_changed rendering_window tree_item (Dir ("cic:/",uritree)) ;
280
281   ignore(tree_item1#connect#select
282    (theory_selection_changed theory_rendering_window None)) ;
283   mktree theory_selection_changed theory_rendering_window tree_item1
284    (Dir ("theory:/",theoryuritree)) ;
285   (sw3,sw2)
286 ;;
287
288 let updateb_pressed theory_rendering_window rendering_window
289  (sw1, sw ,(hbox : GPack.box)) mktree ()
290 =
291  Getter.update () ;
292  (* let's empty the uri trees and rebuild them *)
293  uritree := [] ;
294  theoryuritree := [] ;
295  build_uri_tree () ;
296  hbox#remove !sw1#coerce ;
297  hbox#remove !sw#coerce ;
298  let (sw3,sw2) =
299   create_gtk_trees hbox rendering_window theory_rendering_window mktree
300  in
301   sw1 := sw3 ;
302   sw := sw2
303 ;;
304
305 let theory_check rendering_window () =
306   let output =
307   try
308    TheoryTypeChecker.typecheck (theory_get_current_uri ());
309    "Type Checking was successful"
310   with
311    TheoryTypeChecker.NotWellTyped s ->
312     "Type Checking was NOT successful:\n\t" ^ s
313  in
314   (* next "cast" can't got rid of, but I don't know why *)
315   let errors = (rendering_window#errors : GEdit.text) in
316   let _ = errors#delete_text 0 errors#length  in
317    errors#insert output
318 ;;
319
320 let check rendering_window () =
321   let output =
322   try
323    CicTypeChecker.typecheck (get_current_uri ());
324    "Type Checking was successful"
325   with
326    CicTypeChecker.NotWellTyped s -> "Type Checking was NOT successful:\n\t" ^ s
327  in
328   (* next "cast" can't got rid of, but I don't know why *)
329   let errors = (rendering_window#errors : GEdit.text) in
330   let _ = errors#delete_text 0 errors#length  in
331    errors#insert output
332 ;;
333
334 let annotateb_pressed rendering_window annotation_window () =
335  let module O = Ominidom in
336  match rendering_window#output#get_selection with
337  | Some node ->
338   begin
339    match (node#get_attribute (O.o_mDOMString_of_string "xref")) with
340    | Some xpath ->
341      let annobj = get_annotated_obj ()
342      (* next "cast" can't got rid of, but I don't know why *)
343      and annotation = (annotation_window#annotation : GEdit.text) in
344       ann := CicXPath.get_annotation annobj (xpath#get_string) ;
345       CicAnnotationHinter.create_hints annotation_window annobj (xpath#get_string) ;
346       annotation#delete_text 0 annotation#length ;
347       begin
348        match !(!ann) with
349            None      ->
350             annotation#misc#set_sensitive false ;
351             annotation_window#radio_none#set_active true ;
352             radio_some_status := false
353          | Some ann' ->
354             annotation#insert ann' ;
355             annotation#misc#set_sensitive true ;
356             annotation_window#radio_some#set_active true ;
357             radio_some_status := true
358       end ;
359       GMain.Grab.add (annotation_window#window_to_annotate#coerce) ;
360       annotation_window#show () ;
361    | None ->
362        (* next "cast" can't got rid of, but I don't know why *)
363        let errors = (rendering_window#errors : GEdit.text) in
364         errors#insert ("\nNo xref found\n")
365   end
366  | None -> (rendering_window#errors : GEdit.text)#insert "\nNo selection!\n"
367 ;;
368
369 (* called when the annotation is confirmed *)
370 let save_annotation annotation =
371  if !radio_some_status then
372   !ann := Some (annotation#get_chars 0 annotation#length)
373  else
374   !ann := None ;
375  match !annotated_obj with
376     None -> assert false
377   | Some (annobj,_) ->
378      let uri = get_current_uri () in
379       let annxml = Annotation2Xml.pp_annotation annobj uri in
380        Xml.pp annxml (Some (fst (Getter.get_ann_file_name_and_uri uri)))
381 ;;
382
383 let parse_no_cache uri =
384  let module U = UriManager in
385   XsltProcessor.process uri false "cic"
386 ;;
387
388
389 (* STUFF TO BUILD THE GTK INTERFACE *)
390
391 (* Stuff to build the tree window *)
392
393 (* selection_changed is actually selection_changed or theory_selection_changed*)
394 let mktree selection_changed rendering_window =
395  let rec aux treeitem =
396   function
397      Dir (dirname, content) ->
398       let subtree = GTree.tree () in
399        treeitem#set_subtree subtree ;
400         let expand_sons =
401          List.map
402           (fun ti ->
403             let label = get_name ti
404             and uri = get_uri ti in
405              let treeitem2 = GTree.tree_item ~label:label () in
406               subtree#append treeitem2 ;
407               ignore(treeitem2#connect#select
408                (selection_changed rendering_window uri)) ;
409                (* Almost lazy function *)
410                (fun () -> aux treeitem2 ti)
411           ) (List.sort compare !content)
412         in
413          let lazy_expand_sons = lazy (List.iter (fun f -> f ()) expand_sons) in
414          ignore(treeitem#connect#expand
415           (fun () -> Lazy.force lazy_expand_sons)) ;
416    | _ -> ()
417  in
418   aux 
419 ;;
420
421 (* Stuff for the widget settings *)
422
423 let export_to_postscript (output : GMathView.math_view) () =
424  output#export_to_postscript ~filename:"output.ps" ();
425 ;;
426
427 let activate_t1 output button_set_anti_aliasing button_set_kerning 
428  button_export_to_postscript button_t1 ()
429 =
430  let is_set = button_t1#active in
431   output#set_font_manager_type
432    (if is_set then `font_manager_t1 else `font_manager_gtk) ;
433   if is_set then
434    begin
435     button_set_anti_aliasing#misc#set_sensitive true ;
436     button_set_kerning#misc#set_sensitive true ;
437     button_export_to_postscript#misc#set_sensitive true ;
438    end
439   else
440    begin
441     button_set_anti_aliasing#misc#set_sensitive false ;
442     button_set_kerning#misc#set_sensitive false ;
443     button_export_to_postscript#misc#set_sensitive false ;
444    end
445 ;;
446
447 let set_anti_aliasing output button_set_anti_aliasing () =
448  output#set_anti_aliasing button_set_anti_aliasing#active
449 ;;
450
451 let set_kerning output button_set_kerning () =
452  output#set_kerning button_set_kerning#active
453 ;;
454
455 let changefont output font_size_spinb () =
456  output#set_font_size font_size_spinb#value_as_int
457 ;;
458
459 let set_log_verbosity output log_verbosity_spinb () =
460  output#set_log_verbosity log_verbosity_spinb#value_as_int
461 ;;
462
463 class settings_window output sw button_export_to_postscript jump_callback
464  selection_changed_callback
465 =
466  let settings_window = GWindow.window ~title:"GtkMathView settings" () in
467  let vbox =
468   GPack.vbox ~packing:settings_window#add () in
469  let table =
470   GPack.table
471    ~rows:1 ~columns:3 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
472    ~border_width:5 ~packing:vbox#add () in
473  let button_t1 =
474   GButton.toggle_button ~label:"activate t1 fonts"
475    ~packing:(table#attach ~left:0 ~top:0) () in
476  let button_set_anti_aliasing =
477   GButton.toggle_button ~label:"set_anti_aliasing"
478    ~packing:(table#attach ~left:1 ~top:0) () in
479  let button_set_kerning =
480   GButton.toggle_button ~label:"set_kerning"
481    ~packing:(table#attach ~left:2 ~top:0) () in
482  let table =
483   GPack.table
484    ~rows:2 ~columns:2 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
485    ~border_width:5 ~packing:vbox#add () in
486  let font_size_label =
487   GMisc.label ~text:"font size:"
488    ~packing:(table#attach ~left:0 ~top:0 ~expand:`NONE) () in
489  let font_size_spinb =
490   let sadj =
491    GData.adjustment ~value:14.0 ~lower:5.0 ~upper:50.0 ~step_incr:1.0 ()
492   in
493    GEdit.spin_button 
494     ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:0 ~fill:`NONE) () in
495  let log_verbosity_label =
496   GMisc.label ~text:"log verbosity:"
497    ~packing:(table#attach ~left:0 ~top:1) () in
498  let log_verbosity_spinb =
499   let sadj =
500    GData.adjustment ~value:0.0 ~lower:0.0 ~upper:3.0 ~step_incr:1.0 ()
501   in
502    GEdit.spin_button 
503     ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:1) () in
504  let hbox =
505   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
506  let closeb =
507   GButton.button ~label:"Close"
508    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
509 object(self)
510  method show = settings_window#show
511  initializer
512   button_set_anti_aliasing#misc#set_sensitive false ;
513   button_set_kerning#misc#set_sensitive false ;
514   (* Signals connection *)
515   ignore(button_t1#connect#clicked
516    (activate_t1 output button_set_anti_aliasing button_set_kerning
517     button_export_to_postscript button_t1)) ;
518   ignore(font_size_spinb#connect#changed (changefont output font_size_spinb)) ;
519   ignore(button_set_anti_aliasing#connect#toggled
520    (set_anti_aliasing output button_set_anti_aliasing));
521   ignore(button_set_kerning#connect#toggled
522    (set_kerning output button_set_kerning)) ;
523   ignore(log_verbosity_spinb#connect#changed
524    (set_log_verbosity output log_verbosity_spinb)) ;
525   ignore(closeb#connect#clicked settings_window#misc#hide)
526 end;;
527
528 (* Main windows *)
529
530 class annotation_window output label =
531  let window_to_annotate =
532   GWindow.window ~title:"Annotating environment" ~border_width:2 () in
533  let hbox1 =
534   GPack.hbox ~packing:window_to_annotate#add () in
535  let vbox1 =
536   GPack.vbox ~packing:(hbox1#pack ~padding:5) () in
537  let hbox2 =
538   GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
539  let radio_some = GButton.radio_button ~label:"Annotation below"
540   ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
541  let radio_none = GButton.radio_button ~label:"No annotation"
542   ~group:radio_some#group
543   ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5)
544   ~active:true () in
545  let annotation = GEdit.text ~editable:true ~width:400 ~height:180
546   ~packing:(vbox1#pack ~padding:5) () in
547  let table =
548   GPack.table ~rows:3 ~columns:3 ~packing:(vbox1#pack ~padding:5) () in
549  let annotation_hints =
550   Array.init 9
551    (function i ->
552      GButton.button ~label:("Hint " ^ string_of_int i)
553       ~packing:(table#attach ~left:(i mod 3) ~top:(i / 3)) ()
554    ) in
555  let vbox2 =
556   GPack.vbox ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
557  let confirmb =
558   GButton.button ~label:"O.K."
559    ~packing:(vbox2#pack ~expand:false ~fill:false ~padding:5) () in
560  let abortb =
561   GButton.button ~label:"Abort"
562    ~packing:(vbox2#pack ~expand:false ~fill:false ~padding:5) () in
563 object (self)
564  method window_to_annotate = window_to_annotate
565  method annotation = annotation
566  method radio_some = radio_some
567  method radio_none = radio_none
568  method annotation_hints = annotation_hints
569  method output = (output : GMathView.math_view)
570  method show () = window_to_annotate#show ()
571  initializer
572   (* signal handlers here *)
573   ignore (window_to_annotate#event#connect#delete
574    (fun _ ->
575      window_to_annotate#misc#hide () ;
576      GMain.Grab.remove (window_to_annotate#coerce) ; 
577      true
578    )) ;
579   ignore (confirmb#connect#clicked
580    (fun () ->
581      window_to_annotate#misc#hide () ;
582      save_annotation annotation ;
583      GMain.Grab.remove (window_to_annotate#coerce) ;
584      let new_current_uri =
585       (snd (Getter.get_ann_file_name_and_uri (get_current_uri ())))
586      in
587       visited_uris := new_current_uri::(List.tl !visited_uris) ;
588        label#set_text (UriManager.string_of_uri new_current_uri) ;
589        let mmlfile = parse_no_cache new_current_uri in
590         output#load mmlfile
591    )) ;
592   ignore (abortb#connect#clicked
593    (fun () ->
594      window_to_annotate#misc#hide () ;
595      GMain.Grab.remove (window_to_annotate#coerce)
596    ));
597   ignore (radio_some#connect#clicked
598    (fun () -> annotation#misc#set_sensitive true ; radio_some_status := true)) ;
599   ignore (radio_none #connect#clicked
600    (fun () ->
601      annotation#misc#set_sensitive false;
602      radio_some_status := false)
603    )
604 end;;
605
606 class rendering_window annotation_window output (label : GMisc.label) =
607  let window =
608   GWindow.window ~title:"MathML viewer" ~border_width:2 () in
609  let vbox =
610   GPack.vbox ~packing:window#add () in
611  let _ = vbox#pack ~expand:false ~fill:false ~padding:5 label#coerce in
612  let paned =
613   GPack.paned `HORIZONTAL ~packing:(vbox#pack ~expand:true ~padding:5) () in
614  let scrolled_window0 =
615   GBin.scrolled_window ~border_width:10 ~packing:paned#add1 () in
616  let _ = scrolled_window0#add output#coerce in
617  let scrolled_window =
618   GBin.scrolled_window
619    ~border_width:10 ~packing:paned#add2 ~width:240 ~height:100 () in
620  let errors = GEdit.text ~packing:scrolled_window#add_with_viewport () in
621  let hbox =
622   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
623  let prevb =
624   GButton.button ~label:"Prev"
625    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
626  let nextb =
627   GButton.button ~label:"Next"
628    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
629  let checkb =
630   GButton.button ~label:"Check"
631    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
632  let annotateb =
633   GButton.button ~label:"Annotate"
634    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
635  let settingsb =
636   GButton.button ~label:"Settings"
637    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
638  let button_export_to_postscript =
639   GButton.button ~label:"export_to_postscript"
640   ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
641  let closeb =
642   GButton.button ~label:"Close"
643    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
644 object(self)
645  method nextb = nextb
646  method prevb = prevb
647  method label = label
648  method output = (output : GMathView.math_view)
649  method errors = errors
650  method show () = window#show ()
651  initializer
652   nextb#misc#set_sensitive false ;
653   prevb#misc#set_sensitive false ;
654   button_export_to_postscript#misc#set_sensitive false ;
655
656   (* signal handlers here *)
657   ignore(output#connect#jump (jump self)) ;
658   ignore(output#connect#selection_changed (choose_selection self)) ;
659   ignore(nextb#connect#clicked (next self)) ;
660   ignore(prevb#connect#clicked (prev self)) ;
661   ignore(checkb#connect#clicked (check self)) ;
662   ignore(closeb#connect#clicked window#misc#hide) ;
663   ignore(annotateb#connect#clicked (annotateb_pressed self annotation_window)) ;
664   let settings_window = new settings_window output scrolled_window0
665    button_export_to_postscript (jump self) (choose_selection self) in
666   ignore(settingsb#connect#clicked settings_window#show) ;
667   ignore(button_export_to_postscript#connect#clicked (export_to_postscript output)) ;
668   ignore(window#event#connect#delete (fun _ -> window#misc#hide () ; true ))
669 end;;
670
671 class theory_rendering_window rendering_window =
672  let window =
673   GWindow.window ~title:"MathML theory viewer" ~border_width:2 () in
674  let vbox =
675   GPack.vbox ~packing:window#add () in
676  let label =
677   GMisc.label ~text:"???"
678    ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
679  let paned =
680   GPack.paned `HORIZONTAL ~packing:(vbox#pack ~expand:true ~padding:5) () in
681  let scrolled_window0 =
682   GBin.scrolled_window ~border_width:10 ~packing:paned#add1 () in
683  let output =
684   GMathView.math_view ~width:400 ~height:380 ~packing:scrolled_window0#add () in
685  let scrolled_window =
686   GBin.scrolled_window
687    ~border_width:10 ~packing:paned#add2 ~width:240 ~height:100 () in
688  let errors = GEdit.text ~packing:scrolled_window#add_with_viewport () in
689  let hbox =
690   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
691  let prevb =
692   GButton.button ~label:"Prev"
693    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
694  let nextb =
695   GButton.button ~label:"Next"
696    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
697  let checkb =
698   GButton.button ~label:"Check"
699    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
700  let settingsb =
701   GButton.button ~label:"Settings"
702    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
703  let button_export_to_postscript =
704   GButton.button ~label:"export_to_postscript"
705   ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
706  let closeb =
707   GButton.button ~label:"Close"
708    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
709 object(self)
710  method nextb = nextb
711  method prevb = prevb
712  method label = label
713  method output = (output : GMathView.math_view)
714  method errors = errors
715  method show () = window#show ()
716  initializer
717   nextb#misc#set_sensitive false ;
718   prevb#misc#set_sensitive false ;
719   button_export_to_postscript#misc#set_sensitive false ;
720
721   (* signal handlers here *)
722   ignore(output#connect#jump (jump rendering_window)) ;
723   ignore(output#connect#selection_changed (choose_selection self)) ;
724   ignore(nextb#connect#clicked (theory_next self)) ;
725   ignore(prevb#connect#clicked (theory_prev self)) ;
726   ignore(checkb#connect#clicked (theory_check self)) ;
727   let settings_window = new settings_window output scrolled_window0
728    button_export_to_postscript (jump rendering_window)(choose_selection self) in
729   ignore(settingsb#connect#clicked settings_window#show) ;
730   ignore(button_export_to_postscript#connect#clicked (export_to_postscript output)) ;
731   ignore(closeb#connect#clicked window#misc#hide) ;
732   ignore(window#event#connect#delete (fun _ -> window#misc#hide () ; true ))
733 end;;
734
735 (* CSC: fare in modo che i due alberi vengano svuotati invece che distrutti *)
736 class selection_window theory_rendering_window rendering_window =
737   let label = "cic:/" in
738   let theorylabel = "theory:/" in
739   let win = GWindow.window ~title:"Known uris" ~border_width:2 () in
740   let vbox = GPack.vbox ~packing:win#add () in
741   let hbox1 = GPack.hbox ~packing:(vbox#pack ~padding:5) () in
742   let (sw1,sw) =
743    create_gtk_trees hbox1 rendering_window theory_rendering_window mktree
744   in
745   let hbox =
746    GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
747   let updateb =
748    GButton.button ~label:"Update"
749     ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
750   let quitb =
751    GButton.button ~label:"Quit"
752     ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
753 object (self)
754   method show () = win#show ()
755   initializer
756     (* signal handlers here *)
757     ignore (win#connect#destroy ~callback:GMain.Main.quit) ;
758     ignore (quitb#connect#clicked GMain.Main.quit) ;
759     ignore(updateb#connect#clicked (updateb_pressed
760      theory_rendering_window rendering_window (ref sw1, ref sw, hbox1) mktree))
761 end;;
762
763
764 (* MAIN *)
765
766 let _ =
767  build_uri_tree () ;
768  let output = GMathView.math_view ~width:400 ~height:380 ()
769  and label = GMisc.label ~text:"???" () in
770   let annotation_window = new annotation_window output label in
771   let rendering_window = new rendering_window annotation_window output label in
772   let theory_rendering_window = new theory_rendering_window rendering_window in
773   let selection_window =
774    new selection_window theory_rendering_window rendering_window
775   in
776    selection_window#show () ;
777    GMain.Main.main ()
778 ;;