| TA.Screenshot (_,name) ->
let status = script#grafite_status in
let _,_,menv,subst,_ = status#obj in
- let sequent = List.hd menv in
- guistuff.mathviewer#screenshot status sequent menv subst name;
+ 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 ctx = [] 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 (parsed_text,parsed_text_length,
+ None status ctx menv subst (parsed_text,parsed_text_length,
CicNotationPt.Cast (t,CicNotationPt.Implicit `JustOne))
(* XXX use the metasenv, if possible *)
in