(* Copyright (C) 2000, HELM Team. * * This file is part of HELM, an Hypertextual, Electronic * Library of Mathematics, developed at the Computer Science * Department, University of Bologna, Italy. * * HELM is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License * as published by the Free Software Foundation; either version 2 * of the License, or (at your option) any later version. * * HELM is distributed in the hope that it will be useful, * but WITHOUT ANY WARRANTY; without even the implied warranty of * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the * GNU General Public License for more details. * * You should have received a copy of the GNU General Public License * along with HELM; if not, write to the Free Software * Foundation, Inc., 59 Temple Place - Suite 330, Boston, * MA 02111-1307, USA. * * For details, see the HELM World-Wide-Web page, * http://cs.unibo.it/helm/. *) (******************************************************************************) (* *) (* PROJECT HELM *) (* *) (* Claudio Sacerdoti Coen *) (* 03/04/2001 *) (* *) (* This is a simple gtk interface to the Coq-like pretty printer cicPp for *) (* cic terms exported in xml. It uses directly the modules cicPp and *) (* cicCcache and indirectly all the other modules (cicParser, cicParser2, *) (* cicParser3, getter). *) (* The syntax is "gtkInterface[.opt] filename1 ... filenamen" where *) (* filenamei is the path-name of an xml file describing a cic term. *) (* The terms are loaded in cache and then pretty-printed one at a time and *) (* only once, when the user wants to look at it: if the user wants to look at *) (* a term again, then the pretty-printed term is showed again, but not *) (* recomputed *) (* *) (******************************************************************************) (* GLOBAL REFERENCES (USED BY CALLBACKS) *) let annotated_obj = ref None;; (* reference to a couple option where *) (* the first component is the current *) (* annotated object and the second is *) (* the map from ids to annotated targets *) let ann = ref (ref None);; (* current annotation *) let radio_some_status = ref false;; (* is the radio_some button selected? *) let current_url = ref "";; (* MISC FUNCTIONS *) let pathname_of_annuri uristring = Configuration.annotations_dir ^ Str.replace_first (Str.regexp "^cic:") "" uristring ;; let make_dirs dirpath = ignore (Unix.system ("mkdir -p " ^ dirpath)) ;; exception No_param_dot_CICURI_or_param_dot_annotations_found_in of string;; exception Bad_formed_url of string;; let uri_from_url url = let module N = Neturl in let founduri = ref None in let foundann = ref None in let rec find_uri = function [] -> raise (No_param_dot_CICURI_or_param_dot_annotations_found_in url) | he::tl -> match Str.split (Str.regexp "=") he with ["param.CICURI";uri] -> if !founduri <> None then raise (Bad_formed_url url) else begin founduri := Some uri ; if !foundann = None then find_uri tl end | ["param.annotations";ann] -> if !foundann <> None then raise (Bad_formed_url url) else begin foundann := Some (match ann with "yes" -> ".ann" | "NO" -> "" | _ -> raise (Bad_formed_url url) ) ; if !founduri = None then find_uri tl end | _ -> find_uri tl in find_uri (Str.split (Str.regexp "&") (N.url_query ~encoded:true (N.url_of_string N.ip_url_syntax url))) ; match !founduri,!foundann with (Some uri),(Some ann) -> uri ^ ann | _ , _ -> raise (No_param_dot_CICURI_or_param_dot_annotations_found_in url) ;; let get_current_uri () = UriManager.uri_of_string (uri_from_url !current_url) ;; (* CALLBACKS *) let get_annotated_obj () = match !annotated_obj with None -> let annobj = (CicCache.get_annobj (get_current_uri ())) in annotated_obj := Some annobj ; annobj | Some annobj -> annobj ;; let update_output rendering_window url = rendering_window#label#set_text (uri_from_url url) ; rendering_window#output#load url ;; (* called when an hyperlink is clicked *) let jump rendering_window (node : Ominidom.o_mDOMNode) = let module O = Ominidom in let module U = Unix in match (node#get_attribute (O.o_mDOMString_of_string "href")) with Some str -> let frameseturl = str#get_string in let devnull = U.openfile "/dev/null" [U.O_RDWR] 0o600 in ignore (U.create_process "netscape-remote" [|"netscape-remote" ; "-noraise" ; "-remote" ; "openURL(" ^ frameseturl ^ ",cic)" |] devnull devnull devnull) | None -> assert false ;; (* called by the remote control *) let remotejump rendering_window url = current_url := url ; update_output rendering_window url ;; let choose_selection rendering_window (node : Ominidom.o_mDOMNode option) = let module O = Ominidom in let rec aux node = match node#get_attribute (O.o_mDOMString_of_string "xref") with Some _ -> rendering_window#output#set_selection (Some node) | None -> aux (node#get_parent) in match node with Some x -> aux x | None -> rendering_window#output#set_selection None ;; let annotateb_pressed rendering_window annotation_window () = let module O = Ominidom in match rendering_window#output#get_selection with Some node -> begin match (node#get_attribute (O.o_mDOMString_of_string "xref")) with Some xpath -> let annobj = get_annotated_obj () and annotation = (annotation_window#annotation : GEdit.text) in ann := CicXPath.get_annotation annobj (xpath#get_string) ; CicAnnotationHinter.create_hints annotation_window annobj (xpath#get_string) ; annotation#delete_text 0 annotation#length ; begin match !(!ann) with None -> annotation#misc#set_sensitive false ; annotation_window#radio_none#set_active true ; radio_some_status := false | Some ann' -> annotation#insert ann' ; annotation#misc#set_sensitive true ; annotation_window#radio_some#set_active true ; radio_some_status := true end ; GMain.Grab.add (annotation_window#window_to_annotate#coerce) ; annotation_window#show () ; | None -> rendering_window#label#set_text ("ERROR: No xref found!!!\n") end | None -> rendering_window#label#set_text ("ERROR: No selection!!!\n") ;; (* called when the annotation is confirmed *) let save_annotation annotation = let module S = Str in let module U = UriManager in if !radio_some_status then !ann := Some (annotation#get_chars 0 annotation#length) else !ann := None ; match !annotated_obj with None -> assert false | Some (annobj,_) -> let uri = get_current_uri () in let annxml = Annotation2Xml.pp_annotation annobj uri in make_dirs (pathname_of_annuri (U.buri_of_uri uri)) ; Xml.pp ~quiet:true annxml (Some (pathname_of_annuri (U.string_of_uri (U.annuri_of_uri uri)) ^ ".xml" ) ) ;; (* STUFF TO BUILD THE GTK INTERFACE *) (* Stuff for the widget settings *) let export_to_postscript (output : GMathView.math_view) () = output#export_to_postscript ~filename:"output.ps" (); ;; let activate_t1 output button_set_anti_aliasing button_set_kerning button_export_to_postscript button_t1 () = let is_set = button_t1#active in output#set_font_manager_type (if is_set then `font_manager_t1 else `font_manager_gtk) ; if is_set then begin button_set_anti_aliasing#misc#set_sensitive true ; button_set_kerning#misc#set_sensitive true ; button_export_to_postscript#misc#set_sensitive true ; end else begin button_set_anti_aliasing#misc#set_sensitive false ; button_set_kerning#misc#set_sensitive false ; button_export_to_postscript#misc#set_sensitive false ; end ;; let set_anti_aliasing output button_set_anti_aliasing () = output#set_anti_aliasing button_set_anti_aliasing#active ;; let set_kerning output button_set_kerning () = output#set_kerning button_set_kerning#active ;; let changefont output font_size_spinb () = output#set_font_size font_size_spinb#value_as_int ;; let set_log_verbosity output log_verbosity_spinb () = output#set_log_verbosity log_verbosity_spinb#value_as_int ;; class settings_window output sw button_export_to_postscript jump_callback selection_changed_callback = let settings_window = GWindow.window ~title:"GtkMathView settings" () in let vbox = GPack.vbox ~packing:settings_window#add () in let table = GPack.table ~rows:1 ~columns:3 ~homogeneous:false ~row_spacings:5 ~col_spacings:5 ~border_width:5 ~packing:vbox#add () in let button_t1 = GButton.toggle_button ~label:"activate t1 fonts" ~packing:(table#attach ~left:0 ~top:0) () in let button_set_anti_aliasing = GButton.toggle_button ~label:"set_anti_aliasing" ~packing:(table#attach ~left:1 ~top:0) () in let button_set_kerning = GButton.toggle_button ~label:"set_kerning" ~packing:(table#attach ~left:2 ~top:0) () in let table = GPack.table ~rows:2 ~columns:2 ~homogeneous:false ~row_spacings:5 ~col_spacings:5 ~border_width:5 ~packing:vbox#add () in let font_size_label = GMisc.label ~text:"font size:" ~packing:(table#attach ~left:0 ~top:0 ~expand:`NONE) () in let font_size_spinb = let sadj = GData.adjustment ~value:14.0 ~lower:5.0 ~upper:50.0 ~step_incr:1.0 () in GEdit.spin_button ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:0 ~fill:`NONE) () in let log_verbosity_label = GMisc.label ~text:"log verbosity:" ~packing:(table#attach ~left:0 ~top:1) () in let log_verbosity_spinb = let sadj = GData.adjustment ~value:0.0 ~lower:0.0 ~upper:3.0 ~step_incr:1.0 () in GEdit.spin_button ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:1) () in let hbox = GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in let closeb = GButton.button ~label:"Close" ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in object(self) method show = settings_window#show initializer button_set_anti_aliasing#misc#set_sensitive false ; button_set_kerning#misc#set_sensitive false ; (* Signals connection *) ignore(button_t1#connect#clicked (activate_t1 output button_set_anti_aliasing button_set_kerning button_export_to_postscript button_t1)) ; ignore(font_size_spinb#connect#changed (changefont output font_size_spinb)) ; ignore(button_set_anti_aliasing#connect#toggled (set_anti_aliasing output button_set_anti_aliasing)); ignore(button_set_kerning#connect#toggled (set_kerning output button_set_kerning)) ; ignore(log_verbosity_spinb#connect#changed (set_log_verbosity output log_verbosity_spinb)) ; ignore(closeb#connect#clicked settings_window#misc#hide) end;; (* Main windows *) class annotation_window output label = let window_to_annotate = GWindow.window ~title:"Annotating environment" ~border_width:2 () in let hbox1 = GPack.hbox ~packing:window_to_annotate#add () in let vbox1 = GPack.vbox ~packing:(hbox1#pack ~padding:5) () in let hbox2 = GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in let radio_some = GButton.radio_button ~label:"Annotation below" ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in let radio_none = GButton.radio_button ~label:"No annotation" ~group:radio_some#group ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) ~active:true () in let annotation = GEdit.text ~editable:true ~width:400 ~height:180 ~packing:(vbox1#pack ~padding:5) () in let table = GPack.table ~rows:3 ~columns:3 ~packing:(vbox1#pack ~padding:5) () in let annotation_hints = Array.init 9 (function i -> GButton.button ~label:("Hint " ^ string_of_int i) ~packing:(table#attach ~left:(i mod 3) ~top:(i / 3)) () ) in let vbox2 = GPack.vbox ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in let confirmb = GButton.button ~label:"O.K." ~packing:(vbox2#pack ~expand:false ~fill:false ~padding:5) () in let abortb = GButton.button ~label:"Abort" ~packing:(vbox2#pack ~expand:false ~fill:false ~padding:5) () in object (self) method window_to_annotate = window_to_annotate method annotation = annotation method radio_some = radio_some method radio_none = radio_none method annotation_hints = annotation_hints method output = (output : GMathView.math_view) method show () = window_to_annotate#show () initializer (* signal handlers here *) ignore (window_to_annotate#event#connect#delete (fun _ -> window_to_annotate#misc#hide () ; GMain.Grab.remove (window_to_annotate#coerce) ; true )) ; ignore (confirmb#connect#clicked (fun () -> window_to_annotate#misc#hide () ; save_annotation annotation ; GMain.Grab.remove (window_to_annotate#coerce) ; let new_current_uri = UriManager.annuri_of_uri (get_current_uri ()) in Getter.register new_current_uri (Configuration.annotations_url ^ Str.replace_first (Str.regexp "^cic:") "" (UriManager.string_of_uri new_current_uri) ^ ".xml" ) ; (*CSC: corretto, up to XsltProcessor.url_of_uri let new_current_url = XsltProcessor.url_of_uri new_current_uri in current_url := new_current_url ; label#set_text (UriManager.string_of_uri new_current_uri) ; output#load new_current_url *) () )) ; ignore (abortb#connect#clicked (fun () -> window_to_annotate#misc#hide () ; GMain.Grab.remove (window_to_annotate#coerce) )); ignore (radio_some#connect#clicked (fun () -> annotation#misc#set_sensitive true ; radio_some_status := true)) ; ignore (radio_none #connect#clicked (fun () -> annotation#misc#set_sensitive false; radio_some_status := false) ) end;; class rendering_window annotation_window output (label : GMisc.label) = let window = GWindow.window ~title:"MathML viewer" ~border_width:2 () in let vbox = GPack.vbox ~packing:window#add () in let _ = vbox#pack ~expand:false ~fill:false ~padding:5 label#coerce in let scrolled_window0 = GBin.scrolled_window ~border_width:10 ~packing:(vbox#pack ~expand:true ~padding:5) () in let _ = scrolled_window0#add output#coerce in let hbox = GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in let annotateb = GButton.button ~label:"Annotate" ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in let settingsb = GButton.button ~label:"Settings" ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in let button_export_to_postscript = GButton.button ~label:"export_to_postscript" ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in let closeb = GButton.button ~label:"Close" ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in object(self) method label = label method output = (output : GMathView.math_view) method show () = window#show () initializer button_export_to_postscript#misc#set_sensitive false ; (* signal handlers here *) ignore(output#connect#jump (jump self)) ; ignore(output#connect#selection_changed (choose_selection self)) ; ignore(closeb#connect#clicked (fun _ -> GMain.Main.quit ())) ; ignore(annotateb#connect#clicked (annotateb_pressed self annotation_window)) ; let settings_window = new settings_window output scrolled_window0 button_export_to_postscript (jump self) (choose_selection self) in ignore(settingsb#connect#clicked settings_window#show) ; ignore(button_export_to_postscript#connect#clicked (export_to_postscript output)) ; ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) end;; (* MAIN *) let initialize_everything tmpfile url = let module U = Unix in (* Let's be ready to be remotely controlled *) let socket = U.socket ~domain:U.PF_INET ~kind:U.SOCK_DGRAM ~protocol:0 in let address = U.ADDR_INET (U.inet_addr_of_string "127.000.000.001", 8778) in let buffersize = 2048 in (* are 2048 chars enough? *) let buffer = String.create buffersize in try U.bind socket address ; U.set_nonblock socket ; let output = GMathView.math_view ~width:400 ~height:380 () and label = GMisc.label ~text:"???" () in let annotation_window = new annotation_window output label in let rendering_window = new rendering_window annotation_window output label in let exec_remote_request () = try remotejump rendering_window (String.sub buffer 0 (U.recv socket buffer 0 buffersize [])) with U.Unix_error (U.EAGAIN,_,_) | U.Unix_error (U.EWOULDBLOCK,_,_) -> () in ignore (GMain.Timeout.add ~ms:500 ~callback:(fun () -> exec_remote_request () ; true)) ; rendering_window#show () ; rendering_window#label#set_text (uri_from_url url) ; rendering_window#output#load tmpfile ; GMain.Main.main () with U.Unix_error (_,"bind",_) -> (* Another copy is already under execution ==> I am a remote control *) ignore (U.sendto socket url 0 (String.length url) [] address) ;; let _ = let filename = ref "" in let usage_msg = "\nusage: mmlinterface[.opt] file url\n\n List of options:" in Arg.parse [] (fun x -> if x = "" then raise (Arg.Bad "Empty filename or URL not allowed") ; if !filename = "" then filename := x else if !current_url = "" then current_url := x else begin prerr_string "More than two arguments provided\n" ; Arg.usage [] usage_msg ; exit (-1) end ) usage_msg ; initialize_everything !filename !current_url ;;