+let eval_nmacro include_paths (buffer : GText.buffer) guistuff grafite_status user_goal unparsed_text parsed_text script mac =
+ let parsed_text_length = String.length parsed_text in
+ match mac with
+ | TA.NCheck (_,t) ->
+ let status = script#grafite_status in
+ let ctx = [] in
+ let m, s, status, t =
+ GrafiteDisambiguate.disambiguate_nterm
+ None status [] [] ctx (parsed_text,parsed_text_length,
+ CicNotationPt.Cast (t,CicNotationPt.Implicit `JustOne))
+ (* XXX use the metasenv, if possible *)
+ in
+ guistuff.mathviewer#show_entry (`NCic (t,ctx,m,s));
+ [], "", parsed_text_length