X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2FmatitaScript.ml;h=891d09a50b20495e9c5da8f3c70d6f0d70792f68;hb=e57e808481a6f0a9bd6bd66d6afbfb484ebad2e5;hp=b8c9505497305dcc0f407d2ae8f448d0c29120e6;hpb=9393a9f9370014c904244358abe4ec6e11a9d158;p=helm.git

diff --git a/matita/matitaScript.ml b/matita/matitaScript.ml
index b8c950549..891d09a50 100644
--- a/matita/matitaScript.ml
+++ b/matita/matitaScript.ml
@@ -36,7 +36,7 @@ let debug_print = if debug then prerr_endline else ignore
   (** raised when one of the script margins (top or bottom) is reached *)
 exception Margin
 exception NoUnfinishedProof
-exception ActionCancelled
+exception ActionCancelled of string
 
 let safe_substring s i j =
   try String.sub s i j with Invalid_argument _ -> assert false
@@ -161,7 +161,7 @@ let wrap_with_developments guistuff f arg =
         else
           f arg
       in
-      let do_nothing () = raise ActionCancelled in
+      let do_nothing () = raise (ActionCancelled "Inclusion not performed") in
       let handle_with_devel d =
         let name = MatitamakeLib.name_for_development d in
         let title = "Unable to include " ^ what in
@@ -324,7 +324,9 @@ and eval_executable include_paths (buffer : GText.buffer) guistuff lexicon_statu
    begin
     match ex with
      | TA.Command (_,TA.Set (_,"baseuri",u)) ->
-        if not (GrafiteMisc.is_empty u) then
+        if  Http_getter_storage.is_read_only u then
+          raise (ActionCancelled ("baseuri " ^ u ^ " is readonly"));
+        if not (Http_getter_storage.is_empty u) then
          (match 
             guistuff.ask_confirmation 
               ~title:"Baseuri redefinition" 
@@ -333,9 +335,7 @@ and eval_executable include_paths (buffer : GText.buffer) guistuff lexicon_statu
                 "Do you want to redefine the corresponding "^
                 "part of the library?")
           with
-           | `YES ->
-               let basedir = Helm_registry.get "matita.basedir" in
-                LibraryClean.clean_baseuris ~basedir [u]
+           | `YES -> LibraryClean.clean_baseuris [u]
            | `NO -> ()
            | `CANCEL -> raise MatitaTypes.Cancel)
      | _ -> ()
@@ -803,6 +803,7 @@ object (self)
     try
       is_there_only_comments self#lexicon_status s
     with 
+    | HExtlib.Localized _
     | CicNotationParser.Parse_error _ -> false
     | Margin | End_of_file -> true