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 (*                                 03/04/2001                                 *)
  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 (* GLOBAL REFERENCES (USED BY CALLBACKS) *)
  47
  48 let annotated_obj = ref None;;      (* reference to a couple option where    *)
  49                                     (* the first component is the current    *)
  50                                     (* annotated object and the second is    *)
  51                                     (* the map from ids to annotated targets *)
  52 let ann = ref (ref None);;          (* current annotation *)
  53 let radio_some_status = ref false;; (* is the radio_some button selected? *)
  54
  55 let visited_urls = (ref [] : string list ref);;
  56 let to_visit_urls = ref [];;
  57
  58 exception No_param_dot_CICURI_found_in of string;;
  59 exception Unexpected_URL_format of string;;
  60
  61 (*CSC: never used: Urrah!!!
  62 let url_from_frameseturl frameseturl =
  63  let module N = Neturl in
  64   let l =
  65    (Str.split (Str.regexp "=")
  66     (N.url_query ~encoded:true (N.url_of_string N.ip_url_syntax frameseturl)))
  67   in
  68    match l with
  69       [_ ; url] -> Netencoding.Url.decode url
  70     | _ -> raise (Unexpected_URL_format frameseturl)
  71 ;;
  72 *)
  73
  74 let uri_from_url url =
  75  let module N = Neturl in
  76   let rec find_uri =
  77    function
  78       [] -> raise (No_param_dot_CICURI_found_in url)
  79     | he::tl ->
  80        match Str.split (Str.regexp "=") he with
  81           ["param.CICURI";uri] -> uri
  82         | _ -> find_uri tl
  83   in
  84    find_uri
  85     (Str.split (Str.regexp "&")
  86      (N.url_query ~encoded:true (N.url_of_string N.ip_url_syntax url)))
  87 ;;
  88
  89 (* MISC FUNCTIONS *)
  90
  91 exception NoCurrentUrl;;
  92 exception NoNextOrPrevUrl;;
  93
  94 let get_current_url () =
  95  match !visited_urls with
  96     [] -> raise NoCurrentUrl
  97   | url::_ -> url
  98 ;;
  99
 100 let get_current_uri () =
 101  UriManager.uri_of_string (uri_from_url (get_current_url ()))
 102 ;;
 103
 104 (* CALLBACKS *)
 105
 106 let get_annotated_obj () =
 107  match !annotated_obj with
 108     None   ->
 109      let (annobj, ids_to_targets,_) =
 110       (CicCache.get_annobj (get_current_uri ()))
 111      in
 112       annotated_obj := Some (annobj, ids_to_targets) ;
 113       (annobj, ids_to_targets)
 114   | Some annobj -> annobj
 115 ;;
 116
 117 let update_output rendering_window url =
 118  rendering_window#label#set_text (uri_from_url url) ;
 119  rendering_window#output#load url
 120 ;;
 121
 122 let next rendering_window () =
 123  match !to_visit_urls with
 124     [] -> raise NoNextOrPrevUrl
 125   | url::tl ->
 126      to_visit_urls := tl ;
 127      visited_urls := url::!visited_urls ;
 128      annotated_obj := None ;
 129      update_output rendering_window url ;
 130      rendering_window#prevb#misc#set_sensitive true ;
 131      if tl = [] then
 132       rendering_window#nextb#misc#set_sensitive false
 133 ;;
 134
 135 let prev rendering_window () =
 136  match !visited_urls with
 137     [] -> raise NoCurrentUrl
 138   | [_] -> raise NoNextOrPrevUrl
 139   | uri::(uri'::tl as newvu) ->
 140      visited_urls := newvu ;
 141      to_visit_urls := uri::!to_visit_urls ;
 142      annotated_obj := None ;
 143      update_output rendering_window uri' ;
 144      rendering_window#nextb#misc#set_sensitive true ;
 145      if tl = [] then
 146       rendering_window#prevb#misc#set_sensitive false
 147 ;;
 148
 149 (* called when an hyperlink is clicked *)
 150 let jump rendering_window (node : Ominidom.o_mDOMNode) =
 151  let module O = Ominidom in
 152  let module U = Unix in
 153   match (node#get_attribute (O.o_mDOMString_of_string "href")) with
 154     Some str ->
 155      let frameseturl = str#get_string in
 156      let devnull = U.openfile "/dev/null" [U.O_RDWR] 0o600 in
 157       ignore
 158        (U.create_process "netscape-remote"
 159          [|"netscape-remote" ; "-noraise" ; "-remote" ;
 160            "openURL(" ^ frameseturl ^ ",cic)"
 161          |] devnull devnull devnull)
 162   | None -> assert false
 163 ;;
 164
 165 (*CSC: per ora mai chiamata. Deve essere chiamata quando attivata dal *)
 166 (*CSC: remote-control                                                 *)
 167 let remotejump rendering_window url =
 168  rendering_window#prevb#misc#set_sensitive true ;
 169  rendering_window#nextb#misc#set_sensitive false ;
 170  visited_urls := url::!visited_urls ;
 171  to_visit_urls := [] ;
 172  annotated_obj := None ;
 173  update_output rendering_window url
 174 ;;
 175
 176 let choose_selection rendering_window (node : Ominidom.o_mDOMNode option) =
 177  let module O = Ominidom in
 178   let rec aux node =
 179    match node#get_attribute (O.o_mDOMString_of_string "xref") with
 180      Some _ -> rendering_window#output#set_selection (Some node)
 181    | None   -> aux (node#get_parent)
 182   in
 183    match node with
 184      Some x -> aux x
 185    | None   -> rendering_window#output#set_selection None
 186 ;;
 187
 188 let annotateb_pressed rendering_window annotation_window () =
 189  let module O = Ominidom in
 190  match rendering_window#output#get_selection with
 191    Some node ->
 192     begin
 193      match (node#get_attribute (O.o_mDOMString_of_string "xref")) with
 194         Some xpath ->
 195          let annobj = get_annotated_obj ()
 196          and annotation = (annotation_window#annotation : GEdit.text) in
 197           ann := CicXPath.get_annotation annobj (xpath#get_string) ;
 198           CicAnnotationHinter.create_hints annotation_window annobj
 199            (xpath#get_string) ;
 200           annotation#delete_text 0 annotation#length ;
 201           begin
 202            match !(!ann) with
 203                None      ->
 204                 annotation#misc#set_sensitive false ;
 205                 annotation_window#radio_none#set_active true ;
 206                 radio_some_status := false
 207              | Some ann' ->
 208                 annotation#insert ann' ;
 209                 annotation#misc#set_sensitive true ;
 210                 annotation_window#radio_some#set_active true ;
 211                 radio_some_status := true
 212           end ;
 213           GMain.Grab.add (annotation_window#window_to_annotate#coerce) ;
 214           annotation_window#show () ;
 215      | None -> rendering_window#label#set_text ("ERROR: No xref found!!!\n")
 216     end
 217  | None -> rendering_window#label#set_text ("ERROR: No selection!!!\n")
 218 ;;
 219
 220 (* called when the annotation is confirmed *)
 221 let save_annotation annotation =
 222  if !radio_some_status then
 223   !ann := Some (annotation#get_chars 0 annotation#length)
 224  else
 225   !ann := None ;
 226  match !annotated_obj with
 227     None -> assert false
 228   | Some (annobj,_) ->
 229      let uri = get_current_uri () in
 230       let annxml = Annotation2Xml.pp_annotation annobj uri in
 231        Xml.pp annxml (Some (fst (Getter.get_ann_file_name_and_uri uri)))
 232 ;;
 233
 234 (* STUFF TO BUILD THE GTK INTERFACE *)
 235
 236 (* Stuff for the widget settings *)
 237
 238 let export_to_postscript (output : GMathView.math_view) () =
 239  output#export_to_postscript ~filename:"output.ps" ();
 240 ;;
 241
 242 let activate_t1 output button_set_anti_aliasing button_set_kerning
 243  button_export_to_postscript button_t1 ()
 244 =
 245  let is_set = button_t1#active in
 246   output#set_font_manager_type
 247    (if is_set then `font_manager_t1 else `font_manager_gtk) ;
 248   if is_set then
 249    begin
 250     button_set_anti_aliasing#misc#set_sensitive true ;
 251     button_set_kerning#misc#set_sensitive true ;
 252     button_export_to_postscript#misc#set_sensitive true ;
 253    end
 254   else
 255    begin
 256     button_set_anti_aliasing#misc#set_sensitive false ;
 257     button_set_kerning#misc#set_sensitive false ;
 258     button_export_to_postscript#misc#set_sensitive false ;
 259    end
 260 ;;
 261
 262 let set_anti_aliasing output button_set_anti_aliasing () =
 263  output#set_anti_aliasing button_set_anti_aliasing#active
 264 ;;
 265
 266 let set_kerning output button_set_kerning () =
 267  output#set_kerning button_set_kerning#active
 268 ;;
 269
 270 let changefont output font_size_spinb () =
 271  output#set_font_size font_size_spinb#value_as_int
 272 ;;
 273
 274 let set_log_verbosity output log_verbosity_spinb () =
 275  output#set_log_verbosity log_verbosity_spinb#value_as_int
 276 ;;
 277
 278 class settings_window output sw button_export_to_postscript jump_callback
 279  selection_changed_callback
 280 =
 281  let settings_window = GWindow.window ~title:"GtkMathView settings" () in
 282  let vbox =
 283   GPack.vbox ~packing:settings_window#add () in
 284  let table =
 285   GPack.table
 286    ~rows:1 ~columns:3 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
 287    ~border_width:5 ~packing:vbox#add () in
 288  let button_t1 =
 289   GButton.toggle_button ~label:"activate t1 fonts"
 290    ~packing:(table#attach ~left:0 ~top:0) () in
 291  let button_set_anti_aliasing =
 292   GButton.toggle_button ~label:"set_anti_aliasing"
 293    ~packing:(table#attach ~left:1 ~top:0) () in
 294  let button_set_kerning =
 295   GButton.toggle_button ~label:"set_kerning"
 296    ~packing:(table#attach ~left:2 ~top:0) () in
 297  let table =
 298   GPack.table
 299    ~rows:2 ~columns:2 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
 300    ~border_width:5 ~packing:vbox#add () in
 301  let font_size_label =
 302   GMisc.label ~text:"font size:"
 303    ~packing:(table#attach ~left:0 ~top:0 ~expand:`NONE) () in
 304  let font_size_spinb =
 305   let sadj =
 306    GData.adjustment ~value:14.0 ~lower:5.0 ~upper:50.0 ~step_incr:1.0 ()
 307   in
 308    GEdit.spin_button
 309     ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:0 ~fill:`NONE) () in
 310  let log_verbosity_label =
 311   GMisc.label ~text:"log verbosity:"
 312    ~packing:(table#attach ~left:0 ~top:1) () in
 313  let log_verbosity_spinb =
 314   let sadj =
 315    GData.adjustment ~value:0.0 ~lower:0.0 ~upper:3.0 ~step_incr:1.0 ()
 316   in
 317    GEdit.spin_button
 318     ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:1) () in
 319  let hbox =
 320   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
 321  let closeb =
 322   GButton.button ~label:"Close"
 323    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 324 object(self)
 325  method show = settings_window#show
 326  initializer
 327   button_set_anti_aliasing#misc#set_sensitive false ;
 328   button_set_kerning#misc#set_sensitive false ;
 329   (* Signals connection *)
 330   ignore(button_t1#connect#clicked
 331    (activate_t1 output button_set_anti_aliasing button_set_kerning
 332     button_export_to_postscript button_t1)) ;
 333   ignore(font_size_spinb#connect#changed (changefont output font_size_spinb)) ;
 334   ignore(button_set_anti_aliasing#connect#toggled
 335    (set_anti_aliasing output button_set_anti_aliasing));
 336   ignore(button_set_kerning#connect#toggled
 337    (set_kerning output button_set_kerning)) ;
 338   ignore(log_verbosity_spinb#connect#changed
 339    (set_log_verbosity output log_verbosity_spinb)) ;
 340   ignore(closeb#connect#clicked settings_window#misc#hide)
 341 end;;
 342
 343 (* Main windows *)
 344
 345 class annotation_window output label =
 346  let window_to_annotate =
 347   GWindow.window ~title:"Annotating environment" ~border_width:2 () in
 348  let hbox1 =
 349   GPack.hbox ~packing:window_to_annotate#add () in
 350  let vbox1 =
 351   GPack.vbox ~packing:(hbox1#pack ~padding:5) () in
 352  let hbox2 =
 353   GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
 354  let radio_some = GButton.radio_button ~label:"Annotation below"
 355   ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
 356  let radio_none = GButton.radio_button ~label:"No annotation"
 357   ~group:radio_some#group
 358   ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5)
 359   ~active:true () in
 360  let annotation = GEdit.text ~editable:true ~width:400 ~height:180
 361   ~packing:(vbox1#pack ~padding:5) () in
 362  let table =
 363   GPack.table ~rows:3 ~columns:3 ~packing:(vbox1#pack ~padding:5) () in
 364  let annotation_hints =
 365   Array.init 9
 366    (function i ->
 367      GButton.button ~label:("Hint " ^ string_of_int i)
 368       ~packing:(table#attach ~left:(i mod 3) ~top:(i / 3)) ()
 369    ) in
 370  let vbox2 =
 371   GPack.vbox ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
 372  let confirmb =
 373   GButton.button ~label:"O.K."
 374    ~packing:(vbox2#pack ~expand:false ~fill:false ~padding:5) () in
 375  let abortb =
 376   GButton.button ~label:"Abort"
 377    ~packing:(vbox2#pack ~expand:false ~fill:false ~padding:5) () in
 378 object (self)
 379  method window_to_annotate = window_to_annotate
 380  method annotation = annotation
 381  method radio_some = radio_some
 382  method radio_none = radio_none
 383  method annotation_hints = annotation_hints
 384  method output = (output : GMathView.math_view)
 385  method show () = window_to_annotate#show ()
 386  initializer
 387   (* signal handlers here *)
 388   ignore (window_to_annotate#event#connect#delete
 389    (fun _ ->
 390      window_to_annotate#misc#hide () ;
 391      GMain.Grab.remove (window_to_annotate#coerce) ;
 392      true
 393    )) ;
 394   ignore (confirmb#connect#clicked
 395    (fun () ->
 396      window_to_annotate#misc#hide () ;
 397      save_annotation annotation ;
 398      GMain.Grab.remove (window_to_annotate#coerce) ;
 399      let new_current_uri =
 400       snd (Getter.get_ann_file_name_and_uri (get_current_uri ()))
 401      in
 402 (*CSC: qui c'e' un gran casino: e' l'XsltProcessor che deve ricevere
 403   la richiesta e non il ClientHTTP. Inoltre, prima di inoltrarla,
 404   bisogna comunicare al getter che ora esiste anche il file di annotazioni!!!
 405 *)
 406       (*CSC: DA RIPRISTINARE CON IL RIPRISTINO DELLE ANNOTAZIONI
 407       visited_urls := new_current_uri::(List.tl !visited_urls) ;
 408       *)
 409        let new_current_url = XsltProcessor.url_of_uri new_current_uri in
 410        visited_urls := new_current_url::(List.tl !visited_urls) ;
 411        label#set_text (UriManager.string_of_uri new_current_uri) ;
 412        (*CSC: Perche' non usare update_output? *)
 413        let mmlfile =
 414         ClientHTTP.get_and_save_to_tmp new_current_url
 415        in
 416         output#load mmlfile
 417    )) ;
 418   ignore (abortb#connect#clicked
 419    (fun () ->
 420      window_to_annotate#misc#hide () ;
 421      GMain.Grab.remove (window_to_annotate#coerce)
 422    ));
 423   ignore (radio_some#connect#clicked
 424    (fun () -> annotation#misc#set_sensitive true ; radio_some_status := true)) ;
 425   ignore (radio_none #connect#clicked
 426    (fun () ->
 427      annotation#misc#set_sensitive false;
 428      radio_some_status := false)
 429    )
 430 end;;
 431
 432 class rendering_window annotation_window output (label : GMisc.label) =
 433  let window =
 434   GWindow.window ~title:"MathML viewer" ~border_width:2 () in
 435  let vbox =
 436   GPack.vbox ~packing:window#add () in
 437  let _ = vbox#pack ~expand:false ~fill:false ~padding:5 label#coerce in
 438  let scrolled_window0 =
 439   GBin.scrolled_window ~border_width:10
 440    ~packing:(vbox#pack ~expand:true ~padding:5) () in
 441  let _ = scrolled_window0#add output#coerce in
 442  let hbox =
 443   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
 444  let prevb =
 445   GButton.button ~label:"Prev"
 446    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 447  let nextb =
 448   GButton.button ~label:"Next"
 449    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 450  let annotateb =
 451   GButton.button ~label:"Annotate"
 452    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 453  let settingsb =
 454   GButton.button ~label:"Settings"
 455    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 456  let button_export_to_postscript =
 457   GButton.button ~label:"export_to_postscript"
 458   ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 459  let closeb =
 460   GButton.button ~label:"Close"
 461    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 462 object(self)
 463  method nextb = nextb
 464  method prevb = prevb
 465  method label = label
 466  method output = (output : GMathView.math_view)
 467  method show () = window#show ()
 468  initializer
 469   nextb#misc#set_sensitive false ;
 470   prevb#misc#set_sensitive false ;
 471   button_export_to_postscript#misc#set_sensitive false ;
 472
 473   (* signal handlers here *)
 474   ignore(output#connect#jump (jump self)) ;
 475   ignore(output#connect#selection_changed (choose_selection self)) ;
 476   ignore(nextb#connect#clicked (next self)) ;
 477   ignore(prevb#connect#clicked (prev self)) ;
 478   ignore(closeb#connect#clicked (fun _ -> GMain.Main.quit ())) ;
 479   ignore(annotateb#connect#clicked (annotateb_pressed self annotation_window)) ;
 480   let settings_window = new settings_window output scrolled_window0
 481    button_export_to_postscript (jump self) (choose_selection self) in
 482   ignore(settingsb#connect#clicked settings_window#show) ;
 483   ignore(button_export_to_postscript#connect#clicked (export_to_postscript output)) ;
 484   ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true ))
 485 end;;
 486
 487 (* MAIN *)
 488
 489 let initialize_everything tmpfile url =
 490  let module U = Unix in
 491   (* Let's be ready to be remotely controlled *)
 492   let socket = U.socket ~domain:U.PF_INET ~kind:U.SOCK_DGRAM ~protocol:0 in
 493   let address = U.ADDR_INET (U.inet_addr_of_string "127.000.000.001", 8778) in
 494   let buffersize = 2048 in (* are 2048 chars enough? *)
 495   let buffer = String.create buffersize in
 496    try
 497     U.bind socket address ;
 498     U.set_nonblock socket ;
 499     let output = GMathView.math_view ~width:400 ~height:380 ()
 500     and label = GMisc.label ~text:"???" () in
 501      let annotation_window = new annotation_window output label in
 502      let rendering_window =
 503       new rendering_window annotation_window output label
 504      in
 505      let exec_remote_request () =
 506       try
 507        remotejump rendering_window
 508         (String.sub buffer 0 (U.recv socket buffer 0 buffersize []))
 509       with
 510          U.Unix_error (U.EAGAIN,_,_)
 511        | U.Unix_error (U.EWOULDBLOCK,_,_) -> ()
 512      in
 513       ignore (GMain.Timeout.add ~ms:500
 514        ~callback:(fun () -> exec_remote_request () ; true)) ;
 515       rendering_window#show () ;
 516       rendering_window#label#set_text (uri_from_url url) ;
 517       rendering_window#output#load tmpfile ;
 518       GMain.Main.main ()
 519    with
 520     U.Unix_error (_,"bind",_) ->
 521      (* Another copy is already under execution ==> I am a remote control *)
 522      ignore (U.sendto socket url 0 (String.length url) [] address)
 523 ;;
 524
 525 let _ =
 526  let filename = ref "" in
 527  let usage_msg =
 528    "\nusage: mmlinterface[.opt] file url\n\n List of options:"
 529  in
 530   Arg.parse []
 531    (fun x ->
 532      if x = "" then raise (Arg.Bad "Empty filename or URL not allowed") ;
 533      if !filename = "" then
 534       filename := x
 535      else
 536       visited_urls := x :: !visited_urls
 537    ) usage_msg ;
 538   match !visited_urls with
 539      [url] -> initialize_everything !filename url
 540    | _ ->
 541      prerr_string "Exactly one url expected\n" ;
 542      Arg.usage [] usage_msg ;
 543      exit (-1)
 544 ;;