helm/interface/mmlinterface.ml

   1 (* Copyright (C) 2000, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://cs.unibo.it/helm/.
  24  *)
  25
  26 (******************************************************************************)
  27 (*                                                                            *)
  28 (*                               PROJECT HELM                                 *)
  29 (*                                                                            *)
  30 (*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
  31 (*                                 24/01/2000                                 *)
  32 (*                                                                            *)
  33 (* This is a simple gtk interface to the Coq-like pretty printer cicPp for    *)
  34 (* cic terms exported in xml. It uses directly the modules cicPp and          *)
  35 (* cicCcache and indirectly all the other modules (cicParser, cicParser2,     *)
  36 (* cicParser3, getter).                                                       *)
  37 (* The syntax is  "gtkInterface[.opt] filename1 ... filenamen" where          *)
  38 (* filenamei is the path-name of an xml file describing a cic term.           *)
  39 (* The terms are loaded in cache and then pretty-printed one at a time and    *)
  40 (* only once, when the user wants to look at it: if the user wants to look at *)
  41 (* a term again, then the pretty-printed term is showed again, but not        *)
  42 (* recomputed                                                                 *)
  43 (*                                                                            *)
  44 (******************************************************************************)
  45
  46 (* DEFINITION OF THE URI TREE AND USEFUL FUNCTIONS ON IT *)
  47
  48 type item =
  49    Dir of string * item list ref
  50  | File of string * UriManager.uri
  51 ;;
  52
  53 let uritree = ref []
  54 let theoryuritree = ref []
  55
  56 let get_name =
  57  function
  58     Dir (name,_) -> name
  59   | File (name,_) -> name
  60 ;;
  61
  62 let get_uri =
  63  function
  64     Dir _ -> None
  65   | File (_,uri) -> Some uri
  66 ;;
  67
  68 (* STUFF TO BUILD THE URI TREE *)
  69
  70 exception EmptyUri
  71 exception DuplicatedUri
  72 exception ConflictingUris
  73
  74 let insert_in_uri_tree uri =
  75  let rec aux l =
  76   function
  77      [name] ->
  78       (try
  79         let _ = List.find (fun item -> name = get_name item) !l in
  80          raise DuplicatedUri
  81        with
  82         Not_found -> l := (File (name,uri))::!l
  83       )
  84    | name::tl ->
  85       (try
  86         match List.find (fun item -> name = get_name item) !l with
  87            Dir (_,children) -> aux children tl
  88          | File _ -> raise ConflictingUris
  89        with
  90         Not_found ->
  91          let children = ref [] in
  92           l := (Dir (name,children))::!l ;
  93           aux children tl
  94       )
  95    | [] -> raise EmptyUri
  96  in
  97   aux
  98 ;;
  99
 100 (* Imperative procedure that builds the two uri trees *)
 101 let build_uri_tree () =
 102  let dbh = Dbm.opendbm Configuration.uris_dbm [Dbm.Dbm_rdonly] 0 in
 103    Dbm.iter
 104     (fun uri _ ->
 105       let cicregexp = Str.regexp "cic:"
 106       and theoryregexp = Str.regexp "theory:" in
 107        if Str.string_match cicregexp uri 0 then
 108         let s = Str.replace_first cicregexp "" uri in
 109          let l = Str.split (Str.regexp "/") s in
 110           insert_in_uri_tree (UriManager.uri_of_string uri) uritree l
 111        else if Str.string_match theoryregexp uri 0 then
 112         let s = Str.replace_first theoryregexp "" uri in
 113          let l = Str.split (Str.regexp "/") s in
 114           insert_in_uri_tree (UriManager.uri_of_string uri) theoryuritree l
 115     ) dbh ;
 116    Dbm.close dbh
 117 ;;
 118
 119 (* GLOBAL REFERENCES (USED BY CALLBACKS) *)
 120
 121 let annotated_obj = ref None;;      (* reference to a couple option where    *)
 122                                     (* the first component is the current    *)
 123                                     (* annotated object and the second is    *)
 124                                     (* the map from ids to annotated targets *)
 125 let ann = ref (ref None);;          (* current annotation *)
 126 let radio_some_status = ref false;; (* is the radio_some button selected? *)
 127
 128 let theory_visited_uris = ref [];;
 129 let theory_to_visit_uris = ref [];;
 130 let visited_uris = ref [];;
 131 let to_visit_uris = ref [];;
 132
 133 (* CALLBACKS *)
 134
 135 exception NoCurrentUri;;
 136 exception NoNextOrPrevUri;;
 137
 138 let theory_get_current_uri () =
 139  match !theory_visited_uris with
 140     [] -> raise NoCurrentUri
 141   | uri::_ -> uri
 142 ;;
 143
 144 let get_current_uri () =
 145  match !visited_uris with
 146     [] -> raise NoCurrentUri
 147   | uri::_ -> uri
 148 ;;
 149
 150 let get_annotated_obj () =
 151  match !annotated_obj with
 152     None   ->
 153      let (annobj, ids_to_targets,_) =
 154       (CicCache.get_annobj (get_current_uri ()))
 155      in
 156       annotated_obj := Some (annobj, ids_to_targets) ;
 157       (annobj, ids_to_targets)
 158   | Some annobj -> annobj
 159 ;;
 160
 161 let filename_of_uri uri =
 162  Getter.get uri
 163 ;;
 164
 165 let theory_update_output rendering_window uri =
 166  rendering_window#label#set_text (UriManager.string_of_uri uri) ;
 167  ignore (rendering_window#errors#delete_text 0 rendering_window#errors#length) ;
 168   let mmlfile = XsltProcessor.process uri true "theory" in
 169    rendering_window#output#load mmlfile
 170 ;;
 171
 172 let update_output rendering_window uri =
 173  rendering_window#label#set_text (UriManager.string_of_uri uri) ;
 174  ignore (rendering_window#errors#delete_text 0 rendering_window#errors#length) ;
 175   let mmlfile = XsltProcessor.process uri true "cic" in
 176    rendering_window#output#load mmlfile
 177 ;;
 178
 179 let theory_next rendering_window () =
 180  match !theory_to_visit_uris with
 181     [] -> raise NoNextOrPrevUri
 182   | uri::tl ->
 183      theory_to_visit_uris := tl ;
 184      theory_visited_uris := uri::!theory_visited_uris ;
 185      theory_update_output rendering_window uri ;
 186      rendering_window#prevb#misc#set_sensitive true ;
 187      if tl = [] then
 188       rendering_window#nextb#misc#set_sensitive false
 189 ;;
 190
 191 let next rendering_window () =
 192  match !to_visit_uris with
 193     [] -> raise NoNextOrPrevUri
 194   | uri::tl ->
 195      to_visit_uris := tl ;
 196      visited_uris := uri::!visited_uris ;
 197      annotated_obj := None ;
 198      update_output rendering_window uri ;
 199      rendering_window#prevb#misc#set_sensitive true ;
 200      if tl = [] then
 201       rendering_window#nextb#misc#set_sensitive false
 202 ;;
 203
 204 let theory_prev rendering_window () =
 205  match !theory_visited_uris with
 206     [] -> raise NoCurrentUri
 207   | [_] -> raise NoNextOrPrevUri
 208   | uri::(uri'::tl as newvu) ->
 209      theory_visited_uris := newvu ;
 210      theory_to_visit_uris := uri::!theory_to_visit_uris ;
 211      theory_update_output rendering_window uri' ;
 212      rendering_window#nextb#misc#set_sensitive true ;
 213      if tl = [] then
 214       rendering_window#prevb#misc#set_sensitive false
 215 ;;
 216
 217 let prev rendering_window () =
 218  match !visited_uris with
 219     [] -> raise NoCurrentUri
 220   | [_] -> raise NoNextOrPrevUri
 221   | uri::(uri'::tl as newvu) ->
 222      visited_uris := newvu ;
 223      to_visit_uris := uri::!to_visit_uris ;
 224      annotated_obj := None ;
 225      update_output rendering_window uri' ;
 226      rendering_window#nextb#misc#set_sensitive true ;
 227      if tl = [] then
 228       rendering_window#prevb#misc#set_sensitive false
 229 ;;
 230
 231 (* called when an hyperlink is clicked *)
 232 let jump rendering_window (node : Ominidom.o_mDOMNode) =
 233  let module O = Ominidom in
 234   match (node#get_attribute (O.o_mDOMString_of_string "href")) with
 235     Some str ->
 236      let s = str#get_string in
 237      let uri = UriManager.uri_of_string s in
 238       rendering_window#show () ;
 239       rendering_window#prevb#misc#set_sensitive true ;
 240       rendering_window#nextb#misc#set_sensitive false ;
 241       visited_uris := uri::!visited_uris ;
 242       to_visit_uris := [] ;
 243       annotated_obj := None ;
 244       update_output rendering_window uri
 245   | None -> assert false
 246 ;;
 247
 248 let choose_selection rendering_window (node : Ominidom.o_mDOMNode option) =
 249  let module O = Ominidom in
 250   let rec aux node =
 251    match node#get_attribute (O.o_mDOMString_of_string "xref") with
 252      Some _ -> rendering_window#output#set_selection (Some node)
 253    | None   -> aux (node#get_parent)
 254   in
 255    match node with
 256      Some x -> aux x
 257    | None   -> rendering_window#output#set_selection None
 258 ;;
 259
 260
 261 let theory_selection_changed rendering_window uri () =
 262  match uri with
 263     None -> ()
 264   | Some uri' ->
 265      if !theory_visited_uris <> [] then
 266       rendering_window#prevb#misc#set_sensitive true ;
 267      rendering_window#nextb#misc#set_sensitive false ;
 268      theory_visited_uris := uri'::!theory_visited_uris ;
 269      theory_to_visit_uris := [] ;
 270      rendering_window#show () ;
 271      theory_update_output rendering_window uri'
 272 ;;
 273
 274 let selection_changed rendering_window uri () =
 275  match uri with
 276     None -> ()
 277   | Some uri' ->
 278      if !visited_uris <> [] then
 279       rendering_window#prevb#misc#set_sensitive true ;
 280      rendering_window#nextb#misc#set_sensitive false ;
 281      visited_uris := uri'::!visited_uris ;
 282      to_visit_uris := [] ;
 283      annotated_obj := None ;
 284      rendering_window#show () ;
 285      update_output rendering_window uri'
 286 ;;
 287
 288 let create_gtk_trees (hbox : GPack.box) rendering_window theory_rendering_window mktree =
 289  let sw3 =
 290   GBin.scrolled_window ~width:250 ~height:600
 291    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 292  let tree1 =
 293   GTree.tree ~selection_mode:`BROWSE ~packing:sw3#add_with_viewport () in
 294  let tree_item1 = GTree.tree_item ~label:"theory:/" ~packing:tree1#append () in
 295
 296  let sw2 =
 297   GBin.scrolled_window ~width:250 ~height:600
 298    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 299  let tree =
 300   GTree.tree ~selection_mode:`BROWSE ~packing:sw2#add_with_viewport () in
 301  let tree_item = GTree.tree_item ~label:"cic:/" ~packing:tree#append () in
 302
 303   ignore(tree_item#connect#select (selection_changed rendering_window None)) ;
 304   mktree selection_changed rendering_window tree_item (Dir ("cic:/",uritree)) ;
 305
 306   ignore(tree_item1#connect#select
 307    (theory_selection_changed theory_rendering_window None)) ;
 308   mktree theory_selection_changed theory_rendering_window tree_item1
 309    (Dir ("theory:/",theoryuritree)) ;
 310   (sw3,sw2)
 311 ;;
 312
 313 let updateb_pressed theory_rendering_window rendering_window
 314  (sw1, sw ,(hbox : GPack.box)) mktree ()
 315 =
 316  Getter.update () ;
 317  (* let's empty the uri trees and rebuild them *)
 318  uritree := [] ;
 319  theoryuritree := [] ;
 320  build_uri_tree () ;
 321  hbox#remove !sw1#coerce ;
 322  hbox#remove !sw#coerce ;
 323  let (sw3,sw2) =
 324   create_gtk_trees hbox rendering_window theory_rendering_window mktree
 325  in
 326   sw1 := sw3 ;
 327   sw := sw2
 328 ;;
 329
 330 let theory_check rendering_window () =
 331   let output =
 332   try
 333    TheoryTypeChecker.typecheck (theory_get_current_uri ());
 334    "Type Checking was successful"
 335   with
 336    TheoryTypeChecker.NotWellTyped s ->
 337     "Type Checking was NOT successful:\n\t" ^ s
 338  in
 339   (* next "cast" can't got rid of, but I don't know why *)
 340   let errors = (rendering_window#errors : GEdit.text) in
 341   let _ = errors#delete_text 0 errors#length  in
 342    errors#insert output
 343 ;;
 344
 345 let check rendering_window () =
 346   let output =
 347   try
 348    CicTypeChecker.typecheck (get_current_uri ());
 349    "Type Checking was successful"
 350   with
 351    CicTypeChecker.NotWellTyped s -> "Type Checking was NOT successful:\n\t" ^ s
 352  in
 353   (* next "cast" can't got rid of, but I don't know why *)
 354   let errors = (rendering_window#errors : GEdit.text) in
 355   let _ = errors#delete_text 0 errors#length  in
 356    errors#insert output
 357 ;;
 358
 359 let annotateb_pressed rendering_window annotation_window () =
 360  let module O = Ominidom in
 361  match rendering_window#output#get_selection with
 362  | Some node ->
 363   begin
 364    match (node#get_attribute (O.o_mDOMString_of_string "xref")) with
 365    | Some xpath ->
 366      let annobj = get_annotated_obj ()
 367      (* next "cast" can't got rid of, but I don't know why *)
 368      and annotation = (annotation_window#annotation : GEdit.text) in
 369       ann := CicXPath.get_annotation annobj (xpath#get_string) ;
 370       CicAnnotationHinter.create_hints annotation_window annobj (xpath#get_string) ;
 371       annotation#delete_text 0 annotation#length ;
 372       begin
 373        match !(!ann) with
 374            None      ->
 375             annotation#misc#set_sensitive false ;
 376             annotation_window#radio_none#set_active true ;
 377             radio_some_status := false
 378          | Some ann' ->
 379             annotation#insert ann' ;
 380             annotation#misc#set_sensitive true ;
 381             annotation_window#radio_some#set_active true ;
 382             radio_some_status := true
 383       end ;
 384       GMain.Grab.add (annotation_window#window_to_annotate#coerce) ;
 385       annotation_window#show () ;
 386    | None ->
 387        (* next "cast" can't got rid of, but I don't know why *)
 388        let errors = (rendering_window#errors : GEdit.text) in
 389         errors#insert ("\nNo xref found\n")
 390   end
 391  | None -> (rendering_window#errors : GEdit.text)#insert "\nNo selection!\n"
 392 ;;
 393
 394 (* called when the annotation is confirmed *)
 395 let save_annotation annotation =
 396  if !radio_some_status then
 397   !ann := Some (annotation#get_chars 0 annotation#length)
 398  else
 399   !ann := None ;
 400  match !annotated_obj with
 401     None -> assert false
 402   | Some (annobj,_) ->
 403      let uri = get_current_uri () in
 404       let annxml = Annotation2Xml.pp_annotation annobj uri in
 405        Xml.pp annxml (Some (fst (Getter.get_ann_file_name_and_uri uri)))
 406 ;;
 407
 408 let parse_no_cache uri =
 409  let module U = UriManager in
 410   XsltProcessor.process uri false "cic"
 411 ;;
 412
 413
 414 (* STUFF TO BUILD THE GTK INTERFACE *)
 415
 416 (* Stuff to build the tree window *)
 417
 418 (* selection_changed is actually selection_changed or theory_selection_changed*)
 419 let mktree selection_changed rendering_window =
 420  let rec aux treeitem =
 421   function
 422      Dir (dirname, content) ->
 423       let subtree = GTree.tree () in
 424        treeitem#set_subtree subtree ;
 425         let expand_sons =
 426          List.map
 427           (fun ti ->
 428             let label = get_name ti
 429             and uri = get_uri ti in
 430              let treeitem2 = GTree.tree_item ~label:label () in
 431               subtree#append treeitem2 ;
 432               ignore(treeitem2#connect#select
 433                (selection_changed rendering_window uri)) ;
 434                (* Almost lazy function *)
 435                (fun () -> aux treeitem2 ti)
 436           ) (List.sort compare !content)
 437         in
 438          let lazy_expand_sons = lazy (List.iter (fun f -> f ()) expand_sons) in
 439          ignore(treeitem#connect#expand
 440           (fun () -> Lazy.force lazy_expand_sons)) ;
 441    | _ -> ()
 442  in
 443   aux
 444 ;;
 445
 446 (* Stuff for the widget settings *)
 447
 448 let export_to_postscript (output : GMathView.math_view) () =
 449  output#export_to_postscript ~filename:"output.ps" ();
 450 ;;
 451
 452 let activate_t1 output button_set_anti_aliasing button_set_kerning
 453  button_export_to_postscript button_t1 ()
 454 =
 455  let is_set = button_t1#active in
 456   output#set_font_manager_type
 457    (if is_set then `font_manager_t1 else `font_manager_gtk) ;
 458   if is_set then
 459    begin
 460     button_set_anti_aliasing#misc#set_sensitive true ;
 461     button_set_kerning#misc#set_sensitive true ;
 462     button_export_to_postscript#misc#set_sensitive true ;
 463    end
 464   else
 465    begin
 466     button_set_anti_aliasing#misc#set_sensitive false ;
 467     button_set_kerning#misc#set_sensitive false ;
 468     button_export_to_postscript#misc#set_sensitive false ;
 469    end
 470 ;;
 471
 472 let set_anti_aliasing output button_set_anti_aliasing () =
 473  output#set_anti_aliasing button_set_anti_aliasing#active
 474 ;;
 475
 476 let set_kerning output button_set_kerning () =
 477  output#set_kerning button_set_kerning#active
 478 ;;
 479
 480 let changefont output font_size_spinb () =
 481  output#set_font_size font_size_spinb#value_as_int
 482 ;;
 483
 484 let set_log_verbosity output log_verbosity_spinb () =
 485  output#set_log_verbosity log_verbosity_spinb#value_as_int
 486 ;;
 487
 488 class settings_window output sw button_export_to_postscript jump_callback
 489  selection_changed_callback
 490 =
 491  let settings_window = GWindow.window ~title:"GtkMathView settings" () in
 492  let vbox =
 493   GPack.vbox ~packing:settings_window#add () in
 494  let table =
 495   GPack.table
 496    ~rows:1 ~columns:3 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
 497    ~border_width:5 ~packing:vbox#add () in
 498  let button_t1 =
 499   GButton.toggle_button ~label:"activate t1 fonts"
 500    ~packing:(table#attach ~left:0 ~top:0) () in
 501  let button_set_anti_aliasing =
 502   GButton.toggle_button ~label:"set_anti_aliasing"
 503    ~packing:(table#attach ~left:1 ~top:0) () in
 504  let button_set_kerning =
 505   GButton.toggle_button ~label:"set_kerning"
 506    ~packing:(table#attach ~left:2 ~top:0) () in
 507  let table =
 508   GPack.table
 509    ~rows:2 ~columns:2 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
 510    ~border_width:5 ~packing:vbox#add () in
 511  let font_size_label =
 512   GMisc.label ~text:"font size:"
 513    ~packing:(table#attach ~left:0 ~top:0 ~expand:`NONE) () in
 514  let font_size_spinb =
 515   let sadj =
 516    GData.adjustment ~value:14.0 ~lower:5.0 ~upper:50.0 ~step_incr:1.0 ()
 517   in
 518    GEdit.spin_button
 519     ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:0 ~fill:`NONE) () in
 520  let log_verbosity_label =
 521   GMisc.label ~text:"log verbosity:"
 522    ~packing:(table#attach ~left:0 ~top:1) () in
 523  let log_verbosity_spinb =
 524   let sadj =
 525    GData.adjustment ~value:0.0 ~lower:0.0 ~upper:3.0 ~step_incr:1.0 ()
 526   in
 527    GEdit.spin_button
 528     ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:1) () in
 529  let hbox =
 530   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
 531  let closeb =
 532   GButton.button ~label:"Close"
 533    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 534 object(self)
 535  method show = settings_window#show
 536  initializer
 537   button_set_anti_aliasing#misc#set_sensitive false ;
 538   button_set_kerning#misc#set_sensitive false ;
 539   (* Signals connection *)
 540   ignore(button_t1#connect#clicked
 541    (activate_t1 output button_set_anti_aliasing button_set_kerning
 542     button_export_to_postscript button_t1)) ;
 543   ignore(font_size_spinb#connect#changed (changefont output font_size_spinb)) ;
 544   ignore(button_set_anti_aliasing#connect#toggled
 545    (set_anti_aliasing output button_set_anti_aliasing));
 546   ignore(button_set_kerning#connect#toggled
 547    (set_kerning output button_set_kerning)) ;
 548   ignore(log_verbosity_spinb#connect#changed
 549    (set_log_verbosity output log_verbosity_spinb)) ;
 550   ignore(closeb#connect#clicked settings_window#misc#hide)
 551 end;;
 552
 553 (* Main windows *)
 554
 555 class annotation_window output label =
 556  let window_to_annotate =
 557   GWindow.window ~title:"Annotating environment" ~border_width:2 () in
 558  let hbox1 =
 559   GPack.hbox ~packing:window_to_annotate#add () in
 560  let vbox1 =
 561   GPack.vbox ~packing:(hbox1#pack ~padding:5) () in
 562  let hbox2 =
 563   GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
 564  let radio_some = GButton.radio_button ~label:"Annotation below"
 565   ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
 566  let radio_none = GButton.radio_button ~label:"No annotation"
 567   ~group:radio_some#group
 568   ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5)
 569   ~active:true () in
 570  let annotation = GEdit.text ~editable:true ~width:400 ~height:180
 571   ~packing:(vbox1#pack ~padding:5) () in
 572  let table =
 573   GPack.table ~rows:3 ~columns:3 ~packing:(vbox1#pack ~padding:5) () in
 574  let annotation_hints =
 575   Array.init 9
 576    (function i ->
 577      GButton.button ~label:("Hint " ^ string_of_int i)
 578       ~packing:(table#attach ~left:(i mod 3) ~top:(i / 3)) ()
 579    ) in
 580  let vbox2 =
 581   GPack.vbox ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
 582  let confirmb =
 583   GButton.button ~label:"O.K."
 584    ~packing:(vbox2#pack ~expand:false ~fill:false ~padding:5) () in
 585  let abortb =
 586   GButton.button ~label:"Abort"
 587    ~packing:(vbox2#pack ~expand:false ~fill:false ~padding:5) () in
 588 object (self)
 589  method window_to_annotate = window_to_annotate
 590  method annotation = annotation
 591  method radio_some = radio_some
 592  method radio_none = radio_none
 593  method annotation_hints = annotation_hints
 594  method output = (output : GMathView.math_view)
 595  method show () = window_to_annotate#show ()
 596  initializer
 597   (* signal handlers here *)
 598   ignore (window_to_annotate#event#connect#delete
 599    (fun _ ->
 600      window_to_annotate#misc#hide () ;
 601      GMain.Grab.remove (window_to_annotate#coerce) ;
 602      true
 603    )) ;
 604   ignore (confirmb#connect#clicked
 605    (fun () ->
 606      window_to_annotate#misc#hide () ;
 607      save_annotation annotation ;
 608      GMain.Grab.remove (window_to_annotate#coerce) ;
 609      let new_current_uri =
 610       (snd (Getter.get_ann_file_name_and_uri (get_current_uri ())))
 611      in
 612       visited_uris := new_current_uri::(List.tl !visited_uris) ;
 613        label#set_text (UriManager.string_of_uri new_current_uri) ;
 614        let mmlfile = parse_no_cache new_current_uri in
 615         output#load mmlfile
 616    )) ;
 617   ignore (abortb#connect#clicked
 618    (fun () ->
 619      window_to_annotate#misc#hide () ;
 620      GMain.Grab.remove (window_to_annotate#coerce)
 621    ));
 622   ignore (radio_some#connect#clicked
 623    (fun () -> annotation#misc#set_sensitive true ; radio_some_status := true)) ;
 624   ignore (radio_none #connect#clicked
 625    (fun () ->
 626      annotation#misc#set_sensitive false;
 627      radio_some_status := false)
 628    )
 629 end;;
 630
 631 class rendering_window annotation_window output (label : GMisc.label) =
 632  let window =
 633   GWindow.window ~title:"MathML viewer" ~border_width:2 () in
 634  let vbox =
 635   GPack.vbox ~packing:window#add () in
 636  let _ = vbox#pack ~expand:false ~fill:false ~padding:5 label#coerce in
 637  let paned =
 638   GPack.paned `HORIZONTAL ~packing:(vbox#pack ~expand:true ~padding:5) () in
 639  let scrolled_window0 =
 640   GBin.scrolled_window ~border_width:10 ~packing:paned#add1 () in
 641  let _ = scrolled_window0#add output#coerce in
 642  let scrolled_window =
 643   GBin.scrolled_window
 644    ~border_width:10 ~packing:paned#add2 ~width:240 ~height:100 () in
 645  let errors = GEdit.text ~packing:scrolled_window#add_with_viewport () in
 646  let hbox =
 647   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
 648  let prevb =
 649   GButton.button ~label:"Prev"
 650    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 651  let nextb =
 652   GButton.button ~label:"Next"
 653    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 654  let checkb =
 655   GButton.button ~label:"Check"
 656    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 657  let annotateb =
 658   GButton.button ~label:"Annotate"
 659    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 660  let settingsb =
 661   GButton.button ~label:"Settings"
 662    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 663  let button_export_to_postscript =
 664   GButton.button ~label:"export_to_postscript"
 665   ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 666  let closeb =
 667   GButton.button ~label:"Close"
 668    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 669 object(self)
 670  method nextb = nextb
 671  method prevb = prevb
 672  method label = label
 673  method output = (output : GMathView.math_view)
 674  method errors = errors
 675  method show () = window#show ()
 676  initializer
 677   nextb#misc#set_sensitive false ;
 678   prevb#misc#set_sensitive false ;
 679   button_export_to_postscript#misc#set_sensitive false ;
 680
 681   (* signal handlers here *)
 682   ignore(output#connect#jump (jump self)) ;
 683   ignore(output#connect#selection_changed (choose_selection self)) ;
 684   ignore(nextb#connect#clicked (next self)) ;
 685   ignore(prevb#connect#clicked (prev self)) ;
 686   (* LUCA: check disabled while compression is not fully implemented *)
 687   (* ignore(checkb#connect#clicked (check self)) ; *)
 688   checkb#misc#set_sensitive false ;
 689   ignore(closeb#connect#clicked window#misc#hide) ;
 690   ignore(annotateb#connect#clicked (annotateb_pressed self annotation_window)) ;
 691   let settings_window = new settings_window output scrolled_window0
 692    button_export_to_postscript (jump self) (choose_selection self) in
 693   ignore(settingsb#connect#clicked settings_window#show) ;
 694   ignore(button_export_to_postscript#connect#clicked (export_to_postscript output)) ;
 695   ignore(window#event#connect#delete (fun _ -> window#misc#hide () ; true ))
 696 end;;
 697
 698 class theory_rendering_window rendering_window =
 699  let window =
 700   GWindow.window ~title:"MathML theory viewer" ~border_width:2 () in
 701  let vbox =
 702   GPack.vbox ~packing:window#add () in
 703  let label =
 704   GMisc.label ~text:"???"
 705    ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
 706  let paned =
 707   GPack.paned `HORIZONTAL ~packing:(vbox#pack ~expand:true ~padding:5) () in
 708  let scrolled_window0 =
 709   GBin.scrolled_window ~border_width:10 ~packing:paned#add1 () in
 710  let output =
 711   GMathView.math_view ~width:400 ~height:380 ~packing:scrolled_window0#add () in
 712  let scrolled_window =
 713   GBin.scrolled_window
 714    ~border_width:10 ~packing:paned#add2 ~width:240 ~height:100 () in
 715  let errors = GEdit.text ~packing:scrolled_window#add_with_viewport () in
 716  let hbox =
 717   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
 718  let prevb =
 719   GButton.button ~label:"Prev"
 720    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 721  let nextb =
 722   GButton.button ~label:"Next"
 723    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 724  let checkb =
 725   GButton.button ~label:"Check"
 726    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 727  let settingsb =
 728   GButton.button ~label:"Settings"
 729    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 730  let button_export_to_postscript =
 731   GButton.button ~label:"export_to_postscript"
 732   ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 733  let closeb =
 734   GButton.button ~label:"Close"
 735    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 736 object(self)
 737  method nextb = nextb
 738  method prevb = prevb
 739  method label = label
 740  method output = (output : GMathView.math_view)
 741  method errors = errors
 742  method show () = window#show ()
 743  initializer
 744   nextb#misc#set_sensitive false ;
 745   prevb#misc#set_sensitive false ;
 746   button_export_to_postscript#misc#set_sensitive false ;
 747
 748   (* signal handlers here *)
 749   ignore(output#connect#jump (jump rendering_window)) ;
 750   ignore(output#connect#selection_changed (choose_selection self)) ;
 751   ignore(nextb#connect#clicked (theory_next self)) ;
 752   ignore(prevb#connect#clicked (theory_prev self)) ;
 753   ignore(checkb#connect#clicked (theory_check self)) ;
 754   let settings_window = new settings_window output scrolled_window0
 755    button_export_to_postscript (jump rendering_window)(choose_selection self) in
 756   ignore(settingsb#connect#clicked settings_window#show) ;
 757   ignore(button_export_to_postscript#connect#clicked (export_to_postscript output)) ;
 758   ignore(closeb#connect#clicked window#misc#hide) ;
 759   ignore(window#event#connect#delete (fun _ -> window#misc#hide () ; true ))
 760 end;;
 761
 762 (* CSC: fare in modo che i due alberi vengano svuotati invece che distrutti *)
 763 class selection_window theory_rendering_window rendering_window =
 764   let label = "cic:/" in
 765   let theorylabel = "theory:/" in
 766   let win = GWindow.window ~title:"Known uris" ~border_width:2 () in
 767   let vbox = GPack.vbox ~packing:win#add () in
 768   let hbox1 = GPack.hbox ~packing:(vbox#pack ~padding:5) () in
 769   let (sw1,sw) =
 770    create_gtk_trees hbox1 rendering_window theory_rendering_window mktree
 771   in
 772   let hbox =
 773    GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
 774   let updateb =
 775    GButton.button ~label:"Update"
 776     ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 777   let quitb =
 778    GButton.button ~label:"Quit"
 779     ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 780 object (self)
 781   method show () = win#show ()
 782   initializer
 783     (* signal handlers here *)
 784     ignore (win#connect#destroy ~callback:GMain.Main.quit) ;
 785     ignore (quitb#connect#clicked GMain.Main.quit) ;
 786     ignore(updateb#connect#clicked (updateb_pressed
 787      theory_rendering_window rendering_window (ref sw1, ref sw, hbox1) mktree))
 788 end;;
 789
 790
 791 (* MAIN *)
 792
 793 let _ =
 794  build_uri_tree () ;
 795  let output = GMathView.math_view ~width:400 ~height:380 ()
 796  and label = GMisc.label ~text:"???" () in
 797   let annotation_window = new annotation_window output label in
 798   let rendering_window = new rendering_window annotation_window output label in
 799   let theory_rendering_window = new theory_rendering_window rendering_window in
 800   let selection_window =
 801    new selection_window theory_rendering_window rendering_window
 802   in
 803    selection_window#show () ;
 804    GMain.Main.main ()
 805 ;;