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