From da85c90e3e68296f687c553769ff24744dd67166 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Thu, 4 Feb 2010 10:32:30 +0000 Subject: [PATCH] Bug fixed: goto_top used to reset the status to the first one and then reset_buffer (re-implemented yesterday) used to do the time travel again. Fixed by getting rid of goto_top. Note: the old implementation was slightly more efficient since the initial notation of Matita was not re-loaded every time you go back to top. In practice, this does not seem to matter. --- helm/software/matita/matitaScript.ml | 21 +++------------------ 1 file changed, 3 insertions(+), 18 deletions(-) diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml index 44ead20ba..3a57745a4 100644 --- a/helm/software/matita/matitaScript.ml +++ b/helm/software/matita/matitaScript.ml @@ -559,13 +559,13 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff grafite_status 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 @@ -978,7 +978,6 @@ object (self) | 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 -> []); @@ -1008,19 +1007,6 @@ object (self) 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 (Some self#grafite_status) self#buri_of_current_file ]; @@ -1054,7 +1040,6 @@ object (self) match pos with | `Top -> dispose_old_locked_mark (); - self#goto_top; self#reset_buffer; self#notify | `Bottom -> -- 2.39.2