X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaEngine.ml;h=9778f09007d0e88a8c99dfffb8c2afd87e875a48;hb=3cdf3d1d9e2ee3c12931c2af5c2daf1b0e73a310;hp=f0d8ee46c7820b34feff186135edcd418b9b4fd4;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git

diff --git a/helm/software/matita/matitaEngine.ml b/helm/software/matita/matitaEngine.ml
index f0d8ee46c..9778f0900 100644
--- a/helm/software/matita/matitaEngine.ml
+++ b/helm/software/matita/matitaEngine.ml
@@ -30,7 +30,7 @@ open Printf
 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
@@ -63,15 +63,15 @@ let disambiguate_macro lexicon_status_ref grafite_status macro context =
   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 =
@@ -93,18 +93,21 @@ let eval_ast ?do_heavy_checks ?clean_baseuri lexicon_status
         LexiconEngine.set_proof_aliases lexicon_status [k,value]
        in
         new_lexicon_status,
-         ((new_grafite_status,new_lexicon_status),Some (k,value))::acc
+         ((grafite_status,new_lexicon_status),Some (k,value))::acc
    ) (lexicon_status,[]) new_aliases
  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)
+ ?(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
@@ -115,28 +118,35 @@ let eval_from_stream ~first_statement_only ~include_paths ?(prompt=false)
     in
      (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 ->
           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 _ _ -> ())