* so that we can ensure the inclusion is performed after the included file
* is compiled (if needed). matitac does not need that, since it compiles files
* in the good order, here files may be compiled on demand. *)
* so that we can ensure the inclusion is performed after the included file
* is compiled (if needed). matitac does not need that, since it compiles files
* in the good order, here files may be compiled on demand. *)
in
let t_and_ty = Cic.Cast (term,ty) in
guistuff.mathviewer#show_entry (`Cic (t_and_ty,metasenv));
in
let t_and_ty = Cic.Cast (term,ty) in
guistuff.mathviewer#show_entry (`Cic (t_and_ty,metasenv));
- [({grafite_status with proof_status = No_proof}), parsed_text ],"",
+ [(grafite_status#set_proof_status No_proof), parsed_text ],"",
let (_,menv,subst,_,_,_), _ =
ProofEngineTypes.apply_tactic
(Auto.auto_tac ~dbd ~params
let (_,menv,subst,_,_,_), _ =
ProofEngineTypes.apply_tactic
(Auto.auto_tac ~dbd ~params
and eval_statement include_paths (buffer : GText.buffer) guistuff
grafite_status user_goal script statement
=
and eval_statement include_paths (buffer : GText.buffer) guistuff
grafite_status user_goal script statement
=
match statement with
| `Raw text ->
if Pcre.pmatch ~rex:only_dust_RE text then raise Margin;
let ast =
wrap_with_make include_paths
(GrafiteParser.parse_statement (Ulexing.from_utf8_string text))
match statement with
| `Raw text ->
if Pcre.pmatch ~rex:only_dust_RE text then raise Margin;
let ast =
wrap_with_make include_paths
(GrafiteParser.parse_statement (Ulexing.from_utf8_string text))
- | `Ast (st, text) -> (GrafiteTypes.get_lexicon grafite_status, st), text
+ | `Ast (st, text) -> (grafite_status, st), text
let text_of_loc floc =
let nonskipped_txt,_ = MatitaGtkMisc.utf8_parsed_text unparsed_text floc in
let start, stop = HExtlib.loc_of_floc floc in
let text_of_loc floc =
let nonskipped_txt,_ = MatitaGtkMisc.utf8_parsed_text unparsed_text floc in
let start, stop = HExtlib.loc_of_floc floc in
buffer#insert ~iter:(buffer#get_iter_at_mark (`MARK locked_mark)) newtext;
(* here we need to set the Goal in case we are going to cursor (or to
bottom) and we will face a macro *)
buffer#insert ~iter:(buffer#get_iter_at_mark (`MARK locked_mark)) newtext;
(* here we need to set the Goal in case we are going to cursor (or to
bottom) and we will face a macro *)
- LexiconSync.time_travel
- ~present:(GrafiteTypes.get_lexicon cur_grafite_status)
- ~past:(GrafiteTypes.get_lexicon grafite_status);
+ LexiconSync.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;
GrafiteSync.time_travel ~present:cur_grafite_status ~past:grafite_status;
statements <- new_statements;
history <- new_history;
(* 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;
(* 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:(GrafiteTypes.get_lexicon self#grafite_status)
- ~past:(GrafiteTypes.get_lexicon grafite_status)
+ LexiconSync.time_travel ~present:self#grafite_status ~past:grafite_status
| No_proof | Proof _ -> false
| Incomplete_proof _ -> true
| Intermediate _ -> assert false
| No_proof | Proof _ -> false
| Incomplete_proof _ -> true
| Intermediate _ -> assert false