From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Thu, 4 Feb 2010 10:32:30 +0000 (+0000)
Subject: Bug fixed: goto_top used to reset the status to the first one and then
X-Git-Tag: make_still_working~3057
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=da85c90e3e68296f687c553769ff24744dd67166;p=helm.git

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.
---

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 ->