From: Claudio Sacerdoti Coen Date: Wed, 18 Apr 2001 10:16:08 +0000 (+0000) Subject: WARNING: NOT COMPILING COMMIT X-Git-Tag: v0_1_2~15 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a3e1fdeba3b71604dc8adaa3c06e4cece00ea1c9;p=helm.git WARNING: NOT COMPILING COMMIT This commit comes from a set of files not in CVS to reingeenere the whole architecture of the Gtk Interface into an AnnotationHelper, a ProofChecker and a GtkControl, all independents. The commit is done just before removing from the AnnotationHelper the browsing and remote-control features. With this version, the whole interface does not even compile any more. --- diff --git a/helm/interface/mmlinterface.ml b/helm/interface/mmlinterface.ml index 037f1b132..68c4134d1 100755 --- a/helm/interface/mmlinterface.ml +++ b/helm/interface/mmlinterface.ml @@ -51,54 +51,68 @@ 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 "";; -let visited_urls = (ref [] : string list ref);; -let to_visit_urls = ref [];; +(* MISC FUNCTIONS *) -exception No_param_dot_CICURI_found_in of string;; -exception Unexpected_URL_format of string;; +let pathname_of_annuri uristring = + Configuration.annotations_dir ^ + Str.replace_first (Str.regexp "^cic:") "" uristring +;; -(*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 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_found_in url) + [] -> raise (No_param_dot_CICURI_or_param_dot_annotations_found_in url) | he::tl -> match Str.split (Str.regexp "=") he with - ["param.CICURI";uri] -> uri + ["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))) -;; - -(* MISC FUNCTIONS *) - -exception NoCurrentUrl;; -exception NoNextOrPrevUrl;; - -let get_current_url () = - match !visited_urls with - [] -> raise NoCurrentUrl - | url::_ -> url + (N.url_query ~encoded:true (N.url_of_string N.ip_url_syntax url))) ; + match !founduri,!foundann with + (Some uri),(Some ann) -> uri ^ ann + | _ , _ -> + raise (No_param_dot_CICURI_or_param_dot_annotations_found_in url) ;; let get_current_uri () = - UriManager.uri_of_string (uri_from_url (get_current_url ())) + UriManager.uri_of_string (uri_from_url !current_url) ;; (* CALLBACKS *) @@ -106,11 +120,11 @@ let get_current_uri () = 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 ;; @@ -119,33 +133,6 @@ let update_output rendering_window url = rendering_window#output#load url ;; -let next rendering_window () = - 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 url ; - rendering_window#prevb#misc#set_sensitive true ; - if tl = [] then - rendering_window#nextb#misc#set_sensitive false -;; - -let prev rendering_window () = - match !visited_urls with - [] -> raise NoCurrentUrl - | [_] -> raise NoNextOrPrevUrl - | uri::(uri'::tl as newvu) -> - 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 ; - 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 @@ -162,14 +149,9 @@ let jump rendering_window (node : Ominidom.o_mDOMNode) = | None -> assert false ;; -(*CSC: per ora mai chiamata. Deve essere chiamata quando attivata dal *) -(*CSC: remote-control *) +(* called by the 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 ; + current_url := url ; update_output rendering_window url ;; @@ -219,16 +201,25 @@ let annotateb_pressed rendering_window annotation_window () = (* 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 -> 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 module S = Str in + let module U = UriManager in + if !radio_some_status then + !ann := Some (annotation#get_chars 0 annotation#length) + else + !ann := None ; + match !annotated_obj with + None -> assert false + | Some (annobj,_) -> + let uri = get_current_uri () in + let annxml = Annotation2Xml.pp_annotation annobj uri in + make_dirs + (pathname_of_annuri (U.buri_of_uri uri)) ; + Xml.pp ~quiet:true annxml + (Some + (pathname_of_annuri (U.string_of_uri (U.annuri_of_uri uri)) ^ + ".xml" + ) + ) ;; (* STUFF TO BUILD THE GTK INTERFACE *) @@ -396,24 +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 -(*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) ; + 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) ; - (*CSC: Perche' non usare update_output? *) - let mmlfile = - ClientHTTP.get_and_save_to_tmp new_current_url - in - output#load mmlfile + output#load new_current_url +*) () )) ; ignore (abortb#connect#clicked (fun () -> @@ -441,12 +426,6 @@ class rendering_window annotation_window output (label : GMisc.label) = 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 annotateb = GButton.button ~label:"Annotate" ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in @@ -460,21 +439,15 @@ 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 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(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 @@ -532,13 +505,14 @@ let _ = 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 - visited_urls := x :: !visited_urls + begin + prerr_string "More than two arguments provided\n" ; + Arg.usage [] usage_msg ; + exit (-1) + end ) usage_msg ; - match !visited_urls with - [url] -> initialize_everything !filename url - | _ -> - prerr_string "Exactly one url expected\n" ; - Arg.usage [] usage_msg ; - exit (-1) + initialize_everything !filename !current_url ;;