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 ;;