(* PROJECT HELM *)
(* *)
(* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
-(* 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 *)
(* *)
(******************************************************************************)
-(* 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 *)
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 ->
| 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 ;
(* 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 =
| 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 *)
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) () =
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
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 =
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
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 ;
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)
;;
projects / helm.git / commitdiff