From: Claudio Sacerdoti Coen Date: Wed, 11 Apr 2001 11:00:59 +0000 (+0000) Subject: Unstable commit: just before removing next/prev functionalities X-Git-Tag: v0_1_2~24 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=55b6c7c60e7406f06b324fb5b0eb0f34dacf3dfc;p=helm.git Unstable commit: just before removing next/prev functionalities --- diff --git a/helm/interface/mmlinterface.ml b/helm/interface/mmlinterface.ml index b95303d2f..037f1b132 100755 --- a/helm/interface/mmlinterface.ml +++ b/helm/interface/mmlinterface.ml @@ -28,7 +28,7 @@ (* PROJECT HELM *) (* *) (* Claudio Sacerdoti Coen *) -(* 24/01/2000 *) +(* 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 *) @@ -43,79 +43,6 @@ (* *) (******************************************************************************) -(* DEFINITION OF THE URI TREE AND USEFUL FUNCTIONS ON IT *) - -type item = - Dir of string * item list ref - | File of string * UriManager.uri -;; - -let uritree = ref [] -let theoryuritree = ref [] - -let get_name = - function - Dir (name,_) -> name - | File (name,_) -> name -;; - -let get_uri = - function - Dir _ -> None - | File (_,uri) -> Some uri -;; - -(* STUFF TO BUILD THE URI TREE *) - -exception EmptyUri -exception DuplicatedUri -exception ConflictingUris - -let insert_in_uri_tree uri = - let rec aux l = - function - [name] -> - (try - let _ = List.find (fun item -> name = get_name item) !l in - raise DuplicatedUri - with - Not_found -> l := (File (name,uri))::!l - ) - | name::tl -> - (try - match List.find (fun item -> name = get_name item) !l with - Dir (_,children) -> aux children tl - | File _ -> raise ConflictingUris - with - Not_found -> - let children = ref [] in - l := (Dir (name,children))::!l ; - aux children tl - ) - | [] -> raise EmptyUri - in - aux -;; - -(* Imperative procedure that builds the two uri trees *) -let build_uri_tree () = - let dbh = Dbm.opendbm Configuration.uris_dbm [Dbm.Dbm_rdonly] 0 in - Dbm.iter - (fun uri _ -> - let cicregexp = Str.regexp "cic:" - and theoryregexp = Str.regexp "theory:" in - if Str.string_match cicregexp uri 0 then - let s = Str.replace_first cicregexp "" uri in - let l = Str.split (Str.regexp "/") s in - insert_in_uri_tree (UriManager.uri_of_string uri) uritree l - else if Str.string_match theoryregexp uri 0 then - let s = Str.replace_first theoryregexp "" uri in - let l = Str.split (Str.regexp "/") s in - insert_in_uri_tree (UriManager.uri_of_string uri) theoryuritree l - ) dbh ; - Dbm.close dbh -;; - (* GLOBAL REFERENCES (USED BY CALLBACKS) *) let annotated_obj = ref None;; (* reference to a couple option where *) @@ -125,28 +52,57 @@ let annotated_obj = ref None;; (* reference to a couple option where *) let ann = ref (ref None);; (* current annotation *) let radio_some_status = ref false;; (* is the radio_some button selected? *) -let theory_visited_uris = ref [];; -let theory_to_visit_uris = ref [];; -let visited_uris = ref [];; -let to_visit_uris = ref [];; +let visited_urls = (ref [] : string list ref);; +let to_visit_urls = ref [];; -(* CALLBACKS *) +exception No_param_dot_CICURI_found_in of string;; +exception Unexpected_URL_format of string;; + +(*CSC: never used: Urrah!!! +let url_from_frameseturl frameseturl = + let module N = Neturl in + let l = + (Str.split (Str.regexp "=") + (N.url_query ~encoded:true (N.url_of_string N.ip_url_syntax frameseturl))) + in + match l with + [_ ; url] -> Netencoding.Url.decode url + | _ -> raise (Unexpected_URL_format frameseturl) +;; +*) + +let uri_from_url url = + let module N = Neturl in + let rec find_uri = + function + [] -> raise (No_param_dot_CICURI_found_in url) + | he::tl -> + match Str.split (Str.regexp "=") he with + ["param.CICURI";uri] -> uri + | _ -> find_uri tl + in + find_uri + (Str.split (Str.regexp "&") + (N.url_query ~encoded:true (N.url_of_string N.ip_url_syntax url))) +;; + +(* MISC FUNCTIONS *) -exception NoCurrentUri;; -exception NoNextOrPrevUri;; +exception NoCurrentUrl;; +exception NoNextOrPrevUrl;; -let theory_get_current_uri () = - match !theory_visited_uris with - [] -> raise NoCurrentUri - | uri::_ -> uri +let get_current_url () = + match !visited_urls with + [] -> raise NoCurrentUrl + | url::_ -> url ;; let get_current_uri () = - match !visited_uris with - [] -> raise NoCurrentUri - | uri::_ -> uri + UriManager.uri_of_string (uri_from_url (get_current_url ())) ;; +(* CALLBACKS *) + let get_annotated_obj () = match !annotated_obj with None -> @@ -158,69 +114,31 @@ let get_annotated_obj () = | Some annobj -> annobj ;; -let filename_of_uri uri = - Getter.get uri -;; - -let theory_update_output rendering_window uri = - rendering_window#label#set_text (UriManager.string_of_uri uri) ; - ignore (rendering_window#errors#delete_text 0 rendering_window#errors#length) ; - let mmlfile = XsltProcessor.process uri true "theory" in - rendering_window#output#load mmlfile -;; - -let update_output rendering_window uri = - rendering_window#label#set_text (UriManager.string_of_uri uri) ; - ignore (rendering_window#errors#delete_text 0 rendering_window#errors#length) ; - let mmlfile = XsltProcessor.process uri true "cic" in - rendering_window#output#load mmlfile -;; - -let theory_next rendering_window () = - match !theory_to_visit_uris with - [] -> raise NoNextOrPrevUri - | uri::tl -> - theory_to_visit_uris := tl ; - theory_visited_uris := uri::!theory_visited_uris ; - theory_update_output rendering_window uri ; - rendering_window#prevb#misc#set_sensitive true ; - if tl = [] then - rendering_window#nextb#misc#set_sensitive false +let update_output rendering_window url = + rendering_window#label#set_text (uri_from_url url) ; + rendering_window#output#load url ;; let next rendering_window () = - match !to_visit_uris with - [] -> raise NoNextOrPrevUri - | uri::tl -> - to_visit_uris := tl ; - visited_uris := uri::!visited_uris ; + match !to_visit_urls with + [] -> raise NoNextOrPrevUrl + | url::tl -> + to_visit_urls := tl ; + visited_urls := url::!visited_urls ; annotated_obj := None ; - update_output rendering_window uri ; + update_output rendering_window url ; rendering_window#prevb#misc#set_sensitive true ; if tl = [] then rendering_window#nextb#misc#set_sensitive false ;; -let theory_prev rendering_window () = - match !theory_visited_uris with - [] -> raise NoCurrentUri - | [_] -> raise NoNextOrPrevUri - | uri::(uri'::tl as newvu) -> - theory_visited_uris := newvu ; - theory_to_visit_uris := uri::!theory_to_visit_uris ; - theory_update_output rendering_window uri' ; - rendering_window#nextb#misc#set_sensitive true ; - if tl = [] then - rendering_window#prevb#misc#set_sensitive false -;; - let prev rendering_window () = - match !visited_uris with - [] -> raise NoCurrentUri - | [_] -> raise NoNextOrPrevUri + match !visited_urls with + [] -> raise NoCurrentUrl + | [_] -> raise NoNextOrPrevUrl | uri::(uri'::tl as newvu) -> - visited_uris := newvu ; - to_visit_uris := uri::!to_visit_uris ; + visited_urls := newvu ; + to_visit_urls := uri::!to_visit_urls ; annotated_obj := None ; update_output rendering_window uri' ; rendering_window#nextb#misc#set_sensitive true ; @@ -231,20 +149,30 @@ let prev rendering_window () = (* 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 s = str#get_string in - let uri = UriManager.uri_of_string s in - rendering_window#show () ; - rendering_window#prevb#misc#set_sensitive true ; - rendering_window#nextb#misc#set_sensitive false ; - visited_uris := uri::!visited_uris ; - to_visit_uris := [] ; - annotated_obj := None ; - update_output rendering_window uri + 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 ;; +(*CSC: per ora mai chiamata. Deve essere chiamata quando attivata dal *) +(*CSC: remote-control *) +let remotejump rendering_window url = + rendering_window#prevb#misc#set_sensitive true ; + rendering_window#nextb#misc#set_sensitive false ; + visited_urls := url::!visited_urls ; + to_visit_urls := [] ; + annotated_obj := None ; + update_output rendering_window url +;; + let choose_selection rendering_window (node : Ominidom.o_mDOMNode option) = let module O = Ominidom in let rec aux node = @@ -257,138 +185,36 @@ let choose_selection rendering_window (node : Ominidom.o_mDOMNode option) = | None -> rendering_window#output#set_selection None ;; - -let theory_selection_changed rendering_window uri () = - match uri with - None -> () - | Some uri' -> - if !theory_visited_uris <> [] then - rendering_window#prevb#misc#set_sensitive true ; - rendering_window#nextb#misc#set_sensitive false ; - theory_visited_uris := uri'::!theory_visited_uris ; - theory_to_visit_uris := [] ; - rendering_window#show () ; - theory_update_output rendering_window uri' -;; - -let selection_changed rendering_window uri () = - match uri with - None -> () - | Some uri' -> - if !visited_uris <> [] then - rendering_window#prevb#misc#set_sensitive true ; - rendering_window#nextb#misc#set_sensitive false ; - visited_uris := uri'::!visited_uris ; - to_visit_uris := [] ; - annotated_obj := None ; - rendering_window#show () ; - update_output rendering_window uri' -;; - -let create_gtk_trees (hbox : GPack.box) rendering_window theory_rendering_window mktree = - let sw3 = - GBin.scrolled_window ~width:250 ~height:600 - ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in - let tree1 = - GTree.tree ~selection_mode:`BROWSE ~packing:sw3#add_with_viewport () in - let tree_item1 = GTree.tree_item ~label:"theory:/" ~packing:tree1#append () in - - let sw2 = - GBin.scrolled_window ~width:250 ~height:600 - ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in - let tree = - GTree.tree ~selection_mode:`BROWSE ~packing:sw2#add_with_viewport () in - let tree_item = GTree.tree_item ~label:"cic:/" ~packing:tree#append () in - - ignore(tree_item#connect#select (selection_changed rendering_window None)) ; - mktree selection_changed rendering_window tree_item (Dir ("cic:/",uritree)) ; - - ignore(tree_item1#connect#select - (theory_selection_changed theory_rendering_window None)) ; - mktree theory_selection_changed theory_rendering_window tree_item1 - (Dir ("theory:/",theoryuritree)) ; - (sw3,sw2) -;; - -let updateb_pressed theory_rendering_window rendering_window - (sw1, sw ,(hbox : GPack.box)) mktree () -= - Getter.update () ; - (* let's empty the uri trees and rebuild them *) - uritree := [] ; - theoryuritree := [] ; - build_uri_tree () ; - hbox#remove !sw1#coerce ; - hbox#remove !sw#coerce ; - let (sw3,sw2) = - create_gtk_trees hbox rendering_window theory_rendering_window mktree - in - sw1 := sw3 ; - sw := sw2 -;; - -let theory_check rendering_window () = - let output = - try - TheoryTypeChecker.typecheck (theory_get_current_uri ()); - "Type Checking was successful" - with - TheoryTypeChecker.NotWellTyped s -> - "Type Checking was NOT successful:\n\t" ^ s - in - (* next "cast" can't got rid of, but I don't know why *) - let errors = (rendering_window#errors : GEdit.text) in - let _ = errors#delete_text 0 errors#length in - errors#insert output -;; - -let check rendering_window () = - let output = - try - CicTypeChecker.typecheck (get_current_uri ()); - "Type Checking was successful" - with - CicTypeChecker.NotWellTyped s -> "Type Checking was NOT successful:\n\t" ^ s - in - (* next "cast" can't got rid of, but I don't know why *) - let errors = (rendering_window#errors : GEdit.text) in - let _ = errors#delete_text 0 errors#length in - errors#insert output -;; - 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 () - (* next "cast" can't got rid of, but I don't know why *) - 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 -> - (* next "cast" can't got rid of, but I don't know why *) - let errors = (rendering_window#errors : GEdit.text) in - errors#insert ("\nNo xref found\n") - end - | None -> (rendering_window#errors : GEdit.text)#insert "\nNo selection!\n" + 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 *) @@ -405,44 +231,8 @@ let save_annotation annotation = Xml.pp annxml (Some (fst (Getter.get_ann_file_name_and_uri uri))) ;; -let parse_no_cache uri = - let module U = UriManager in - XsltProcessor.process uri false "cic" -;; - - (* STUFF TO BUILD THE GTK INTERFACE *) -(* Stuff to build the tree window *) - -(* selection_changed is actually selection_changed or theory_selection_changed*) -let mktree selection_changed rendering_window = - let rec aux treeitem = - function - Dir (dirname, content) -> - let subtree = GTree.tree () in - treeitem#set_subtree subtree ; - let expand_sons = - List.map - (fun ti -> - let label = get_name ti - and uri = get_uri ti in - let treeitem2 = GTree.tree_item ~label:label () in - subtree#append treeitem2 ; - ignore(treeitem2#connect#select - (selection_changed rendering_window uri)) ; - (* Almost lazy function *) - (fun () -> aux treeitem2 ti) - ) (List.sort compare !content) - in - let lazy_expand_sons = lazy (List.iter (fun f -> f ()) expand_sons) in - ignore(treeitem#connect#expand - (fun () -> Lazy.force lazy_expand_sons)) ; - | _ -> () - in - aux -;; - (* Stuff for the widget settings *) let export_to_postscript (output : GMathView.math_view) () = @@ -607,11 +397,22 @@ object (self) save_annotation annotation ; GMain.Grab.remove (window_to_annotate#coerce) ; let new_current_uri = - (snd (Getter.get_ann_file_name_and_uri (get_current_uri ()))) + snd (Getter.get_ann_file_name_and_uri (get_current_uri ())) in - visited_uris := new_current_uri::(List.tl !visited_uris) ; +(*CSC: qui c'e' un gran casino: e' l'XsltProcessor che deve ricevere + la richiesta e non il ClientHTTP. Inoltre, prima di inoltrarla, + bisogna comunicare al getter che ora esiste anche il file di annotazioni!!! +*) + (*CSC: DA RIPRISTINARE CON IL RIPRISTINO DELLE ANNOTAZIONI + visited_urls := new_current_uri::(List.tl !visited_urls) ; + *) + let new_current_url = XsltProcessor.url_of_uri new_current_uri in + visited_urls := new_current_url::(List.tl !visited_urls) ; label#set_text (UriManager.string_of_uri new_current_uri) ; - let mmlfile = parse_no_cache new_current_uri in + (*CSC: Perche' non usare update_output? *) + let mmlfile = + ClientHTTP.get_and_save_to_tmp new_current_url + in output#load mmlfile )) ; ignore (abortb#connect#clicked @@ -634,15 +435,10 @@ class rendering_window annotation_window output (label : GMisc.label) = let vbox = GPack.vbox ~packing:window#add () in let _ = vbox#pack ~expand:false ~fill:false ~padding:5 label#coerce in - let paned = - GPack.paned `HORIZONTAL ~packing:(vbox#pack ~expand:true ~padding:5) () in let scrolled_window0 = - GBin.scrolled_window ~border_width:10 ~packing:paned#add1 () in + GBin.scrolled_window ~border_width:10 + ~packing:(vbox#pack ~expand:true ~padding:5) () in let _ = scrolled_window0#add output#coerce in - let scrolled_window = - GBin.scrolled_window - ~border_width:10 ~packing:paned#add2 ~width:240 ~height:100 () in - let errors = GEdit.text ~packing:scrolled_window#add_with_viewport () in let hbox = GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in let prevb = @@ -651,9 +447,6 @@ class rendering_window annotation_window output (label : GMisc.label) = let nextb = GButton.button ~label:"Next" ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in - let checkb = - GButton.button ~label:"Check" - ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in let annotateb = GButton.button ~label:"Annotate" ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in @@ -671,7 +464,6 @@ object(self) method prevb = prevb method label = label method output = (output : GMathView.math_view) - method errors = errors method show () = window#show () initializer nextb#misc#set_sensitive false ; @@ -683,125 +475,70 @@ object(self) ignore(output#connect#selection_changed (choose_selection self)) ; ignore(nextb#connect#clicked (next self)) ; ignore(prevb#connect#clicked (prev self)) ; - (* LUCA: check disabled while compression is not fully implemented *) - (* ignore(checkb#connect#clicked (check self)) ; *) - checkb#misc#set_sensitive false ; - ignore(closeb#connect#clicked window#misc#hide) ; + 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 _ -> window#misc#hide () ; true )) + ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) end;; -class theory_rendering_window rendering_window = - let window = - GWindow.window ~title:"MathML theory viewer" ~border_width:2 () in - let vbox = - GPack.vbox ~packing:window#add () in - let label = - GMisc.label ~text:"???" - ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in - let paned = - GPack.paned `HORIZONTAL ~packing:(vbox#pack ~expand:true ~padding:5) () in - let scrolled_window0 = - GBin.scrolled_window ~border_width:10 ~packing:paned#add1 () in - let output = - GMathView.math_view ~width:400 ~height:380 ~packing:scrolled_window0#add () in - let scrolled_window = - GBin.scrolled_window - ~border_width:10 ~packing:paned#add2 ~width:240 ~height:100 () in - let errors = GEdit.text ~packing:scrolled_window#add_with_viewport () in - let hbox = - GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in - let prevb = - GButton.button ~label:"Prev" - ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in - let nextb = - GButton.button ~label:"Next" - ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in - let checkb = - GButton.button ~label:"Check" - ~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 nextb = nextb - method prevb = prevb - method label = label - method output = (output : GMathView.math_view) - method errors = errors - method show () = window#show () - initializer - nextb#misc#set_sensitive false ; - prevb#misc#set_sensitive false ; - button_export_to_postscript#misc#set_sensitive false ; - - (* signal handlers here *) - ignore(output#connect#jump (jump rendering_window)) ; - ignore(output#connect#selection_changed (choose_selection self)) ; - ignore(nextb#connect#clicked (theory_next self)) ; - ignore(prevb#connect#clicked (theory_prev self)) ; - ignore(checkb#connect#clicked (theory_check self)) ; - let settings_window = new settings_window output scrolled_window0 - button_export_to_postscript (jump rendering_window)(choose_selection self) in - ignore(settingsb#connect#clicked settings_window#show) ; - ignore(button_export_to_postscript#connect#clicked (export_to_postscript output)) ; - ignore(closeb#connect#clicked window#misc#hide) ; - ignore(window#event#connect#delete (fun _ -> window#misc#hide () ; true )) -end;; - -(* CSC: fare in modo che i due alberi vengano svuotati invece che distrutti *) -class selection_window theory_rendering_window rendering_window = - let label = "cic:/" in - let theorylabel = "theory:/" in - let win = GWindow.window ~title:"Known uris" ~border_width:2 () in - let vbox = GPack.vbox ~packing:win#add () in - let hbox1 = GPack.hbox ~packing:(vbox#pack ~padding:5) () in - let (sw1,sw) = - create_gtk_trees hbox1 rendering_window theory_rendering_window mktree - in - let hbox = - GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in - let updateb = - GButton.button ~label:"Update" - ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in - let quitb = - GButton.button ~label:"Quit" - ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in -object (self) - method show () = win#show () - initializer - (* signal handlers here *) - ignore (win#connect#destroy ~callback:GMain.Main.quit) ; - ignore (quitb#connect#clicked GMain.Main.quit) ; - ignore(updateb#connect#clicked (updateb_pressed - theory_rendering_window rendering_window (ref sw1, ref sw, hbox1) mktree)) -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 _ = - (* first of all initialize the processor by requiring the desired stylesheets *) - XsltProcessor.initialize () ; - build_uri_tree () ; - 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 theory_rendering_window = new theory_rendering_window rendering_window in - let selection_window = - new selection_window theory_rendering_window rendering_window - in - selection_window#show () ; - GMain.Main.main () + 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 + visited_urls := x :: !visited_urls + ) usage_msg ; + match !visited_urls with + [url] -> initialize_everything !filename url + | _ -> + prerr_string "Exactly one url expected\n" ; + Arg.usage [] usage_msg ; + exit (-1) ;;