interim version (added smallLexer)

[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..26ba7ffd06e404001dec125120258de453da1ecf 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')) 
 ;;