]> matita.cs.unibo.it Git - helm.git/commitdiff
WARNING: NOT COMPILING COMMIT
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 18 Apr 2001 10:16:08 +0000 (10:16 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 18 Apr 2001 10:16:08 +0000 (10:16 +0000)
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.

helm/interface/mmlinterface.ml

index 037f1b13216d7ae699d37fcb357f2606e94e0797..68c4134d188fa5e78706c660ab673dab28bbfe15 100755 (executable)
@@ -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
 ;;