| TA.Screenshot (_,name) ->
let status = script#grafite_status in
let _,_,menv,subst,_ = status#obj in
- let sequent = List.hd menv in
let name = Filename.dirname (script#filename) ^ "/" ^ name in
- guistuff.mathviewer#screenshot status sequent menv subst name;
+ 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
(* XXX use the metasenv, if possible *)
in
guistuff.mathviewer#show_entry (`NCic (t,ctx,m,s));
- [], "", parsed_text_length
+ [status, parsed_text], "", parsed_text_length
let rec eval_macro include_paths (buffer : GText.buffer) guistuff grafite_status user_goal unparsed_text parsed_text script mac =
let module MQ = MetadataQuery in
eval_executable include_paths buffer guistuff
grafite_status user_goal unparsed_text skipped nonskipped script ex loc
| GrafiteParser.LSome (GrafiteAst.Comment (loc, GrafiteAst.Code (_, ex)))
- (*when Helm_registry.get_bool "matita.literate" *) ->
+ when Helm_registry.get_bool "matita.execcomments" ->
let _, nonskipped, skipped, parsed_text_length = text_of_loc loc in
eval_executable include_paths buffer guistuff
grafite_status user_goal unparsed_text skipped nonskipped script ex loc