From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 27 Sep 2019 14:58:30 +0000 (+0200)
Subject: debugging code removed
X-Git-Tag: make_still_working~229^2~1^2
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=37ee4577977f031ae897b615784128911450acfa

debugging code removed
---

diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml
index 5b7352d74..ad34b7a57 100644
--- a/matita/matita/matitaGui.ml
+++ b/matita/matita/matitaGui.ml
@@ -601,15 +601,11 @@ class gui () =
           let saved_use_library= !MultiPassDisambiguator.use_library in
           try
            MultiPassDisambiguator.use_library := !all_disambiguation_passes;
-           prerr_endline "PRIMA";
            f script;
            MultiPassDisambiguator.use_library := saved_use_library;
-           prerr_endline "DOPO";
-           unlock_world () ;
-           prerr_endline "FINE";
+           unlock_world ()
           with
            | MultiPassDisambiguator.DisambiguationError (offset,errorll) ->
-              prerr_endline "EXC1";
               (try
                 interactive_error_interp 
                  ~all_passes:!all_disambiguation_passes source_view#source_buffer
@@ -626,9 +622,7 @@ class gui () =
                        notify_exn source_view exc);
                 | exc -> notify_exn source_view exc);
               MultiPassDisambiguator.use_library := saved_use_library;
-              prerr_endline "DOPO1";
-              unlock_world ();
-              prerr_endline "FINE1"
+              unlock_world ()
            | exc ->
               (try notify_exn source_view exc
                with Sys.Break as e -> notify_exn source_view e);