prerr_endline script;
stupid_indenter script
;;
+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 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 _,_,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 menv subst (parsed_text,parsed_text_length,
+ CicNotationPt.Cast (t,CicNotationPt.Implicit `JustOne))
+ (* XXX use the metasenv, if possible *)
+ in
+ guistuff.mathviewer#show_entry (`NCic (t,ctx,m,s));
+ [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
let grafite_status,macro = lazy_macro context in
eval_macro include_paths buffer guistuff grafite_status
user_goal unparsed_text (skipped_txt ^ nonskipped_txt) script macro
+ | GrafiteEngine.NMacro (_loc,macro) ->
+ eval_nmacro include_paths buffer guistuff grafite_status
+ user_goal unparsed_text (skipped_txt ^ nonskipped_txt) script macro
+
and eval_statement include_paths (buffer : GText.buffer) guistuff
grafite_status user_goal script statement
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.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
| 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
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