Added toggle for enabling/disabling the conversion from multibyte unicode

[helm.git] / helm / software / matita / matitaGui.ml

diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml
index e2a5588dc178dc2f6eb00394c5658f2e9013f621..a9faa592e8de974b5ce3192a81eacf22f556ac0c 100644 (file)
--- a/helm/software/matita/matitaGui.ml
+++ b/helm/software/matita/matitaGui.ml
@@ -234,16 +234,40 @@ class interpErrorModel =
 
 let rec interactive_error_interp ?(all_passes=false) (source_buffer:GSourceView.source_buffer) notify_exn offset errorll
 = 
+  assert (List.flatten errorll <> []);
   let errorll' =
    let remove_non_significant =
      List.filter (fun (_env,_diff,_loc,_msg,significant) -> significant) in
    if all_passes then errorll else
      let safe_list_nth l n = try List.nth l n with Failure _ -> [] in
     (* We remove passes 1,2 and 5,6 *)
-     []::[]
-     ::(remove_non_significant (safe_list_nth errorll 2))
-     ::(remove_non_significant (safe_list_nth errorll 3))
-     ::[]::[]
+     let res =
+      []::[]
+      ::(remove_non_significant (safe_list_nth errorll 2))
+      ::(remove_non_significant (safe_list_nth errorll 3))
+      ::[]::[]
+     in
+      if List.flatten res <> [] then res
+      else
+       (* all errors (if any) are not significant: we keep them *)
+       let res =
+        []::[]
+        ::(safe_list_nth errorll 2)
+        ::(safe_list_nth errorll 3)
+        ::[]::[]
+       in
+        if List.flatten res <> [] then
+        begin
+          HLog.warn
+          "All disambiguation errors are not significant. Showing them anyway." ;
+         res
+        end
+       else
+         begin
+          HLog.warn
+          "No errors in phases 2 and 3. Showing all errors in all phases" ;
+          errorll
+         end
    in
   let choices =
    let pass = ref 0 in
@@ -754,7 +778,11 @@ class gui () =
            unlock_world ()
           with
            | GrafiteDisambiguator.DisambiguationError (offset,errorll) ->
-              interactive_error_interp source_buffer notify_exn offset errorll ;
+              (try
+                interactive_error_interp source_buffer notify_exn offset
+                 errorll
+               with
+                exc -> notify_exn exc);
               unlock_world ()
            | exc ->
               notify_exn exc;
@@ -984,12 +1012,27 @@ class gui () =
         not (Hr.get_opt_default Hr.bool ~default:false "matita.tactics_bar")
       then 
         main#tacticsBarMenuItem#set_active false;
-      MatitaGtkMisc.toggle_callback 
+      MatitaGtkMisc.toggle_callback ~check:main#fullscreenMenuItem
         ~callback:(function 
           | true -> main#toplevel#fullscreen () 
-          | false -> main#toplevel#unfullscreen ())
-        ~check:main#fullscreenMenuItem;
+          | false -> main#toplevel#unfullscreen ());
       main#fullscreenMenuItem#set_active false;
+      MatitaGtkMisc.toggle_callback ~check:main#ppNotationMenuItem
+        ~callback:(function
+          | true ->
+              CicNotation.set_active_notations
+                (List.map fst (CicNotation.get_all_notations ()))
+          | false ->
+              CicNotation.set_active_notations []);
+      MatitaGtkMisc.toggle_callback ~check:main#hideCoercionsMenuItem
+        ~callback:(fun enabled -> Acic2content.hide_coercions := enabled);
+      MatitaGtkMisc.toggle_callback ~check:main#unicodeAsTexMenuItem
+        ~callback:(fun enabled ->
+          Helm_registry.set_bool "matita.paste_unicode_as_tex" enabled);
+      if not (Helm_registry.has "matita.paste_unicode_as_tex") then
+        Helm_registry.set_bool "matita.paste_unicode_as_tex" true;
+      main#unicodeAsTexMenuItem#set_active
+        (Helm_registry.get_bool "matita.paste_unicode_as_tex");
         (* log *)
       HLog.set_log_callback self#console#log_callback;
       GtkSignal.user_handler :=