From 37ee4577977f031ae897b615784128911450acfa Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 27 Sep 2019 16:58:30 +0200 Subject: [PATCH] debugging code removed --- matita/matita/matitaGui.ml | 10 ++-------- 1 file changed, 2 insertions(+), 8 deletions(-) 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); -- 2.39.2