From 90f5cf2abe808c8343847e1e910918440fb27410 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 15 Jul 2011 14:41:20 +0000
Subject: [PATCH] Use replace when switching tabs (see previous commit).

---
 matita/matita/matitaScript.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml
index 13668a8ae..931fb049a 100644
--- a/matita/matita/matitaScript.ml
+++ b/matita/matita/matitaScript.ml
@@ -256,8 +256,7 @@ let similarsymbols_tag = `NAME similarsymbols_tag_name in
 let initial_statuses current baseuri =
  let status = new MatitaEngine.status baseuri in
  (match current with
-     Some current ->
-      NCicLibrary.time_travel status;
+     Some current -> NCicLibrary.time_travel status;
 (*
       (* MATITA 1.0: there is a known bug in invalidation; temporary fix here *)
       NCicEnvironment.invalidate () *)
@@ -789,6 +788,7 @@ object (self)
     List.iter (fun o -> o status) observers
 
   method activate =
+    NCicLibrary.replace self#status;
     self#notify
 
   method loadFromFile f =
-- 
2.39.2