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 sequent = List.hd menv in
+ guistuff.mathviewer#screenshot status sequent menv subst name;
+ [status, parsed_text], "", parsed_text_length
| TA.NCheck (_,t) ->
let status = script#grafite_status in
let ctx = [] in
let parsed_text, _, _, parsed_text_length = text_of_loc loc in
[grafite_status,parsed_text],"",
parsed_text_length
+ | GrafiteParser.LSome (GrafiteAst.Executable (loc, ex)) ->
+ 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
+ | GrafiteParser.LSome (GrafiteAst.Comment (loc, GrafiteAst.Code (_, ex)))
+ (*when Helm_registry.get_bool "matita.literate" *) ->
+ 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
| GrafiteParser.LSome (GrafiteAst.Comment (loc, _)) ->
let parsed_text, _, _, parsed_text_length = text_of_loc loc in
let remain_len = String.length unparsed_text - parsed_text_length in
| (statuses,text)::tl ->
(statuses,parsed_text ^ text)::tl,"",parsed_text_length + len
| [] -> [], "", 0)
- | GrafiteParser.LSome (GrafiteAst.Executable (loc, ex)) ->
- 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
let fresh_script_id =
let i = ref 0 in