open Printf
-open GrafiteTypes
-
let debug = false ;;
let debug_print = if debug then prerr_endline else ignore ;;
-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 disambiguate_command lexicon_status_ref status cmd =
+ let lexicon_status,metasenv,cmd =
+ GrafiteDisambiguate.disambiguate_command
+ ~baseuri:(
+ try
+ Some (GrafiteTypes.get_string_option status "baseuri")
+ with
+ GrafiteTypes.Option_error _ -> None)
+ !lexicon_status_ref (GrafiteTypes.get_proof_metasenv status) cmd
+ in
+ lexicon_status_ref := lexicon_status;
+ GrafiteTypes.set_metasenv metasenv status,cmd
+
+let disambiguate_tactic lexicon_status_ref status goal tac =
+ let metasenv,tac =
+ GrafiteDisambiguate.disambiguate_tactic
+ lexicon_status_ref
+ (GrafiteTypes.get_proof_context status goal)
+ (GrafiteTypes.get_proof_metasenv status)
+ tac
+ in
+ GrafiteTypes.set_metasenv metasenv status,tac
-let eval_from_stream ?(prompt=false) ?do_heavy_checks ~include_paths
- ?clean_baseuri status str cb
+let eval_ast ?do_heavy_checks ?clean_baseuri lexicon_status
+ status ast
=
- while true do
- if prompt then (print_string "matita> "; flush stdout);
- let ast = GrafiteParser.parse_statement str in
- cb !status ast;
- status :=
- eval_ast ~include_paths ?do_heavy_checks ?clean_baseuri !status ast
- done
-;;
+ let lexicon_status_ref = ref lexicon_status in
+ let status,new_objs =
+ GrafiteEngine.eval_ast
+ ~disambiguate_tactic:(disambiguate_tactic lexicon_status_ref)
+ ~disambiguate_command:(disambiguate_command lexicon_status_ref)
+ ?do_heavy_checks ?clean_baseuri status ast
+ in
+ let lexicon_status =
+ LexiconSync.add_aliases_for_objs !lexicon_status_ref new_objs
+ in
+ lexicon_status,status
-let eval_string ?do_heavy_checks ~include_paths ?clean_baseuri status str =
- try
- eval_from_stream
- ?do_heavy_checks ~include_paths ?clean_baseuri status
- (Ulexing.from_utf8_string str) (fun _ _ -> ())
- with End_of_file -> ()
+let eval_from_stream ~include_paths ?(prompt=false) ?do_heavy_checks
+ ?clean_baseuri lexicon_status status str cb
+=
+ let rec loop lexicon_status status =
+ if prompt then (print_string "matita> "; flush stdout);
+ try
+ let lexicon_status,ast = GrafiteParser.parse_statement ~include_paths str lexicon_status in
+ (match ast with
+ GrafiteParser.LNone _ -> loop lexicon_status status
+ | GrafiteParser.LSome ast ->
+ cb status ast;
+ let lexicon_status,status =
+ eval_ast ?do_heavy_checks ?clean_baseuri lexicon_status status ast
+ in
+ loop lexicon_status status)
+ with
+ End_of_file -> lexicon_status,status
+in
+ loop lexicon_status status
+;;
+let eval_string ~include_paths ?do_heavy_checks ?clean_baseuri lexicon_status
+ status str
+=
+ eval_from_stream ~include_paths ?do_heavy_checks ?clean_baseuri lexicon_status
+ status (Ulexing.from_utf8_string str) (fun _ _ -> ())