(* 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
let i = ref 0 in
fun () -> incr i; !i
-class script ~(source_view: GSourceView.source_view)
+class script ~(source_view: GSourceView2.source_view)
~(mathviewer: MatitaTypes.mathViewer)
~set_star
~ask_confirmation
let s = match statement with Some s -> s | None -> self#getFuture in
if self#bos then LibraryClean.clean_baseuris [self#buri_of_current_file];
HLog.debug ("evaluating: " ^ first_line s ^ " ...");
+ let time1 = Unix.gettimeofday () in
let entries, newtext, parsed_len =
try
eval_statement self#include_paths buffer guistuff
self#grafite_status userGoal self (`Raw s)
with End_of_file -> raise Margin
in
+ let time2 = Unix.gettimeofday () in
+ HLog.debug ("... done in " ^ string_of_float (time2 -. time1) ^ "s");
let new_statuses, new_statements =
let statuses, texts = List.split entries in
statuses, texts