let status = script#grafite_status in
let _,_,menv,subst,_ = status#obj in
let name = Filename.dirname (script#filename) ^ "/" ^ name in
- guistuff.mathviewer#screenshot status menv 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
+ | TA.NIntroGuess _loc ->
+ let names_ref = ref [] in
+ let s =
+ NTactics.intros_tac ~names_ref [] script#grafite_status
+ in
+ let rex = Pcre.regexp ~flags:[`MULTILINE] "\\A([\\n\\t\\r ]*).*\\Z" in
+ let nl = Pcre.replace ~rex ~templ:"$1" parsed_text in
+ [s, nl ^ "#" ^ String.concat " " !names_ref ^ ";"], "", parsed_text_length
+ | TA.NAutoInteractive (_loc, (None,a)) ->
+ let trace_ref = ref [] in
+ let s =
+ NnAuto.auto_tac
+ ~params:(None,a) ~trace_ref script#grafite_status
+ in
+ let depth =
+ try List.assoc "depth" a
+ with Not_found -> ""
+ in
+ let trace = "/"^(if int_of_string depth > 1 then depth else "")^"/ by " in
+ let thms =
+ match !trace_ref with
+ | [] -> "{}"
+ | thms ->
+ String.concat ", "
+ (HExtlib.filter_map (function
+ | CicNotationPt.NRef r -> Some (NCicPp.r2s true r)
+ | _ -> None)
+ thms)
+ in
+ let rex = Pcre.regexp ~flags:[`MULTILINE] "\\A([\\n\\t\\r ]*).*\\Z" in
+ let nl = Pcre.replace ~rex ~templ:"$1" parsed_text in
+ [s, nl ^ trace ^ thms ^ ";"], "", parsed_text_length
+ | TA.NAutoInteractive (_, (Some _,_)) -> assert false
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
(* no idea why ocaml wants this *)
let parsed_text_length = String.length parsed_text in
let dbd = LibraryDb.instance () in
- let pp_macro = ApplyTransformation.txt_of_macro ~map_unicode_to_tex:true in
+ let pp_macro = ApplyTransformation.txt_of_macro ~map_unicode_to_tex:false in
match mac with
(* WHELP's stuff *)
| TA.WMatch (loc, term) ->
in
let ty,_ =
CicTypeChecker.type_of_aux'
- menv [] proof_term CicUniv.empty_ugraph
+ [] [] proof_term CicUniv.empty_ugraph
in
- prerr_endline (CicPp.ppterm proof_term);
+ prerr_endline (CicPp.ppterm proof_term ^ " n lambda= " ^ string_of_int how_many_lambdas);
(* use declarative output *)
let obj =
(* il proof_term vive in cc, devo metterci i lambda no? *)
- (Cic.CurrentProof ("xxx",menv,proof_term,ty,[],[]))
+ (Cic.CurrentProof ("xxx",[],proof_term,ty,[],[]))
in
ApplyTransformation.txt_of_cic_object
~map_unicode_to_tex:(Helm_registry.get_bool
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 buffer = source_view#buffer in
let source_buffer = source_view#source_buffer in
-let initial_statuses baseuri =
+let initial_statuses current baseuri =
+ let empty_lstatus = new LexiconEngine.status in
+ (match current with
+ Some current ->
+ LexiconSync.time_travel ~present:current ~past:empty_lstatus;
+ GrafiteSync.time_travel ~present:current ();
+ (* CSC: there is a known bug in invalidation; temporary fix here *)
+ NCicEnvironment.invalidate ()
+ | None -> ());
let lexicon_status =
- CicNotation2.load_notation ~include_paths:[] (new LexiconEngine.status)
+ CicNotation2.load_notation ~include_paths:[] empty_lstatus
BuildTimeConf.core_notation_script
in
let grafite_status = GrafiteSync.init lexicon_status baseuri in
val mutable statements = [] (** executed statements *)
- val mutable history = [ initial_statuses default_buri ]
+ val mutable history = [ initial_statuses None default_buri ]
(** list of states before having executed statements. Head element of this
* list is the current state, last element is the state at the beginning of
* the script.
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
match history with s::_ -> s | [] -> assert false
in
LexiconSync.time_travel ~present:cur_grafite_status ~past:grafite_status;
- GrafiteSync.time_travel ~present:cur_grafite_status ~past:grafite_status;
+ GrafiteSync.time_travel ~present:cur_grafite_status ~past:grafite_status ();
statements <- new_statements;
history <- new_history;
self#moveMark (- offset)
| Some f -> Some (Librarian.absolutize f)
| None -> None
in
- self#goto_top;
filename_ <- file;
include_paths_ <-
(match file with Some file -> read_include_paths file | None -> []);
HLog.debug ("backup " ^ f ^ " saved")
end
- method private goto_top =
- let grafite_status =
- let rec last x = function
- | [] -> x
- | hd::tl -> last hd tl
- in
- last (self#grafite_status) history
- in
- (* FIXME: this is not correct since there is no undo for
- * library_objects.set_default... *)
- GrafiteSync.time_travel ~present:self#grafite_status ~past:grafite_status;
- LexiconSync.time_travel ~present:self#grafite_status ~past:grafite_status
-
method private reset_buffer =
statements <- [];
- history <- [ initial_statuses self#buri_of_current_file ];
+ history <- [ initial_statuses (Some self#grafite_status) self#buri_of_current_file ];
userGoal <- None;
self#notify;
buffer#remove_tag locked_tag ~start:buffer#start_iter ~stop:buffer#end_iter;
match pos with
| `Top ->
dispose_old_locked_mark ();
- self#goto_top;
self#reset_buffer;
self#notify
| `Bottom ->
projects / helm.git / blobdiff