+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.Screenshot (_,name) ->
+ let status = script#grafite_status in
+ let _,_,menv,subst,_ = status#obj in
+ let name = Filename.dirname (script#filename) ^ "/" ^ name in
+ let sequents =
+ let selected = Continuationals.Stack.head_goals status#stack in
+ List.filter (fun x,_ -> List.mem x selected) menv
+ in
+ guistuff.mathviewer#screenshot status sequents menv subst name;
+ [status, parsed_text], "", parsed_text_length
+ | TA.NCheck (_,t) ->
+ let status = script#grafite_status in
+ let _,_,menv,subst,_ = status#obj in
+ let ctx =
+ try let _,(_,ctx,_) = List.hd menv in ctx
+ with Failure "hd" -> []
+ in
+ let m, s, status, t =
+ GrafiteDisambiguate.disambiguate_nterm
+ None status ctx menv subst (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));
+ [status, parsed_text], "", parsed_text_length
+ | TA.NIntroGuess _loc ->
+ let names_ref = ref [] in
+ let s =
+ NTactics.intros_tac ~names_ref [] script#grafite_status
+ in
+ let rex = Pcre.regexp ~flags:[`MULTILINE] "\\A([\\n\\t\\r ]*).*\\Z" in
+ let nl = Pcre.replace ~rex ~templ:"$1" parsed_text in
+ [s, nl ^ "#" ^ String.concat " " !names_ref ^ ";"], "", parsed_text_length
+ | TA.NAutoInteractive (_loc, (None,a)) ->
+ let trace_ref = ref [] in
+ let s =
+ NnAuto.auto_tac
+ ~params:(None,a) ~trace_ref script#grafite_status
+ in
+ let depth =
+ try List.assoc "depth" a
+ with Not_found -> ""
+ in
+ let trace = "/"^(if int_of_string depth > 1 then depth else "")^"/ by " in
+ let thms =
+ match !trace_ref with
+ | [] -> "{}"
+ | thms ->
+ String.concat ", "
+ (HExtlib.filter_map (function
+ | CicNotationPt.NRef r -> Some (NCicPp.r2s true r)
+ | _ -> None)
+ thms)
+ in
+ let rex = Pcre.regexp ~flags:[`MULTILINE] "\\A([\\n\\t\\r ]*).*\\Z" in
+ let nl = Pcre.replace ~rex ~templ:"$1" parsed_text in
+ [s, nl ^ trace ^ thms ^ ";"], "", parsed_text_length
+ | TA.NAutoInteractive (_, (Some _,_)) -> assert false