raise exn
let fname () =
- match Helm_registry.get_list Helm_registry.string "matita.args" with
+ let rec aux = function
+ | ""::tl -> aux tl
| [x] -> x
+ | [] -> MatitaInit.die_usage ()
| l ->
- prerr_endline ("Wrong commands: " ^ String.concat " " l);
+ prerr_endline
+ ("Wrong commands: " ^
+ String.concat " " (List.map (fun x -> "'" ^ x ^ "'") l));
MatitaInit.die_usage ()
+ in
+ aux (Helm_registry.get_list Helm_registry.string "matita.args")
let pp_ocaml_mode () =
HLog.message "";
else
"matitac"
in
- let rc = if rc then "OK" else "FAIL" in
+ let rc = if rc then "\e[0;32mOK\e[0m" else "\e[0;31mFAIL\e[0m" in
let times =
let fmt t =
let seconds = int_of_float t in
assert (fnamelen > rootlen);
String.sub fname rootlen (fnamelen - rootlen)
in
- let s =
- Printf.sprintf "%s %-35s %-4s %s %s" cc fname rc times extra
+ let fname =
+ if fname.[0] = '/' then
+ String.sub fname 1 (String.length fname - 1)
+ else
+ fname
in
+ let s = Printf.sprintf "%s %-35s %-4s %s %s" cc fname rc times extra in
print_endline s;
flush stdout
end
let baseuri =
DependenciesParser.baseuri_of_script ~include_paths fname in
let moo_fname =
- LibraryMisc.obj_file_of_baseuri ~baseuri ~writable:true
+ LibraryMisc.obj_file_of_baseuri
+ ~must_exist:false ~baseuri ~writable:true
in
let lexicon_fname=
- LibraryMisc.lexicon_file_of_baseuri ~baseuri ~writable:true
+ LibraryMisc.lexicon_file_of_baseuri
+ ~must_exist:false ~baseuri ~writable:true
in
let metadata_fname =
- LibraryMisc.metadata_file_of_baseuri ~baseuri ~writable:true
+ LibraryMisc.metadata_file_of_baseuri
+ ~must_exist:false ~baseuri ~writable:true
in
GrafiteMarshal.save_moo moo_fname moo_content_rev;
LibraryNoDb.save_metadata metadata_fname metadata;