From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 6 Jul 2005 15:03:41 +0000 (+0000)
Subject: check on baseuri
X-Git-Tag: V_0_7_1~55
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e8a1f51b3fa848bf04fc13b5a33666e1856aab71;p=helm.git

check on baseuri
---

diff --git a/helm/matita/matita.ma.templ b/helm/matita/matita.ma.templ
index 157c010d1..4fa107ce0 100644
--- a/helm/matita/matita.ma.templ
+++ b/helm/matita/matita.ma.templ
@@ -12,5 +12,5 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/<fill here>".
+set "baseuri" "cic:/matita/#fill here#".
 
diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index b20755d87..ebcf0538a 100644
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -459,7 +459,11 @@ let eval_command status cmd =
   | TacticAst.Set (loc, name, value) -> 
       let value = 
         if name = "baseuri" then
-          MatitaMisc.strip_trailing_slash value
+          let v = MatitaMisc.strip_trailing_slash value in
+          try
+            ignore (String.index v ' ');
+            command_error "baseuri can't contain spaces"
+          with Not_found -> v
         else
           value
       in