X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Finterface%2Fmmlinterface.ml;h=64c068fc3b55da06d7a70dd1ff28806d6f7bc9e9;hb=4ef40e8fb4de63f9699268b389f052007bc87f54;hp=68c4134d188fa5e78706c660ab673dab28bbfe15;hpb=4faf0e37e7019de16dd6862bb34d84f799a2a230;p=helm.git diff --git a/helm/interface/mmlinterface.ml b/helm/interface/mmlinterface.ml index 68c4134d1..64c068fc3 100755 --- a/helm/interface/mmlinterface.ml +++ b/helm/interface/mmlinterface.ml @@ -28,7 +28,7 @@ (* PROJECT HELM *) (* *) (* Claudio Sacerdoti Coen *) -(* 03/04/2001 *) +(* 24/01/2000 *) (* *) (* 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,6 +43,79 @@ (* *) (******************************************************************************) +(* 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 *) @@ -51,110 +124,127 @@ let annotated_obj = ref None;; (* reference to a couple option where *) (* 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 theory_visited_uris = ref [];; +let theory_to_visit_uris = ref [];; +let visited_uris = ref [];; +let to_visit_uris = ref [];; + +(* CALLBACKS *) + +exception NoCurrentUri;; +exception NoNextOrPrevUri;; + +let theory_get_current_uri () = + match !theory_visited_uris with + [] -> raise NoCurrentUri + | uri::_ -> uri ;; let get_current_uri () = - UriManager.uri_of_string (uri_from_url !current_url) + match !visited_uris with + [] -> raise NoCurrentUri + | uri::_ -> uri ;; -(* CALLBACKS *) - let get_annotated_obj () = match !annotated_obj with None -> - let annobj = + let (annobj, ids_to_targets,_) = (CicCache.get_annobj (get_current_uri ())) in - annotated_obj := Some annobj ; - annobj + annotated_obj := Some (annobj, ids_to_targets) ; + (annobj, ids_to_targets) | Some annobj -> annobj ;; -let update_output rendering_window url = - rendering_window#label#set_text (uri_from_url url) ; - rendering_window#output#load url +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 next rendering_window () = + match !to_visit_uris with + [] -> raise NoNextOrPrevUri + | uri::tl -> + to_visit_uris := tl ; + visited_uris := uri::!visited_uris ; + annotated_obj := None ; + update_output rendering_window uri ; + 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 + | uri::(uri'::tl as newvu) -> + visited_uris := newvu ; + to_visit_uris := uri::!to_visit_uris ; + annotated_obj := None ; + update_output rendering_window uri' ; + rendering_window#nextb#misc#set_sensitive true ; + if tl = [] then + rendering_window#prevb#misc#set_sensitive false ;; (* 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) + 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 | 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 = @@ -167,63 +257,192 @@ 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 () - 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") + | 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" ;; (* called when the annotation is confirmed *) let save_annotation annotation = - let module S = Str 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 + Xml.pp annxml (Some (fst (Getter.get_ann_file_name_and_uri uri))) +;; + +let parse_no_cache uri = 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" - ) - ) + 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) () = @@ -387,18 +606,13 @@ object (self) 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 ; + let new_current_uri = + (snd (Getter.get_ann_file_name_and_uri (get_current_uri ()))) + in + visited_uris := new_current_uri::(List.tl !visited_uris) ; label#set_text (UriManager.string_of_uri new_current_uri) ; - output#load new_current_url -*) () + let mmlfile = parse_no_cache new_current_uri in + output#load mmlfile )) ; ignore (abortb#connect#clicked (fun () -> @@ -420,12 +634,26 @@ 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:(vbox#pack ~expand:true ~padding:5) () in + GBin.scrolled_window ~border_width:10 ~packing:paned#add1 () 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 = + 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 annotateb = GButton.button ~label:"Annotate" ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in @@ -439,80 +667,139 @@ class rendering_window annotation_window output (label : GMisc.label) = 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 self)) ; ignore(output#connect#selection_changed (choose_selection self)) ; - ignore(closeb#connect#clicked (fun _ -> GMain.Main.quit ())) ; + 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(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 )) + ignore(window#event#connect#delete (fun _ -> window#misc#hide () ; true )) end;; -(* MAIN *) +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 ; -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) -;; + (* 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 _ = - 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 + 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 () ;;