helm/interface/mmlinterface.ml

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