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 exception GtkInterfaceInternalError;;
 113
 114 let theory_get_current_uri () =
 115  match !theory_visited_uris with
 116     [] -> raise NoCurrentUri
 117   | uri::_ -> uri
 118 ;;
 119
 120 let get_current_uri () =
 121  match !visited_uris with
 122     [] -> raise NoCurrentUri
 123   | uri::_ -> uri
 124 ;;
 125
 126 let get_annotated_obj () =
 127  match !annotated_obj with
 128     None   ->
 129      let (annobj, ids_to_targets,_) =
 130       (CicCache.get_annobj (get_current_uri ()))
 131      in
 132       annotated_obj := Some (annobj, ids_to_targets) ;
 133       (annobj, ids_to_targets)
 134   | Some annobj -> annobj
 135 ;;
 136
 137 let filename_of_uri uri =
 138  Getter.get uri
 139 ;;
 140
 141 let theory_update_output rendering_window uri =
 142  rendering_window#label#set_text (UriManager.string_of_uri uri) ;
 143  ignore (rendering_window#errors#delete_text 0 rendering_window#errors#length) ;
 144   let mmlfile = XsltProcessor.process uri true "theory" in
 145    rendering_window#output#load mmlfile
 146 ;;
 147
 148 let update_output rendering_window uri =
 149  rendering_window#label#set_text (UriManager.string_of_uri uri) ;
 150  ignore (rendering_window#errors#delete_text 0 rendering_window#errors#length) ;
 151   let mmlfile = XsltProcessor.process uri true "cic" in
 152    rendering_window#output#load mmlfile
 153 ;;
 154
 155 let theory_next rendering_window () =
 156  match !theory_to_visit_uris with
 157     [] -> raise NoNextOrPrevUri
 158   | uri::tl ->
 159      theory_to_visit_uris := tl ;
 160      theory_visited_uris := uri::!theory_visited_uris ;
 161      theory_update_output rendering_window uri ;
 162      rendering_window#prevb#misc#set_sensitive true ;
 163      if tl = [] then
 164       rendering_window#nextb#misc#set_sensitive false
 165 ;;
 166
 167 let next rendering_window () =
 168  match !to_visit_uris with
 169     [] -> raise NoNextOrPrevUri
 170   | uri::tl ->
 171      to_visit_uris := tl ;
 172      visited_uris := uri::!visited_uris ;
 173      annotated_obj := None ;
 174      update_output rendering_window uri ;
 175      rendering_window#prevb#misc#set_sensitive true ;
 176      if tl = [] then
 177       rendering_window#nextb#misc#set_sensitive false
 178 ;;
 179
 180 let theory_prev rendering_window () =
 181  match !theory_visited_uris with
 182     [] -> raise NoCurrentUri
 183   | [_] -> raise NoNextOrPrevUri
 184   | uri::(uri'::tl as newvu) ->
 185      theory_visited_uris := newvu ;
 186      theory_to_visit_uris := uri::!theory_to_visit_uris ;
 187      theory_update_output rendering_window uri' ;
 188      rendering_window#nextb#misc#set_sensitive true ;
 189      if tl = [] then
 190       rendering_window#prevb#misc#set_sensitive false
 191 ;;
 192
 193 let prev rendering_window () =
 194  match !visited_uris with
 195     [] -> raise NoCurrentUri
 196   | [_] -> raise NoNextOrPrevUri
 197   | uri::(uri'::tl as newvu) ->
 198      visited_uris := newvu ;
 199      to_visit_uris := uri::!to_visit_uris ;
 200      annotated_obj := None ;
 201      update_output rendering_window uri' ;
 202      rendering_window#nextb#misc#set_sensitive true ;
 203      if tl = [] then
 204       rendering_window#prevb#misc#set_sensitive false
 205 ;;
 206
 207 (* called when an hyperlink is clicked *)
 208 let jump rendering_window s =
 209  let uri = UriManager.uri_of_string s in
 210   rendering_window#show () ;
 211   rendering_window#prevb#misc#set_sensitive true ;
 212   rendering_window#nextb#misc#set_sensitive false ;
 213   visited_uris := uri::!visited_uris ;
 214   to_visit_uris := [] ;
 215   annotated_obj := None ;
 216   update_output rendering_window uri
 217 ;;
 218
 219 let changefont rendering_window () =
 220  rendering_window#output#set_font_size rendering_window#spinb#value_as_int
 221 ;;
 222
 223
 224 let theory_selection_changed rendering_window uri () =
 225  match uri with
 226     None -> ()
 227   | Some uri' ->
 228      if !theory_visited_uris <> [] then
 229       rendering_window#prevb#misc#set_sensitive true ;
 230      rendering_window#nextb#misc#set_sensitive false ;
 231      theory_visited_uris := uri'::!theory_visited_uris ;
 232      theory_to_visit_uris := [] ;
 233      rendering_window#show () ;
 234      theory_update_output rendering_window uri'
 235 ;;
 236
 237 let selection_changed rendering_window uri () =
 238  match uri with
 239     None -> ()
 240   | Some uri' ->
 241      if !visited_uris <> [] then
 242       rendering_window#prevb#misc#set_sensitive true ;
 243      rendering_window#nextb#misc#set_sensitive false ;
 244      visited_uris := uri'::!visited_uris ;
 245      to_visit_uris := [] ;
 246      annotated_obj := None ;
 247      rendering_window#show () ;
 248      update_output rendering_window uri'
 249 ;;
 250
 251 (* CSC: unificare con la creazione la prima volta *)
 252 let rec updateb_pressed theory_rendering_window rendering_window
 253  (sw1, sw ,(hbox : GPack.box)) mktree ()
 254 =
 255  Getter.update () ;
 256  (* let's empty the uri trees and rebuild them *)
 257  uritree := [] ;
 258  theoryuritree := [] ;
 259  build_uri_tree () ;
 260  hbox#remove !sw1#coerce ;
 261  hbox#remove !sw#coerce ;
 262
 263  let sw3 =
 264   GBin.scrolled_window ~width:250 ~height:600
 265    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 266  let tree1 =
 267   GTree.tree ~selection_mode:`BROWSE ~packing:sw3#add_with_viewport () in
 268  let tree_item1 = GTree.tree_item ~label:"theory:/" ~packing:tree1#append () in
 269   sw1 := sw3 ;
 270   ignore(tree_item1#connect#select
 271    (theory_selection_changed theory_rendering_window None)) ;
 272   mktree theory_selection_changed theory_rendering_window tree_item1
 273    (Dir ("theory:/",theoryuritree)) ;
 274
 275  let sw2 =
 276   GBin.scrolled_window ~width:250 ~height:600
 277    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 278  let tree =
 279   GTree.tree ~selection_mode:`BROWSE ~packing:sw2#add_with_viewport () in
 280  let tree_item = GTree.tree_item ~label:"cic:/" ~packing:tree#append () in
 281   sw := sw2 ;
 282   ignore(tree_item#connect#select (selection_changed rendering_window None)) ;
 283   mktree selection_changed rendering_window tree_item (Dir ("cic:/",uritree))
 284 ;;
 285
 286 let theory_check rendering_window () =
 287   let output =
 288   try
 289    TheoryTypeChecker.typecheck (theory_get_current_uri ());
 290    "Type Checking was successful"
 291   with
 292    TheoryTypeChecker.NotWellTyped s ->
 293     "Type Checking was NOT successful:\n\t" ^ s
 294  in
 295   (* next "cast" can't got rid of, but I don't know why *)
 296   let errors = (rendering_window#errors : GEdit.text) in
 297   let _ = errors#delete_text 0 errors#length  in
 298    errors#insert output
 299 ;;
 300
 301 let check rendering_window () =
 302   let output =
 303   try
 304    CicTypeChecker.typecheck (get_current_uri ());
 305    "Type Checking was successful"
 306   with
 307    CicTypeChecker.NotWellTyped s -> "Type Checking was NOT successful:\n\t" ^ s
 308  in
 309   (* next "cast" can't got rid of, but I don't know why *)
 310   let errors = (rendering_window#errors : GEdit.text) in
 311   let _ = errors#delete_text 0 errors#length  in
 312    errors#insert output
 313 ;;
 314
 315 let annotateb_pressed rendering_window annotation_window () =
 316  let xpath = (rendering_window#output#get_selection : string option) in
 317   match xpath with
 318      None -> (rendering_window#errors : GEdit.text)#insert "\nNo selection!\n"
 319    | Some xpath ->
 320     try
 321      let annobj = get_annotated_obj ()
 322      (* next "cast" can't got rid of, but I don't know why *)
 323      and annotation = (annotation_window#annotation : GEdit.text) in
 324       ann := CicXPath.get_annotation annobj xpath ;
 325       CicAnnotationHinter.create_hints annotation_window annobj xpath ;
 326       annotation#delete_text 0 annotation#length ;
 327       begin
 328        match !(!ann) with
 329            None      ->
 330             annotation#misc#set_sensitive false ;
 331             annotation_window#radio_none#set_active true ;
 332             radio_some_status := false
 333          | Some ann' ->
 334             annotation#insert ann' ;
 335             annotation#misc#set_sensitive true ;
 336             annotation_window#radio_some#set_active true ;
 337             radio_some_status := true
 338       end ;
 339       GMain.Grab.add (annotation_window#window_to_annotate#coerce) ;
 340       annotation_window#show () ;
 341     with
 342       e ->
 343        (* next "cast" can't got rid of, but I don't know why *)
 344        let errors = (rendering_window#errors : GEdit.text) in
 345         errors#insert ("\n" ^ Printexc.to_string e ^ "\n")
 346 ;;
 347
 348 (* called when the annotation is confirmed *)
 349 let save_annotation annotation =
 350  if !radio_some_status then
 351   !ann := Some (annotation#get_chars 0 annotation#length)
 352  else
 353   !ann := None ;
 354  match !annotated_obj with
 355     None -> raise GtkInterfaceInternalError
 356   | Some (annobj,_) ->
 357      let uri = get_current_uri () in
 358       let annxml = Annotation2Xml.pp_annotation annobj uri in
 359        Xml.pp annxml (Some (fst (Getter.get_ann_file_name_and_uri uri)))
 360 ;;
 361
 362 let parse_no_cache uri =
 363  let module U = UriManager in
 364   XsltProcessor.process uri false "cic"
 365 ;;
 366
 367
 368 (* STUFF TO BUILD THE GTK INTERFACE *)
 369
 370 (* Stuff to build the tree window *)
 371
 372 (* selection_changed is actually selection_changed or theory_selection_changed*)
 373 let mktree selection_changed rendering_window =
 374  let rec aux treeitem =
 375   function
 376      Dir (dirname, content) ->
 377       let subtree = GTree.tree () in
 378        treeitem#set_subtree subtree ;
 379         List.iter
 380          (fun ti ->
 381            let label = get_name ti
 382            and uri = get_uri ti in
 383             let treeitem2 = GTree.tree_item ~label:label () in
 384              subtree#append treeitem2 ;
 385              ignore(treeitem2#connect#select
 386               (selection_changed rendering_window uri)) ;
 387              aux treeitem2 ti
 388          ) !content
 389    | _ -> ()
 390  in
 391   aux
 392 ;;
 393
 394 class annotation_window output label =
 395  let window_to_annotate =
 396   GWindow.window ~title:"Annotating environment" ~border_width:2 () in
 397  let hbox1 =
 398   GPack.hbox ~packing:window_to_annotate#add () in
 399  let vbox1 =
 400   GPack.vbox ~packing:(hbox1#pack ~padding:5) () in
 401  let hbox2 =
 402   GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
 403  let radio_some = GButton.radio_button ~label:"Annotation below"
 404   ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
 405  let radio_none = GButton.radio_button ~label:"No annotation"
 406   ~group:radio_some#group
 407   ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5)
 408   ~active:true () in
 409  let annotation = GEdit.text ~editable:true ~width:400 ~height:180
 410   ~packing:(vbox1#pack ~padding:5) () in
 411  let table =
 412   GPack.table ~rows:3 ~columns:3 ~packing:(vbox1#pack ~padding:5) () in
 413  let annotation_hints =
 414   Array.init 9
 415    (function i ->
 416      GButton.button ~label:("Hint " ^ string_of_int i)
 417       ~packing:(table#attach ~left:(i mod 3) ~top:(i / 3)) ()
 418    ) in
 419  let vbox2 =
 420   GPack.vbox ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
 421  let confirmb =
 422   GButton.button ~label:"O.K."
 423    ~packing:(vbox2#pack ~expand:false ~fill:false ~padding:5) () in
 424  let abortb =
 425   GButton.button ~label:"Abort"
 426    ~packing:(vbox2#pack ~expand:false ~fill:false ~padding:5) () in
 427 object (self)
 428  method window_to_annotate = window_to_annotate
 429  method annotation = annotation
 430  method radio_some = radio_some
 431  method radio_none = radio_none
 432  method annotation_hints = annotation_hints
 433  method output = (output : GMathView.math_view)
 434  method show () = window_to_annotate#show ()
 435  initializer
 436   (* signal handlers here *)
 437   ignore (window_to_annotate#event#connect#delete
 438    (fun _ ->
 439      window_to_annotate#misc#hide () ;
 440      GMain.Grab.remove (window_to_annotate#coerce) ;
 441      true
 442    )) ;
 443   ignore (confirmb#connect#clicked
 444    (fun () ->
 445      window_to_annotate#misc#hide () ;
 446      save_annotation annotation ;
 447      GMain.Grab.remove (window_to_annotate#coerce) ;
 448      let new_current_uri =
 449       (snd (Getter.get_ann_file_name_and_uri (get_current_uri ())))
 450      in
 451       visited_uris := new_current_uri::(List.tl !visited_uris) ;
 452        label#set_text (UriManager.string_of_uri new_current_uri) ;
 453        output#load (parse_no_cache new_current_uri)
 454    )) ;
 455   ignore (abortb#connect#clicked
 456    (fun () ->
 457      window_to_annotate#misc#hide () ;
 458      GMain.Grab.remove (window_to_annotate#coerce)
 459    ));
 460   ignore (radio_some#connect#clicked
 461    (fun () -> annotation#misc#set_sensitive true ; radio_some_status := true)) ;
 462   ignore (radio_none #connect#clicked
 463    (fun () ->
 464      annotation#misc#set_sensitive false;
 465      radio_some_status := false)
 466    )
 467 end;;
 468
 469 class rendering_window annotation_window output (label : GMisc.label) =
 470  let window =
 471   GWindow.window ~title:"MathML viewer" ~border_width:2 () in
 472  let vbox =
 473   GPack.vbox ~packing:window#add () in
 474  let _ = vbox#pack ~expand:false ~fill:false ~padding:5 label#coerce in
 475  let paned =
 476   GPack.paned `HORIZONTAL ~packing:(vbox#pack ~padding:5) () in
 477  let scrolled_window0 =
 478   GBin.scrolled_window ~border_width:10 ~packing:paned#add1 () in
 479  let _ = scrolled_window0#add output#coerce in
 480  let scrolled_window =
 481   GBin.scrolled_window
 482    ~border_width:10 ~packing:paned#add2 ~width:240 ~height:100 () in
 483  let errors = GEdit.text ~packing:scrolled_window#add_with_viewport () in
 484  let hbox =
 485   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
 486  let prevb =
 487   GButton.button ~label:"Prev"
 488    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 489  let nextb =
 490   GButton.button ~label:"Next"
 491    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 492  let checkb =
 493   GButton.button ~label:"Check"
 494    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 495  let annotateb =
 496   GButton.button ~label:"Annotate"
 497    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 498  let spinb =
 499   let sadj =
 500    GData.adjustment ~value:14.0 ~lower:5.0 ~upper:50.0 ~step_incr:1.0 ()
 501   in
 502    GEdit.spin_button
 503     ~adjustment:sadj ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5)
 504     () in
 505  let closeb =
 506   GButton.button ~label:"Close"
 507    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 508 object(self)
 509  method nextb = nextb
 510  method prevb = prevb
 511  method label = label
 512  method spinb = spinb
 513  method output = (output : GMathView.math_view)
 514  method errors = errors
 515  method show () = window#show ()
 516  initializer
 517   nextb#misc#set_sensitive false ;
 518   prevb#misc#set_sensitive false ;
 519
 520   (* signal handlers here *)
 521   ignore(output#connect#jump (jump self)) ;
 522   ignore(nextb#connect#clicked (next self)) ;
 523   ignore(prevb#connect#clicked (prev self)) ;
 524   ignore(checkb#connect#clicked (check self)) ;
 525   ignore(spinb#connect#changed (changefont self)) ;
 526   ignore(closeb#connect#clicked window#misc#hide) ;
 527   ignore(annotateb#connect#clicked (annotateb_pressed self annotation_window)) ;
 528   ignore(window#event#connect#delete (fun _ -> window#misc#hide () ; true ))
 529 end;;
 530
 531 class theory_rendering_window rendering_window =
 532  let window =
 533   GWindow.window ~title:"MathML theory viewer" ~border_width:2 () in
 534  let vbox =
 535   GPack.vbox ~packing:window#add () in
 536  let label =
 537   GMisc.label ~text:"???"
 538    ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
 539  let paned =
 540   GPack.paned `HORIZONTAL ~packing:(vbox#pack ~padding:5) () in
 541  let scrolled_window0 =
 542   GBin.scrolled_window ~border_width:10 ~packing:paned#add1 () in
 543  let output =
 544   GMathView.math_view ~width:400 ~height:380 ~packing:scrolled_window0#add () in
 545  let scrolled_window =
 546   GBin.scrolled_window
 547    ~border_width:10 ~packing:paned#add2 ~width:240 ~height:100 () in
 548  let errors = GEdit.text ~packing:scrolled_window#add_with_viewport () in
 549  let hbox =
 550   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
 551  let prevb =
 552   GButton.button ~label:"Prev"
 553    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 554  let nextb =
 555   GButton.button ~label:"Next"
 556    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 557  let checkb =
 558   GButton.button ~label:"Check"
 559    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 560  let spinb =
 561   let sadj =
 562    GData.adjustment ~value:14.0 ~lower:5.0 ~upper:50.0 ~step_incr:1.0 ()
 563   in
 564    GEdit.spin_button
 565     ~adjustment:sadj ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5)
 566     () in
 567  let closeb =
 568   GButton.button ~label:"Close"
 569    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 570 object(self)
 571  method nextb = nextb
 572  method prevb = prevb
 573  method label = label
 574  method output = (output : GMathView.math_view)
 575  method errors = errors
 576  method spinb = spinb
 577  method show () = window#show ()
 578  initializer
 579   nextb#misc#set_sensitive false ;
 580   prevb#misc#set_sensitive false ;
 581
 582   (* signal handlers here *)
 583   ignore(output#connect#jump (jump rendering_window)) ;
 584   ignore(nextb#connect#clicked (theory_next self)) ;
 585   ignore(prevb#connect#clicked (theory_prev self)) ;
 586   ignore(checkb#connect#clicked (theory_check self)) ;
 587   ignore(spinb#connect#changed (changefont self)) ;
 588   ignore(closeb#connect#clicked window#misc#hide) ;
 589   ignore(window#event#connect#delete (fun _ -> window#misc#hide () ; true ))
 590 end;;
 591
 592 (* CSC: fare in modo che i due alberi vengano svuotati invece che distrutti *)
 593 class selection_window theory_rendering_window rendering_window =
 594   let label = "cic:/" in
 595   let theorylabel = "theory:/" in
 596   let win = GWindow.window ~title:"Known uris" ~border_width:2 () in
 597   let vbox = GPack.vbox ~packing:win#add () in
 598   let hbox1 = GPack.hbox ~packing:(vbox#pack ~padding:5) () in
 599   let sw1 = GBin.scrolled_window ~width:250 ~height:600
 600    ~packing:(hbox1#pack ~padding:5) () in
 601   let tree1 =
 602    GTree.tree ~selection_mode:`BROWSE ~packing:sw1#add_with_viewport () in
 603   let tree_item1 =
 604    GTree.tree_item ~label:theorylabel ~packing:tree1#append () in
 605   let sw = GBin.scrolled_window ~width:250 ~height:600
 606    ~packing:(hbox1#pack ~padding:5) () in
 607   let tree =
 608    GTree.tree ~selection_mode:`BROWSE ~packing:sw#add_with_viewport () in
 609   let tree_item =
 610    GTree.tree_item ~label:label ~packing:tree#append () in
 611   let hbox =
 612    GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
 613   let updateb =
 614    GButton.button ~label:"Update"
 615     ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 616   let quitb =
 617    GButton.button ~label:"Quit"
 618     ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 619 object (self)
 620   method show () = win#show ()
 621   initializer
 622     mktree theory_selection_changed theory_rendering_window tree_item1
 623      (Dir ("theory:/",theoryuritree));
 624     mktree selection_changed rendering_window tree_item
 625      (Dir ("cic:/",uritree));
 626
 627     (* signal handlers here *)
 628     ignore (tree_item1#connect#select
 629      ~callback:(theory_selection_changed theory_rendering_window None)) ;
 630     ignore (tree_item#connect#select
 631      ~callback:(selection_changed rendering_window None)) ;
 632     ignore (win#connect#destroy ~callback:GMain.Main.quit) ;
 633     ignore (quitb#connect#clicked GMain.Main.quit) ;
 634     ignore(updateb#connect#clicked (updateb_pressed
 635      theory_rendering_window rendering_window (ref sw1, ref sw, hbox1) mktree))
 636 end;;
 637
 638
 639 (* MAIN *)
 640
 641 let _ =
 642  build_uri_tree () ;
 643  let output = GMathView.math_view ~width:400 ~height:380 ()
 644  and label = GMisc.label ~text:"???" () in
 645   let annotation_window = new annotation_window output label in
 646   let rendering_window = new rendering_window annotation_window output label in
 647   let theory_rendering_window = new theory_rendering_window rendering_window in
 648   let selection_window =
 649    new selection_window theory_rendering_window rendering_window
 650   in
 651    selection_window#show () ;
 652    GMain.Main.main ()
 653 ;;