let debug = false ;;
let debug_print = if debug then prerr_endline else ignore ;;
-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 :=
- GrafiteEngine.eval_ast
- ~disambiguate_tactic:GrafiteDisambiguate.disambiguate_tactic
- ~disambiguate_command:GrafiteDisambiguate.disambiguate_command
- ?do_heavy_checks ?include_paths ?clean_baseuri !status ast
- done
- with End_of_file -> ()
-
-let eval_from_stream_greedy
- ?do_heavy_checks ?include_paths ?clean_baseuri status str cb
+let eval_ast ~include_paths ?do_heavy_checks ?clean_baseuri status ast =
+ GrafiteEngine.eval_ast
+ ~baseuri_of_script:(GrafiteParserMisc.baseuri_of_script ~include_paths)
+ ~disambiguate_tactic:GrafiteDisambiguate.disambiguate_tactic
+ ~disambiguate_command:GrafiteDisambiguate.disambiguate_command
+ ?do_heavy_checks ?clean_baseuri status ast
+
+let eval_from_stream ?(prompt=false) ?do_heavy_checks ~include_paths
+ ?clean_baseuri status str cb
=
while true do
- print_string "matita> ";
- flush stdout;
+ if prompt then (print_string "matita> "; flush stdout);
let ast = GrafiteParser.parse_statement str in
cb !status ast;
status :=
- GrafiteEngine.eval_ast
- ~disambiguate_tactic:GrafiteDisambiguate.disambiguate_tactic
- ~disambiguate_command:GrafiteDisambiguate.disambiguate_command
- ?do_heavy_checks ?include_paths ?clean_baseuri !status ast
+ eval_ast ~include_paths ?do_heavy_checks ?clean_baseuri !status ast
done
;;
-let eval_string ?do_heavy_checks ?include_paths ?clean_baseuri status str =
+let eval_string ?do_heavy_checks ~include_paths ?clean_baseuri status str =
+ try
eval_from_stream
- ?do_heavy_checks ?include_paths ?clean_baseuri status
+ ?do_heavy_checks ~include_paths ?clean_baseuri status
(Ulexing.from_utf8_string str) (fun _ _ -> ())
-
-let default_options () = no_options
-
-let initial_status =
- lazy {
- aliases = DisambiguateTypes.Environment.empty;
- multi_aliases = DisambiguateTypes.Environment.empty;
- moo_content_rev = [];
- metadata = [];
- proof_status = No_proof;
- options = default_options ();
- objects = [];
- coercions = [];
- notation_ids = [];
- }
+ with End_of_file -> ()