"matita.do_heavy_checks", "true";
"matita.moo", "true";
"matita.extract", "false";
+ "matita.execcomments", "false";
]
let set_registry_values =
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
| _ -> 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";
^ "\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";
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))