X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Finterface%2Fmmlinterface.ml;h=68c4134d188fa5e78706c660ab673dab28bbfe15;hb=89262281b6e83bd2321150f81f1a0583645eb0c8;hp=784c9f4b127e47a21089047296af4dc079675dfa;hpb=cba890e4cba5857f3891e0f5cd087743529ff062;p=helm.git diff --git a/helm/interface/mmlinterface.ml b/helm/interface/mmlinterface.ml index 784c9f4b1..68c4134d1 100755 --- a/helm/interface/mmlinterface.ml +++ b/helm/interface/mmlinterface.ml @@ -1,9 +1,34 @@ +(* 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 *) -(* 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 *) @@ -18,83 +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 [] - -(* Brutti, per via del widget che non e' imperativo *) -let loaded_uri = ref "";; -let theory_loaded_uri = 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 *) @@ -103,403 +51,284 @@ 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 theory_visited_uris = ref [];; -let theory_to_visit_uris = ref [];; -let visited_uris = ref [];; -let to_visit_uris = ref [];; - -(* CALLBACKS *) - -exception NoCurrentUri;; -exception NoNextOrPrevUri;; -exception GtkInterfaceInternalError;; - -let theory_get_current_uri () = - match !theory_visited_uris with - [] -> raise NoCurrentUri - | uri::_ -> uri +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 () = - match !visited_uris with - [] -> raise NoCurrentUri - | uri::_ -> uri + UriManager.uri_of_string (uri_from_url !current_url) ;; +(* CALLBACKS *) + let get_annotated_obj () = match !annotated_obj with None -> - let (annobj, ids_to_targets,_) = + let annobj = (CicCache.get_annobj (get_current_uri ())) in - annotated_obj := Some (annobj, ids_to_targets) ; - (annobj, ids_to_targets) + annotated_obj := Some annobj ; + annobj | 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 - theory_loaded_uri := mmlfile ; - !(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 - loaded_uri := mmlfile ; - !(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 +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 = - let module M = Minidom in - let s = - match M.node_get_attribute node (M.mDOMString_of_string "href") with - None -> assert false - | Some s -> M.string_of_mDOMString s +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 - 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 choose_selection rendering_window node = - let module M = Minidom in - let rec aux node = - match M.node_get_attribute node (M.mDOMString_of_string "xref") with - None -> - let parent = - match M.node_get_parent node with - None -> assert false - | Some parent -> parent - in - aux parent - | Some s -> !(rendering_window#output)#set_selection (Some node) - in - match node with - None -> !(rendering_window#output)#set_selection None - | Some node -> aux node -;; - - -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' -;; - -(* CSC: unificare con la creazione la prima volta *) -let rec 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 = - 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 - sw1 := sw3 ; - ignore(tree_item1#connect#select - (theory_selection_changed theory_rendering_window None)) ; - mktree theory_selection_changed theory_rendering_window tree_item1 - (Dir ("theory:/",theoryuritree)) ; - - 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 - sw := sw2 ; - ignore(tree_item#connect#select (selection_changed rendering_window None)) ; - mktree selection_changed rendering_window tree_item (Dir ("cic:/",uritree)) -;; - -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 + match node with + Some x -> aux x + | None -> rendering_window#output#set_selection None ;; let annotateb_pressed rendering_window annotation_window () = - let module M = Minidom in - match !(rendering_window#output)#get_selection with - None -> (rendering_window#errors : GEdit.text)#insert "\nNo selection!\n" - | Some node -> - let xpath = - match M.node_get_attribute node (M.mDOMString_of_string "xref") with - None -> assert false - | Some xpath -> M.string_of_mDOMString xpath - in - try - 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 ; - CicAnnotationHinter.create_hints annotation_window annobj xpath ; - 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 () ; - with - e -> - (* next "cast" can't got rid of, but I don't know why *) - let errors = (rendering_window#errors : GEdit.text) in - errors#insert ("\n" ^ Printexc.to_string e ^ "\n") + 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 = - if !radio_some_status then - !ann := Some (annotation#get_chars 0 annotation#length) - else - !ann := None ; - match !annotated_obj with - None -> raise GtkInterfaceInternalError - | 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 S = Str in let module U = UriManager in - XsltProcessor.process uri false "cic" + 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 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 ; - List.iter - (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)) ; - aux treeitem2 ti - ) (List.sort compare !content) - | _ -> () - in - aux -;; - (* Stuff for the widget settings *) -let export_to_postscript output () = - !output#export_to_postscript "output.ps" ; +let export_to_postscript (output : GMathView.math_view) () = + output#export_to_postscript ~filename:"output.ps" (); ;; -let activate_t1 output sw is_set jump_callback selection_changed_callback - last_uri () +let activate_t1 output button_set_anti_aliasing button_set_kerning + button_export_to_postscript button_t1 () = - is_set := not !is_set ; - sw#remove !output#coerce ; - output := - (GMathView.math_view ~packing:sw#add ~width:400 ~height:380 - ~use_t1_lib:!is_set ()) ; - !output#load !last_uri ; - ignore(!output#connect#jump jump_callback) ; - ignore(!output#connect#selection_changed selection_changed_callback) ; + 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 is_set () = - is_set := not !is_set ; - !output#set_anti_aliasing !is_set +let set_anti_aliasing output button_set_anti_aliasing () = + output#set_anti_aliasing button_set_anti_aliasing#active ;; -let set_kerning output is_set () = - is_set := not !is_set ; - !output#set_kerning !is_set +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 + 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 + output#set_log_verbosity log_verbosity_spinb#value_as_int ;; -class settings_window output sw jump_callback selection_changed_callback - last_uri +class settings_window output sw button_export_to_postscript jump_callback + selection_changed_callback = let settings_window = GWindow.window ~title:"GtkMathView settings" () in - let table = GPack.table ~rows:5 ~columns:5 ~packing:settings_window#add () 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:4 ~top:2) () in - let button_set_anti_aliasing = GButton.toggle_button ~label:"set_anti_aliasing" ~packing:(table#attach ~left:1 ~top:3) () in - let button_set_kerning = - GButton.toggle_button ~label:"set_kerning" - ~packing:(table#attach ~left:3 ~top:3) () in + ~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:2 ~top:2) () in + ~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 *) - let is_set_use_t1_lib = ref false in - ignore(button_t1#connect#clicked - (activate_t1 output sw is_set_use_t1_lib jump_callback - selection_changed_callback last_uri)) ; + 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)) ; - let is_set_anti_aliasing = ref false in - ignore(button_set_anti_aliasing#connect#toggled - (set_anti_aliasing output is_set_anti_aliasing)); - let is_set_kerning = ref false in - ignore(button_set_kerning#connect#toggled - (set_kerning output is_set_kerning)) ; + 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)) + (set_log_verbosity output log_verbosity_spinb)) ; + ignore(closeb#connect#clicked settings_window#misc#hide) end;; (* Main windows *) @@ -543,7 +372,7 @@ object (self) method radio_some = radio_some method radio_none = radio_none method annotation_hints = annotation_hints - method output = (output : GMathView.math_view ref) + method output = (output : GMathView.math_view) method show () = window_to_annotate#show () initializer (* signal handlers here *) @@ -558,14 +387,18 @@ object (self) window_to_annotate#misc#hide () ; 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 ()))) - in - visited_uris := new_current_uri::(List.tl !visited_uris) ; + 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) ; - let mmlfile = parse_no_cache new_current_uri in - loaded_uri := mmlfile ; - !output#load mmlfile + output#load new_current_url +*) () )) ; ignore (abortb#connect#clicked (fun () -> @@ -587,26 +420,12 @@ 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 - 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 + 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 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 @@ -620,155 +439,80 @@ 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 ref) - method errors = errors + method output = (output : GMathView.math_view) 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(nextb#connect#clicked (next self)) ; - ignore(prevb#connect#clicked (prev self)) ; - ignore(checkb#connect#clicked (check self)) ; - ignore(closeb#connect#clicked window#misc#hide) ; + 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 - (jump self) (choose_selection self) loaded_uri 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 )) -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 = - ref (GMathView.math_view ~use_t1_lib:false ~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 ref) - method errors = errors - method show () = window#show () - initializer - nextb#misc#set_sensitive false ; - prevb#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 - (jump rendering_window) (choose_selection self) theory_loaded_uri in + 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(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 = GBin.scrolled_window ~width:250 ~height:600 - ~packing:(hbox1#pack ~padding:5) () in - let tree1 = - GTree.tree ~selection_mode:`BROWSE ~packing:sw1#add_with_viewport () in - let tree_item1 = - GTree.tree_item ~label:theorylabel ~packing:tree1#append () in - let sw = GBin.scrolled_window ~width:250 ~height:600 - ~packing:(hbox1#pack ~padding:5) () in - let tree = - GTree.tree ~selection_mode:`BROWSE ~packing:sw#add_with_viewport () in - let tree_item = - GTree.tree_item ~label:label ~packing:tree#append () 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 - mktree theory_selection_changed theory_rendering_window tree_item1 - (Dir ("theory:/",theoryuritree)); - mktree selection_changed rendering_window tree_item - (Dir ("cic:/",uritree)); - - (* signal handlers here *) - ignore (tree_item1#connect#select - ~callback:(theory_selection_changed theory_rendering_window None)) ; - ignore (tree_item#connect#select - ~callback:(selection_changed rendering_window None)) ; - 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)) + 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 _ = - build_uri_tree () ; - let output = - ref (GMathView.math_view ~use_t1_lib:false ~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 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 ;;