1) Matitaweb now disambiguates scripts as it runs them

[helm.git] / matitaB / components / grafite_engine / grafiteEngine.ml

diff --git a/matitaB/components/grafite_engine/grafiteEngine.ml b/matitaB/components/grafite_engine/grafiteEngine.ml
index d2f12dc9dde5640dde9b910928c203140314718e..a0b00150f2fc5a1563a68155f7e0f2bff45ef6f2 100644 (file)
--- a/matitaB/components/grafite_engine/grafiteEngine.ml
+++ b/matitaB/components/grafite_engine/grafiteEngine.ml
@@ -134,13 +134,12 @@ let eval_alias status data=
 let basic_eval_input_notation (l1,l2) status =
   GrafiteParser.extend status l1 
    (fun env loc ->
-     let rec inner_loc default = function
-       | [] -> default
-       | (_,(NotationEnv.NoType,NotationEnv.LocValue l))::_ -> l
-       | _::tl -> inner_loc default tl
+     let rec get_disamb = function
+     | [] -> Stdpp.dummy_loc,None,None
+     | (_,(NotationEnv.NoType,NotationEnv.DisambiguationValue dv))::_ -> dv
+     | _::tl -> get_disamb tl
      in
-     let inner_loc = inner_loc loc env in
-     let l2' = TermContentPres.instantiate_level2 status env inner_loc l2 in
+     let l2' = TermContentPres.instantiate_level2 status env (get_disamb env) l2 in
      prerr_endline ("new l2 ast : " ^ (NotationPp.pp_term status l2'));
      NotationPt.AttributedTerm (`Loc loc,l2')) 
 ;;
@@ -772,8 +771,11 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
         if dir <> Some `RightToLeft then eval_input_notation status (l1,l2)
         else status
       in
+      let status =
        if dir <> Some `LeftToRight then eval_output_notation status (l1,l2)
        else status
+      in prerr_endline ("new grammar:\n" ^ (Print_grammar.ebnf_of_term status));
+      status
   | GrafiteAst.Alias (loc, spec) -> 
      let diff =
       (*CSC: Warning: this code should be factorized with the corresponding