From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 4 Sep 2006 13:31:55 +0000 (+0000)
Subject: matitac now fails if it tries to insert a new alias
X-Git-Tag: 0.4.95@7852~1088
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8178b146713be49b5d21744d2cc68d3d4af726a3;p=helm.git

matitac now fails if it tries to insert a new alias
---

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 ->