From 2c977fe8fdfb6930ed73c6ef806ed35423f4ab6c Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 15 Jul 2011 14:40:34 +0000 Subject: [PATCH] New function replace to be used in place of time_travel every time the user switches to a new tab. In this way, every tab is independent and it only sees the objects defined in that tab. This fixes the following bug: in tab A go down; go down in tab B; go up in tab A (at this point also the objects declared in B where removed); do something in B or go up in B (BOOM)) --- matita/components/ng_library/nCicLibrary.ml | 5 +++++ matita/components/ng_library/nCicLibrary.mli | 1 + 2 files changed, 6 insertions(+) diff --git a/matita/components/ng_library/nCicLibrary.ml b/matita/components/ng_library/nCicLibrary.ml index 27fb0baf6..826779401 100644 --- a/matita/components/ng_library/nCicLibrary.ml +++ b/matita/components/ng_library/nCicLibrary.ml @@ -162,6 +162,11 @@ let time_travel0 (sto,ali) = let time_travel status = time_travel0 status#timestamp;; +let replace status = + let sto,ali = status#timestamp in + storage := sto; local_aliases := ali +;; + type obj = string * Obj.t (* includes are transitively closed; dependencies are only immediate *) type dump = diff --git a/matita/components/ng_library/nCicLibrary.mli b/matita/components/ng_library/nCicLibrary.mli index 63589694a..ee1ed3ece 100644 --- a/matita/components/ng_library/nCicLibrary.mli +++ b/matita/components/ng_library/nCicLibrary.mli @@ -35,6 +35,7 @@ val get_obj: #NCic.status -> NUri.uri -> NCic.obj (* changes the current timesta *) val time_travel: #status -> unit +val replace: #status -> unit val init: unit -> unit -- 2.39.2