From 4c2a5e7da43e15d9a5f35d65f6bd6eda9a117d93 Mon Sep 17 00:00:00 2001
From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Mon, 9 Jan 2006 13:52:05 +0000
Subject: [PATCH] avoid writing in read only baseuris

---
 helm/ocaml/grafite_engine/grafiteEngine.ml | 15 +++++++++------
 helm/ocaml/grafite_engine/grafiteTypes.mli |  4 ++++
 2 files changed, 13 insertions(+), 6 deletions(-)

diff --git a/helm/ocaml/grafite_engine/grafiteEngine.ml b/helm/ocaml/grafite_engine/grafiteEngine.ml
index 26d7712d3..c0a453c93 100644
--- a/helm/ocaml/grafite_engine/grafiteEngine.ml
+++ b/helm/ocaml/grafite_engine/grafiteEngine.ml
@@ -25,11 +25,14 @@
 
 (* $Id$ *)
 
+open Printf
+
 exception Drop
 exception IncludedFileNotCompiled of string (* file name *)
 exception Macro of
  GrafiteAst.loc *
   (Cic.context -> GrafiteTypes.status * Cic.term GrafiteAst.macro)
+exception ReadOnlyUri of string
 
 type options = { 
   do_heavy_checks: bool ; 
@@ -544,7 +547,6 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status cmd ->
      GrafiteTypes.add_moo_content [cmd] status,[]
   | GrafiteAst.Include (loc, baseuri) ->
      let moopath = LibraryMisc.obj_file_of_baseuri ~basedir ~baseuri in
-     let metadatapath= LibraryMisc.metadata_file_of_baseuri ~basedir ~baseuri in
      if not (Sys.file_exists moopath) then
        raise (IncludedFileNotCompiled moopath);
      let status = eval_from_moo.efm_go status moopath in
@@ -555,11 +557,15 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status cmd ->
           let v = Http_getter_misc.strip_trailing_slash value in
           try
             ignore (String.index v ' ');
-            raise (GrafiteTypes.Command_error "baseuri can't contain spaces")
+            GrafiteTypes.command_error "baseuri can't contain spaces"
           with Not_found -> v
         in
+        if Http_getter_storage.is_read_only value then begin
+          HLog.error (sprintf "uri %s belongs to a read-only repository" value);
+          raise (ReadOnlyUri value)
+        end;
         if not (GrafiteMisc.is_empty value) && opts.clean_baseuri then begin
-          HLog.warn ("baseuri " ^ value ^ " is not empty");
+          HLog.message ("baseuri " ^ value ^ " is not empty");
           HLog.message ("cleaning baseuri " ^ value);
           LibraryClean.clean_baseuris ~basedir [value];
         end;
@@ -637,9 +643,6 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status cmd ->
                   "\nPlease use a variant."));
            end;
          assert (metasenv = metasenv');
-         let goalno =
-           match metasenv' with (goalno,_,_)::_ -> goalno | _ -> assert false 
-         in
          let initial_proof = (Some uri, metasenv, bo, ty) in
          let initial_stack = Continuationals.Stack.of_metasenv metasenv in
          { status with GrafiteTypes.proof_status =
diff --git a/helm/ocaml/grafite_engine/grafiteTypes.mli b/helm/ocaml/grafite_engine/grafiteTypes.mli
index 70089623b..a8b86c276 100644
--- a/helm/ocaml/grafite_engine/grafiteTypes.mli
+++ b/helm/ocaml/grafite_engine/grafiteTypes.mli
@@ -23,10 +23,14 @@
  * http://helm.cs.unibo.it/
  *)
 
+(* $Id$ *)
+
 exception Option_error of string * string
 exception Statement_error of string
 exception Command_error of string
 
+val command_error: string -> 'a   (** @raise Command_error *)
+
 type incomplete_proof = {
   proof: ProofEngineTypes.proof;
   stack: Continuationals.Stack.t;
-- 
2.39.2