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