helm/annotationHelper/cicAnnotationHelper.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 let current_url = ref "";;
  55
  56 (* GLOBAL CONSTANTS *)
  57
  58 let helmns = Ominidom.o_mDOMString_of_string "http://www.cs.unibo.it/helm";;
  59
  60 (* MISC FUNCTIONS *)
  61
  62 let pathname_of_annuri uristring =
  63  Configuration.annotations_dir ^
  64   Str.replace_first (Str.regexp "^cic:") "" uristring
  65 ;;
  66
  67 let make_dirs dirpath =
  68  ignore (Unix.system ("mkdir -p " ^ dirpath))
  69 ;;
  70
  71 module UrlManipulator =
  72  struct
  73   exception No_param_dot_CICURI_or_param_dot_annotations_found_in of string;;
  74   exception No_param_found_in of string * string;;
  75   exception Bad_formed_url of string;;
  76
  77   let uri_from_url url =
  78    let module N = Neturl in
  79    let founduri = ref None in
  80    let foundann = ref None in
  81     let rec find_uri =
  82      function
  83         [] -> raise (No_param_dot_CICURI_or_param_dot_annotations_found_in url)
  84       | he::tl ->
  85          match Str.split (Str.regexp "=") he with
  86             ["param.CICURI";uri] ->
  87               if !founduri <> None then
  88                raise (Bad_formed_url url)
  89               else
  90                begin
  91                 founduri := Some uri ;
  92                 if !foundann = None then
  93                  find_uri tl
  94                end
  95           | ["param.annotations";ann] ->
  96               if !foundann <> None then
  97                raise (Bad_formed_url url)
  98               else
  99                begin
 100                 foundann :=
 101                  Some
 102                   (match ann with
 103                       "yes" -> ".ann"
 104                     | "NO"  -> ""
 105                     | _     -> raise (Bad_formed_url url)
 106                   ) ;
 107                 if !founduri = None then
 108                  find_uri tl
 109                end
 110           | _ -> find_uri tl
 111     in
 112      find_uri
 113       (Str.split (Str.regexp "&")
 114        (N.url_query ~encoded:true (N.url_of_string N.ip_url_syntax url))) ;
 115      match !founduri,!foundann with
 116         (Some uri),(Some ann) -> uri ^ ann
 117       | _         , _         ->
 118          raise (No_param_dot_CICURI_or_param_dot_annotations_found_in url)
 119   ;;
 120
 121   let extractParam param url =
 122    let module N = Neturl in
 123     let rec find_param =
 124      function
 125         [] -> raise (No_param_found_in (param,url))
 126       | he::tl ->
 127          match Str.split (Str.regexp "=") he with
 128             [name;value] when name = param -> value
 129           | _ -> find_param tl
 130     in
 131      find_param
 132       (Str.split (Str.regexp "&")
 133        (N.url_query ~encoded:true (N.url_of_string N.ip_url_syntax url)))
 134   ;;
 135
 136   let set_annotations_to_yes query url =
 137    let found =ref false in
 138    let rec aux =
 139     function
 140        [] ->
 141         if !found then ""
 142         else raise (No_param_found_in ("param.annotations",url))
 143      | he::tl ->
 144         match Str.split (Str.regexp "=") he with
 145            ["param.annotations" as s ; ann] ->
 146              found := true ;
 147              let auxtl = aux tl in
 148               s ^ "=yes" ^
 149                (if auxtl = "" then "" else "&" ^ auxtl)
 150          | [name ; value] ->
 151             let auxtl = aux tl in
 152              name ^ "=" ^ value ^
 153               (if auxtl = "" then "" else "&" ^ auxtl)
 154          | [name] ->
 155             let auxtl = aux tl in
 156              name ^ "=" ^
 157               (if auxtl = "" then "" else "&" ^ auxtl)
 158          | _ -> raise (Bad_formed_url url)
 159    in
 160     aux (Str.split (Str.regexp "&") query)
 161   ;;
 162
 163   let annurl_of_url url =
 164    let module N = Neturl in
 165     let nurl = N.url_of_string N.ip_url_syntax url in
 166      let query = N.url_query ~encoded:true nurl in
 167      let newquery = set_annotations_to_yes query url in
 168       N.string_of_url (N.modify_url ~encoded:true ~query:newquery nurl)
 169   ;;
 170 end
 171
 172 let get_current_uri () =
 173  UriManager.uri_of_string (UrlManipulator.uri_from_url !current_url)
 174 ;;
 175
 176 (* CALLBACKS *)
 177
 178 let get_annotated_obj () =
 179  match !annotated_obj with
 180     None   ->
 181      let annobj =
 182       (CicCache.get_annobj (get_current_uri ()))
 183      in
 184       annotated_obj := Some annobj ;
 185       annobj
 186   | Some annobj -> annobj
 187 ;;
 188
 189 let update_output rendering_window url =
 190  rendering_window#label#set_text (UrlManipulator.uri_from_url url) ;
 191  rendering_window#output#load url
 192 ;;
 193
 194 let choose_selection rendering_window (node : Ominidom.o_mDOMNode option) =
 195  let module O = Ominidom in
 196   let rec aux node =
 197    match node#get_attribute_ns (O.o_mDOMString_of_string "xref") helmns with
 198      Some _ -> rendering_window#output#set_selection (Some node)
 199    | None   -> aux (node#get_parent)
 200   in
 201    match node with
 202      Some x -> aux x
 203    | None   -> rendering_window#output#set_selection None
 204 ;;
 205
 206 let annotateb_pressed rendering_window annotation_window () =
 207  let module O = Ominidom in
 208  match rendering_window#output#get_selection with
 209    Some node ->
 210     begin
 211      match (node#get_attribute_ns (O.o_mDOMString_of_string "xref") helmns) with
 212         Some xpath ->
 213          let annobj = get_annotated_obj ()
 214          and annotation = (annotation_window#annotation : GEdit.text) in
 215           ann := CicXPath.get_annotation annobj (xpath#get_string) ;
 216           CicAnnotationHinter.create_hints annotation_window annobj
 217            (xpath#get_string) ;
 218           annotation#delete_text 0 annotation#length ;
 219           begin
 220            match !(!ann) with
 221                None      ->
 222                 annotation#misc#set_sensitive false ;
 223                 annotation_window#radio_none#set_active true ;
 224                 radio_some_status := false
 225              | Some ann' ->
 226                 annotation#insert ann' ;
 227                 annotation#misc#set_sensitive true ;
 228                 annotation_window#radio_some#set_active true ;
 229                 radio_some_status := true
 230           end ;
 231           GMain.Grab.add (annotation_window#window_to_annotate#coerce) ;
 232           annotation_window#show () ;
 233      | None -> rendering_window#label#set_text ("ERROR: No xref found!!!\n")
 234     end
 235  | None -> rendering_window#label#set_text ("ERROR: No selection!!!\n")
 236 ;;
 237
 238 (* called when the annotation is confirmed *)
 239 let save_annotation annotation =
 240  let module S = Str in
 241  let module U = UriManager in
 242   if !radio_some_status then
 243    !ann := Some (annotation#get_chars 0 annotation#length)
 244   else
 245    !ann := None ;
 246   match !annotated_obj with
 247      None -> assert false
 248    | Some (annobj,_) ->
 249       let uri = get_current_uri () in
 250        let annxml = CicAnnotation2Xml.pp_annotation annobj uri in
 251         make_dirs
 252           (pathname_of_annuri (U.buri_of_uri uri)) ;
 253         Xml.pp ~quiet:true annxml
 254          (Some
 255           (pathname_of_annuri (U.string_of_uri (U.annuri_of_uri uri)) ^
 256            ".xml"
 257           )
 258          )
 259 ;;
 260
 261 (* STUFF TO BUILD THE GTK INTERFACE *)
 262
 263 (* Stuff for the widget settings *)
 264
 265 let export_to_postscript (output : GMathView.math_view) () =
 266  output#export_to_postscript ~filename:"output.ps" ();
 267 ;;
 268
 269 let activate_t1 output button_set_anti_aliasing button_set_kerning
 270  button_set_transparency button_export_to_postscript button_t1 ()
 271 =
 272  let is_set = button_t1#active in
 273   output#set_font_manager_type
 274    (if is_set then `font_manager_t1 else `font_manager_gtk) ;
 275   if is_set then
 276    begin
 277     button_set_anti_aliasing#misc#set_sensitive true ;
 278     button_set_kerning#misc#set_sensitive true ;
 279     button_set_transparency#misc#set_sensitive true ;
 280     button_export_to_postscript#misc#set_sensitive true ;
 281    end
 282   else
 283    begin
 284     button_set_anti_aliasing#misc#set_sensitive false ;
 285     button_set_kerning#misc#set_sensitive false ;
 286     button_set_transparency#misc#set_sensitive false ;
 287     button_export_to_postscript#misc#set_sensitive false ;
 288    end
 289 ;;
 290
 291 let set_anti_aliasing output button_set_anti_aliasing () =
 292  output#set_anti_aliasing button_set_anti_aliasing#active
 293 ;;
 294
 295 let set_kerning output button_set_kerning () =
 296  output#set_kerning button_set_kerning#active
 297 ;;
 298
 299 let set_transparency output button_set_transparency () =
 300  output#set_transparency button_set_transparency#active
 301 ;;
 302
 303 let changefont output font_size_spinb () =
 304  output#set_font_size font_size_spinb#value_as_int
 305 ;;
 306
 307 let set_log_verbosity output log_verbosity_spinb () =
 308  output#set_log_verbosity log_verbosity_spinb#value_as_int
 309 ;;
 310
 311 class settings_window output sw button_export_to_postscript
 312  selection_changed_callback
 313 =
 314  let settings_window = GWindow.window ~title:"GtkMathView settings" () in
 315  let vbox =
 316   GPack.vbox ~packing:settings_window#add () in
 317  let table =
 318   GPack.table
 319    ~rows:1 ~columns:3 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
 320    ~border_width:5 ~packing:vbox#add () in
 321  let button_t1 =
 322   GButton.toggle_button ~label:"activate t1 fonts"
 323    ~packing:(table#attach ~left:0 ~top:0) () in
 324  let button_set_anti_aliasing =
 325   GButton.toggle_button ~label:"set_anti_aliasing"
 326    ~packing:(table#attach ~left:0 ~top:1) () in
 327  let button_set_kerning =
 328   GButton.toggle_button ~label:"set_kerning"
 329    ~packing:(table#attach ~left:1 ~top:1) () in
 330  let button_set_transparency =
 331   GButton.toggle_button ~label:"set_transparency"
 332    ~packing:(table#attach ~left:2 ~top:1) () in
 333  let table =
 334   GPack.table
 335    ~rows:2 ~columns:2 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
 336    ~border_width:5 ~packing:vbox#add () in
 337  let font_size_label =
 338   GMisc.label ~text:"font size:"
 339    ~packing:(table#attach ~left:0 ~top:0 ~expand:`NONE) () in
 340  let font_size_spinb =
 341   let sadj =
 342    GData.adjustment ~value:14.0 ~lower:5.0 ~upper:50.0 ~step_incr:1.0 ()
 343   in
 344    GEdit.spin_button
 345     ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:0 ~fill:`NONE) () in
 346  let log_verbosity_label =
 347   GMisc.label ~text:"log verbosity:"
 348    ~packing:(table#attach ~left:0 ~top:1) () in
 349  let log_verbosity_spinb =
 350   let sadj =
 351    GData.adjustment ~value:0.0 ~lower:0.0 ~upper:3.0 ~step_incr:1.0 ()
 352   in
 353    GEdit.spin_button
 354     ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:1) () in
 355  let hbox =
 356   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
 357  let closeb =
 358   GButton.button ~label:"Close"
 359    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 360 object(self)
 361  method show = settings_window#show
 362  initializer
 363   button_set_anti_aliasing#misc#set_sensitive false ;
 364   button_set_kerning#misc#set_sensitive false ;
 365   button_set_transparency#misc#set_sensitive false ;
 366   (* Signals connection *)
 367   ignore(button_t1#connect#clicked
 368    (activate_t1 output button_set_anti_aliasing button_set_kerning
 369     button_set_transparency button_export_to_postscript button_t1)) ;
 370   ignore(font_size_spinb#connect#changed (changefont output font_size_spinb)) ;
 371   ignore(button_set_anti_aliasing#connect#toggled
 372    (set_anti_aliasing output button_set_anti_aliasing));
 373   ignore(button_set_kerning#connect#toggled
 374    (set_kerning output button_set_kerning)) ;
 375   ignore(button_set_transparency#connect#toggled
 376    (set_transparency output button_set_transparency)) ;
 377   ignore(log_verbosity_spinb#connect#changed
 378    (set_log_verbosity output log_verbosity_spinb)) ;
 379   ignore(closeb#connect#clicked settings_window#misc#hide)
 380 end;;
 381
 382 (* Main windows *)
 383
 384 class annotation_window output label =
 385  let window_to_annotate =
 386   GWindow.window ~title:"Annotating environment" ~border_width:2 () in
 387  let hbox1 =
 388   GPack.hbox ~packing:window_to_annotate#add () in
 389  let vbox1 =
 390   GPack.vbox ~packing:(hbox1#pack ~padding:5) () in
 391  let hbox2 =
 392   GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
 393  let radio_some = GButton.radio_button ~label:"Annotation below"
 394   ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
 395  let radio_none = GButton.radio_button ~label:"No annotation"
 396   ~group:radio_some#group
 397   ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5)
 398   ~active:true () in
 399  let annotation = GEdit.text ~editable:true ~width:400 ~height:180
 400   ~packing:(vbox1#pack ~padding:5) () in
 401  let table =
 402   GPack.table ~rows:3 ~columns:3 ~packing:(vbox1#pack ~padding:5) () in
 403  let annotation_hints =
 404   Array.init 9
 405    (function i ->
 406      GButton.button ~label:("Hint " ^ string_of_int i)
 407       ~packing:(table#attach ~left:(i mod 3) ~top:(i / 3)) ()
 408    ) in
 409  let vbox2 =
 410   GPack.vbox ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
 411  let confirmb =
 412   GButton.button ~label:"O.K."
 413    ~packing:(vbox2#pack ~expand:false ~fill:false ~padding:5) () in
 414  let abortb =
 415   GButton.button ~label:"Abort"
 416    ~packing:(vbox2#pack ~expand:false ~fill:false ~padding:5) () in
 417 object (self)
 418  method window_to_annotate = window_to_annotate
 419  method annotation = annotation
 420  method radio_some = radio_some
 421  method radio_none = radio_none
 422  method annotation_hints = annotation_hints
 423  method output = (output : GMathView.math_view)
 424  method show () = window_to_annotate#show ()
 425  initializer
 426   (* signal handlers here *)
 427   ignore (window_to_annotate#event#connect#delete
 428    (fun _ ->
 429      window_to_annotate#misc#hide () ;
 430      GMain.Grab.remove (window_to_annotate#coerce) ;
 431      true
 432    )) ;
 433   ignore (confirmb#connect#clicked
 434    (fun () ->
 435      window_to_annotate#misc#hide () ;
 436      save_annotation annotation ;
 437      GMain.Grab.remove (window_to_annotate#coerce) ;
 438      let new_current_uri = UriManager.annuri_of_uri (get_current_uri ()) in
 439       Getter.register new_current_uri
 440        (Configuration.annotations_url ^
 441          Str.replace_first (Str.regexp "^cic:") ""
 442           (UriManager.string_of_uri new_current_uri) ^ ".xml"
 443        ) ;
 444       let new_current_url = UrlManipulator.annurl_of_url !current_url in
 445        current_url := new_current_url ;
 446        label#set_text (UriManager.string_of_uri new_current_uri) ;
 447        output#load new_current_url
 448    )) ;
 449   ignore (abortb#connect#clicked
 450    (fun () ->
 451      window_to_annotate#misc#hide () ;
 452      GMain.Grab.remove (window_to_annotate#coerce)
 453    ));
 454   ignore (radio_some#connect#clicked
 455    (fun () -> annotation#misc#set_sensitive true ; radio_some_status := true)) ;
 456   ignore (radio_none #connect#clicked
 457    (fun () ->
 458      annotation#misc#set_sensitive false;
 459      radio_some_status := false)
 460    )
 461 end;;
 462
 463 class rendering_window annotation_window output (label : GMisc.label) =
 464  let window =
 465   GWindow.window ~title:"MathML viewer" ~border_width:2 () in
 466  let vbox =
 467   GPack.vbox ~packing:window#add () in
 468  let _ = vbox#pack ~expand:false ~fill:false ~padding:5 label#coerce in
 469  let scrolled_window0 =
 470   GBin.scrolled_window ~border_width:10
 471    ~packing:(vbox#pack ~expand:true ~padding:5) () in
 472  let _ = scrolled_window0#add output#coerce in
 473  let hbox =
 474   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
 475  let annotateb =
 476   GButton.button ~label:"Annotate"
 477    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 478  let settingsb =
 479   GButton.button ~label:"Settings"
 480    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 481  let button_export_to_postscript =
 482   GButton.button ~label:"export_to_postscript"
 483   ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 484  let closeb =
 485   GButton.button ~label:"Close"
 486    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 487 object(self)
 488  method label = label
 489  method output = (output : GMathView.math_view)
 490  method show () = window#show ()
 491  initializer
 492   button_export_to_postscript#misc#set_sensitive false ;
 493
 494   (* signal handlers here *)
 495   ignore(output#connect#selection_changed (choose_selection self)) ;
 496   ignore(closeb#connect#clicked (fun _ -> GMain.Main.quit ())) ;
 497   ignore(annotateb#connect#clicked (annotateb_pressed self annotation_window)) ;
 498   let settings_window = new settings_window output scrolled_window0
 499    button_export_to_postscript (choose_selection self) in
 500   ignore(settingsb#connect#clicked settings_window#show) ;
 501   ignore(button_export_to_postscript#connect#clicked (export_to_postscript output)) ;
 502   ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true ))
 503 end;;
 504
 505 (* MAIN *)
 506
 507 let initialize_everything tmpfile url =
 508  let module U = Unix in
 509   let output = GMathView.math_view ~width:400 ~height:380 ()
 510    and label = GMisc.label ~text:"???" () in
 511     let annotation_window = new annotation_window output label in
 512     let rendering_window =
 513      new rendering_window annotation_window output label
 514     in
 515      rendering_window#show () ;
 516      rendering_window#label#set_text (UrlManipulator.uri_from_url url) ;
 517      rendering_window#output#load tmpfile ;
 518      GMain.Main.main ()
 519 ;;
 520
 521 let _ =
 522  let filename = ref "" in
 523  let usage_msg =
 524    "\nusage: annotationHelper[.opt] file url\n\n List of options:"
 525  in
 526   Arg.parse []
 527    (fun x ->
 528      if x = "" then raise (Arg.Bad "Empty filename or URL not allowed") ;
 529      if !filename = "" then
 530       filename := x
 531      else if !current_url = "" then
 532       current_url := x
 533      else
 534       begin
 535        prerr_string "More than two arguments provided\n" ;
 536        Arg.usage [] usage_msg ;
 537        exit (-1)
 538       end
 539    ) usage_msg ;
 540    Getter.getter_url :=
 541     Netencoding.Url.decode
 542      (UrlManipulator.extractParam "param.getterURL" !current_url) ;
 543    initialize_everything !filename !current_url
 544 ;;