X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FmatitaScript.ml;h=157906fc8ce3eba402581ccc4c5d54133fcf21f3;hb=b890d1579e24e6f7e1d4c6af9afcb0431584a3e0;hp=6528eab9a9cbcb4d7446087dd7a02cd7aa538a75;hpb=6ab0b3e34eee7c4efa628e2994b461347d1bcebf;p=helm.git

diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml
index 6528eab9a..157906fc8 100644
--- a/matita/matita/matitaScript.ml
+++ b/matita/matita/matitaScript.ml
@@ -271,10 +271,11 @@ let initial_statuses current baseuri =
      Some current ->
       NCicLibrary.time_travel
        ((new GrafiteTypes.status current#baseuri)#set_disambiguate_db current#disambiguate_db);
-      (* CSC: there is a known bug in invalidation; temporary fix here *)
+      (* MATITA 1.0: there is a known bug in invalidation; temporary fix here *)
       NCicEnvironment.invalidate ()
    | None -> ());
  let lexicon_status = empty_lstatus in
+ (* MATITA 1.0: ma serve ancora fare questo back-track sul lexicon_status? *)
  let grafite_status = (new GrafiteTypes.status baseuri)#set_disambiguate_db lexicon_status#disambiguate_db in
   grafite_status
 in
@@ -1036,6 +1037,11 @@ let at_page page =
 let current () =
  at_page ((MatitaMisc.get_gui ())#main#scriptNotebook#current_page)
 
+let destroy page =
+ let s = at_page page in
+  _script := List.filter ((<>) s) !_script
+;;
+
 let iter_scripts f = List.iter f !_script;;
 
 let _ =