From 8178b146713be49b5d21744d2cc68d3d4af726a3 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 4 Sep 2006 13:31:55 +0000 Subject: [PATCH] matitac now fails if it tries to insert a new alias --- matita/matitaEngine.ml | 18 ++++++++++++++++-- matita/matitaEngine.mli | 1 + 2 files changed, 17 insertions(+), 2 deletions(-) diff --git a/matita/matitaEngine.ml b/matita/matitaEngine.ml index 404809959..9d88777ac 100644 --- a/matita/matitaEngine.ml +++ b/matita/matitaEngine.ml @@ -98,9 +98,11 @@ let eval_ast ?do_heavy_checks ?clean_baseuri lexicon_status in ((new_grafite_status,new_lexicon_status),None)::intermediate_states +exception TryingToAdd of string + 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) + lexicon_status grafite_status str cb = let rec loop lexicon_status grafite_status statuses = let loop = @@ -123,6 +125,18 @@ let eval_from_stream ~first_statement_only ~include_paths ?(prompt=false) let new_statuses = eval_ast ?do_heavy_checks ?clean_baseuri lexicon_status 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 diff --git a/matita/matitaEngine.mli b/matita/matitaEngine.mli index 3fb5c7637..b20aa2bd5 100644 --- a/matita/matitaEngine.mli +++ b/matita/matitaEngine.mli @@ -48,6 +48,7 @@ val eval_from_stream : ?prompt:bool -> ?do_heavy_checks:bool -> ?clean_baseuri:bool -> + ?enforce_no_new_aliases:bool -> (* default true *) LexiconEngine.status -> GrafiteTypes.status -> Ulexing.lexbuf -> -- 2.39.2