]> matita.cs.unibo.it Git - helm.git/blobdiff - matitaB/matita/matitadaemon.ml
Matitaweb: first attempt at "Save as".
[helm.git] / matitaB / matita / matitadaemon.ml
index 61b2dc5479a311eddd69c2b7c831fdee11647b3f..a07e7e16039489d962b2b318890d1fb21960e133 100644 (file)
@@ -351,6 +351,8 @@ let logout (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
   cgi#out_channel#commit_work()
 ;;
 
+exception File_already_exists;;
+
 let save (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
   let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
   let env = cgi#environment in
@@ -363,7 +365,12 @@ let save (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
     let locked = cgi#argument_value "locked" in
     let unlocked = cgi#argument_value "unlocked" in
     let filename = libdir uid ^ "/" ^ (cgi # argument_value "file") in
+    let force = bool_of_string (cgi#argument_value "force") in
     prerr_endline ("Matita will save the file for user " ^ uid);
+
+    if ((not force) && (Sys.file_exists filename)) then 
+      raise File_already_exists;
+
     let oc = open_out filename in
     output_string oc (locked ^ unlocked);
     close_out oc;
@@ -382,7 +389,9 @@ let save (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
       ();
     cgi#out_channel#output_string "<response>ok</response>"
   with
-  | Not_found _ -> 
+  | File_already_exists ->
+      cgi#out_channel#output_string "<response>cancelled</response>"
+  | Sys_error _ -> 
     cgi # set_header
       ~status:`Internal_server_error
       ~cache:`No_cache