let debug = false ;;
let debug_print = if debug then prerr_endline else ignore ;;
-let disambiguate_tactic lexicon_status_ref grafite_status goal tac =
+let disambiguate_tactic text prefix_len lexicon_status_ref grafite_status goal tac =
let metasenv,tac =
GrafiteDisambiguate.disambiguate_tactic
lexicon_status_ref
GrafiteTypes.set_metasenv metasenv grafite_status,macro
let eval_ast ?do_heavy_checks ?clean_baseuri lexicon_status
- grafite_status ast
+ grafite_status (text,prefix_len,ast)
=
let lexicon_status_ref = ref lexicon_status in
let new_grafite_status,new_objs =
GrafiteEngine.eval_ast
- ~disambiguate_tactic:(disambiguate_tactic lexicon_status_ref)
+ ~disambiguate_tactic:(disambiguate_tactic text prefix_len lexicon_status_ref)
~disambiguate_command:(disambiguate_command lexicon_status_ref)
~disambiguate_macro:(disambiguate_macro lexicon_status_ref)
- ?do_heavy_checks ?clean_baseuri grafite_status ast in
+ ?do_heavy_checks ?clean_baseuri grafite_status (text,prefix_len,ast) in
let new_lexicon_status =
LexiconSync.add_aliases_for_objs !lexicon_status_ref new_objs in
let new_aliases =
in
((new_grafite_status,new_lexicon_status),None)::intermediate_states
+exception TryingToAdd of string
+
+let out = ref ignore
+
+let set_callback f = out := f
+
let eval_from_stream ~first_statement_only ~include_paths ?(prompt=false)
- ?do_heavy_checks ?clean_baseuri lexicon_status grafite_status str cb
+ ?do_heavy_checks ?clean_baseuri ?(enforce_no_new_aliases=true)
+ ?(watch_statuses=fun _ _ -> ()) lexicon_status grafite_status str cb
=
let rec loop lexicon_status grafite_status statuses =
let loop =
if first_statement_only then
- fun _ _ _ -> raise End_of_file
+ fun _ _ statuses -> statuses
else
loop
in
if prompt then (print_string "matita> "; flush stdout);
- try
- let lexicon_status,ast =
- GrafiteParser.parse_statement ~include_paths str lexicon_status
- in
+ let cont =
+ try
+ Some (GrafiteParser.parse_statement ~include_paths str lexicon_status)
+ with
+ End_of_file -> None
+ in
+ match cont with
+ | None -> statuses
+ | Some (lexicon_status,ast) ->
(match ast with
GrafiteParser.LNone _ ->
+ watch_statuses lexicon_status grafite_status ;
loop lexicon_status grafite_status
(((grafite_status,lexicon_status),None)::statuses)
| GrafiteParser.LSome ast ->
+ !out ast;
cb grafite_status ast;
let new_statuses =
eval_ast ?do_heavy_checks ?clean_baseuri lexicon_status
- grafite_status ast in
+ grafite_status ("",0,ast) in
+ if enforce_no_new_aliases then
+ List.iter
+ (fun (_,alias) ->
+ match alias with
+ None -> ()
+ | Some (k,((v,_) as value)) ->
+ let newtxt =
+ DisambiguatePp.pp_environment
+ (DisambiguateTypes.Environment.add k value
+ DisambiguateTypes.Environment.empty)
+ in
+ raise (TryingToAdd newtxt)) new_statuses;
let grafite_status,lexicon_status =
match new_statuses with
[] -> assert false
| (s,_)::_ -> s
in
+ watch_statuses lexicon_status grafite_status ;
loop lexicon_status grafite_status (new_statuses @ statuses))
- with
- End_of_file -> statuses
in
loop lexicon_status grafite_status []
;;
-
-let eval_string ~first_statement_only ~include_paths ?do_heavy_checks
- ?clean_baseuri lexicon_status status str
-=
- eval_from_stream ~first_statement_only ~include_paths ?do_heavy_checks
- ?clean_baseuri lexicon_status status (Ulexing.from_utf8_string str)
- (fun _ _ -> ())