X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaInit.ml;h=70125f54c222bb5dc3c3d146a8a7cc8aecfee294;hb=3e373f30525987b7b121ed74c8a1292dc71d185c;hp=72792a56d1d58399d5c93b58f5fd08d02bfd2b9c;hpb=ea3883261d74eda2451ab90efc354a9c03b48707;p=helm.git

diff --git a/helm/software/matita/matitaInit.ml b/helm/software/matita/matitaInit.ml
index 72792a56d..70125f54c 100644
--- a/helm/software/matita/matitaInit.ml
+++ b/helm/software/matita/matitaInit.ml
@@ -54,6 +54,7 @@ let registry_defaults = [
   "matita.do_heavy_checks",      "true";
   "matita.moo",                  "true";
   "matita.extract",              "false";
+  "matita.execcomments",         "false";
 ]
 
 let set_registry_values =
@@ -175,7 +176,10 @@ let parse_cmdline init_status =
     let includes = ref [] in
     let default_includes = [ 
       BuildTimeConf.stdlib_dir_devel;
-      BuildTimeConf.stdlib_dir_installed ; ] 
+      BuildTimeConf.stdlib_dir_installed ; 
+      BuildTimeConf.new_stdlib_dir_devel;
+      BuildTimeConf.new_stdlib_dir_installed ; 
+    ] 
     in
     let absolutize s =
       if Pcre.pmatch ~pat:"^/" s then s else Sys.getcwd () ^"/"^s
@@ -193,6 +197,7 @@ let parse_cmdline init_status =
       | _ -> raise (Failure "bad baseuri, use -b 'path::uri'")
     in
     let no_default_includes = ref false in
+    let execcomments = ref false in
     let arg_spec =
       let std_arg_spec = [
         "-b", Arg.String set_baseuri, "<path::uri> forces the baseuri of path";
@@ -220,6 +225,8 @@ let parse_cmdline init_status =
              ^ "\n    WARNING: not for the casual user");
         "-no-default-includes", Arg.Set no_default_includes,
           "Do not include the default searched paths for the include command"; 
+        "-execcomments", Arg.Set execcomments,
+          "Execute the content of (** ... *) comments";
 	"-v", 
           Arg.Unit (fun () -> Helm_registry.set_bool "matita.verbose" true), 
           "Verbose mode";
@@ -243,6 +250,7 @@ let parse_cmdline init_status =
       Helm_registry.set_list Helm_registry.of_string ~key ~value:l
     in
     Arg.parse arg_spec (add_l args) (usage ());
+    Helm_registry.set_bool ~key:"matita.execcomments" ~value:!execcomments;
     let default_includes = if !no_default_includes then [] else default_includes in
     let includes = 
       List.map (fun x -> HExtlib.normalize_path (absolutize x))