check on baseuri

diff --git a/helm/matita/matita.ma.templ b/helm/matita/matita.ma.templ
index 157c010d11ffb7b7183bb12971c6857a1c3f8b2f..4fa107ce00eb641a3849cf1d182e6c15d1d3ad40 100644 (file)
--- 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 b20755d870bb4a87def160f7f57d05e9ee7c12e4..ebcf0538ac75030c6e71e9fffc961d3e5d2ccafd 100644 (file)
--- 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