From: Claudio Sacerdoti Coen Date: Mon, 27 Dec 2010 20:58:08 +0000 (+0000) Subject: Some comments (new problems found). X-Git-Tag: make_still_working~2619 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b890d1579e24e6f7e1d4c6af9afcb0431584a3e0;p=helm.git Some comments (new problems found). --- diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml index 0f7789a89..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 diff --git a/matita/matita/matitaScript.mli b/matita/matita/matitaScript.mli index 81ade1c88..0c12679f1 100644 --- a/matita/matita/matitaScript.mli +++ b/matita/matita/matitaScript.mli @@ -101,7 +101,9 @@ object end val script: - urichooser: (GSourceView2.source_view -> NReference.reference list -> NReference.reference list) -> + urichooser: + (GSourceView2.source_view -> NReference.reference list -> + NReference.reference list) -> ask_confirmation: (title:string -> message:string -> [`YES | `NO | `CANCEL]) -> parent:GBin.scrolled_window -> @@ -112,4 +114,5 @@ val script: val destroy: int -> unit val current: unit -> script val at_page: int -> script + val iter_scripts: (script -> unit) -> unit