let debug = false ;;
let debug_print = if debug then prerr_endline else ignore ;;
-type options = { do_heavy_checks: bool ; include_paths: string list }
+type options = {
+ do_heavy_checks: bool ;
+ include_paths: string list ;
+ clean_baseuri: bool
+}
type statement =
(CicNotationPt.term, GrafiteAst.obj, string) GrafiteAst.statement
let status,obj = disambiguate_obj status obj in
status, GrafiteAst.Obj (loc,obj)
-let try_open_in paths path =
+let try_open_in ~f paths path =
let rec aux = function
- | [] -> open_in path
+ | [] -> f path
| p :: tl ->
try
- open_in (p ^ "/" ^ path)
+ f (p ^ "/" ^ path)
with Sys_error _ -> aux tl
in
try
(GrafiteAstPp.pp_command cmd ^ "\n") :: status.moo_content_rev}
| GrafiteAst.Include (loc, path) ->
let path = MatitaMisc.obj_file_of_script path in
- let stream =
- try
- Stream.of_channel (try_open_in opts.include_paths path)
- with Sys_error _ -> raise (UnableToInclude path)
- in
- let status = ref status in
- !eval_from_stream_ref status stream (fun _ _ -> ());
- !status
+ (try
+ let ic = try_open_in ~f:open_in opts.include_paths path in
+ let stream = Stream.of_channel ic in
+ let status = ref status in
+ !eval_from_stream_ref status stream (fun _ _ -> ());
+ close_in ic;
+ !status
+ with Sys_error _ -> raise (UnableToInclude path))
| GrafiteAst.Set (loc, name, value) ->
let value =
if name = "baseuri" then
else
value
in
+ if not (MatitacleanLib.is_empty value) then
+ begin
+ MatitaLog.warn ("baseuri " ^ value ^ " is not empty");
+ if opts.clean_baseuri then
+ begin
+ MatitaLog.message ("cleaning baseuri " ^ value);
+ MatitacleanLib.clean_baseuris [value]
+ end
+ end;
set_option status name value
| GrafiteAst.Drop loc -> raise Drop
| GrafiteAst.Qed loc ->
begin
let dbd = MatitaDb.instance () in
let similar = MetadataQuery.match_term ~dbd ty in
+ let similar_len = List.length similar in
+ if similar_len> 30 then
+ (MatitaLog.message
+ ("Duplicate check will compare your theorem with " ^
+ string_of_int similar_len ^
+ " theorems, this may take a while."));
let convertible =
List.filter (
fun u ->
let eval_comment status c = status
-let eval_ast ?(do_heavy_checks=false) ?(include_paths=[]) status st =
- let opts =
- {do_heavy_checks = do_heavy_checks ; include_paths = include_paths}
+let eval_ast
+ ?(do_heavy_checks=false) ?(include_paths=[]) ?(clean_baseuri=true) status st
+=
+ let opts = {
+ do_heavy_checks = do_heavy_checks ;
+ include_paths = include_paths;
+ clean_baseuri = clean_baseuri }
in
match st with
| GrafiteAst.Executable (_,ex) -> eval_executable opts status ex
| GrafiteAst.Comment (_,c) -> eval_comment status c
-let eval_from_stream ?do_heavy_checks ?include_paths status str cb =
+let eval_from_stream
+ ?do_heavy_checks ?include_paths ?clean_baseuri status str cb
+=
try
while true do
let ast = GrafiteParser.parse_statement str in
cb !status ast;
- status := eval_ast ?do_heavy_checks ?include_paths !status ast
+ status := eval_ast ?do_heavy_checks ?include_paths ?clean_baseuri !status ast
done
with End_of_file -> ()
(* to avoid a long list of recursive functions *)
let _ = eval_from_stream_ref := eval_from_stream
-let eval_from_stream_greedy ?do_heavy_checks ?include_paths status str cb =
+let eval_from_stream_greedy
+ ?do_heavy_checks ?include_paths ?clean_baseuri status str cb
+=
while true do
print_string "matita> ";
flush stdout;
let ast = GrafiteParser.parse_statement str in
cb !status ast;
- status := eval_ast ?do_heavy_checks ?include_paths !status ast
+ status := eval_ast ?do_heavy_checks ?include_paths ?clean_baseuri !status ast
done
;;
-let eval_string ?do_heavy_checks ?include_paths status str =
+let eval_string ?do_heavy_checks ?include_paths ?clean_baseuri status str =
eval_from_stream
- ?do_heavy_checks ?include_paths status (Stream.of_string str) (fun _ _ ->())
+ ?do_heavy_checks ?include_paths ?clean_baseuri status (Stream.of_string str) (fun _ _ ->())
let default_options () =
(*