X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2FmatitaGui.ml;h=5b7352d743f9cbaf4ade7b39b3af0cd85fb3cbe7;hp=ad34b7a5773c85aa87ee5bebe025f6e977ce0707;hb=5b5dca0c118dfbe3ba8f0514ef07549544eb7810;hpb=f00a612006ac05f49a42ab507a95d3298bc1457a diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml index ad34b7a57..5b7352d74 100644 --- a/matita/matita/matitaGui.ml +++ b/matita/matita/matitaGui.ml @@ -601,11 +601,15 @@ 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; - unlock_world () + prerr_endline "DOPO"; + unlock_world () ; + prerr_endline "FINE"; with | MultiPassDisambiguator.DisambiguationError (offset,errorll) -> + prerr_endline "EXC1"; (try interactive_error_interp ~all_passes:!all_disambiguation_passes source_view#source_buffer @@ -622,7 +626,9 @@ class gui () = notify_exn source_view exc); | exc -> notify_exn source_view exc); MultiPassDisambiguator.use_library := saved_use_library; - unlock_world () + prerr_endline "DOPO1"; + unlock_world (); + prerr_endline "FINE1" | exc -> (try notify_exn source_view exc with Sys.Break as e -> notify_exn source_view e);