X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2FmatitaGui.ml;h=55db1774cde3e4818ae5bf468082b046a95afe8e;hb=cd91767a396b7bbc72e6e3ee90a3b758421f935d;hp=ff00ce27b69d925cc125a1220149cd9614a211a4;hpb=a28dc063c6268fe3dcd384c85c0a1c3a0e61192e;p=helm.git

diff --git a/matita/matitaGui.ml b/matita/matitaGui.ml
index ff00ce27b..55db1774c 100644
--- a/matita/matitaGui.ml
+++ b/matita/matitaGui.ml
@@ -157,7 +157,7 @@ class interpErrorModel =
               (let loc_row = tree_store#append () in
                 begin
                  match lll with
-                    [passes,envs_and_diffs,_] ->
+                    [passes,envs_and_diffs,_,_] ->
                       tree_store#set ~row:loc_row ~column:id_col
                        ("Error location " ^ string_of_int (!idx1+1) ^
                         ", error message " ^ string_of_int (!idx1+1) ^ ".1" ^
@@ -175,7 +175,7 @@ class interpErrorModel =
                 Some loc_row) in
             let idx2 = ref ~-1 in
              List.iter
-              (fun passes,envs_and_diffs,_ ->
+              (fun passes,envs_and_diffs,_,_ ->
                 incr idx2;
                 let msg_row =
                  if List.length lll = 1 then
@@ -234,11 +234,41 @@ 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 *)
-    []::[]::
-     List.tl (List.tl (List.rev (List.tl (List.tl (List.rev errorll))))) in
+     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
    List.flatten
@@ -246,15 +276,15 @@ let rec interactive_error_interp ?(all_passes=false) (source_buffer:GSourceView.
       (fun l ->
         incr pass;
         List.map
-         (fun (env,diff,offset,msg) ->
-           offset, [[!pass], [[!pass], env, diff], msg]) l
+         (fun (env,diff,offset,msg,significant) ->
+           offset, [[!pass], [[!pass], env, diff], msg, significant]) l
       ) errorll') in
   (* Here we are doing a stable sort and list_uniq returns the latter
      "equal" element. I.e. we are showing the error corresponding to the
      most advanced disambiguation pass *)
   let choices =
    let choices_compare (o1,_) (o2,_) = compare o1 o2 in
-   let choices_compare_by_passes (p1,_,_) (p2,_,_) =
+   let choices_compare_by_passes (p1,_,_,_) (p2,_,_,_) =
     compare p1 p2 in
    let rec uniq =
     function
@@ -277,14 +307,15 @@ let rec interactive_error_interp ?(all_passes=false) (source_buffer:GSourceView.
            List.sort choices_compare_by_passes
             (uniq_by_env (List.stable_sort choices_compare_by_env errors))
          in
-         let choices_compare_by_msg (_,_,m1) (_,_,m2) =
+         let choices_compare_by_msg (_,_,m1,_) (_,_,m2,_) =
           compare (Lazy.force m1) (Lazy.force m2) in
          let rec uniq_by_msg =
           function
              [] -> []
            | h::[] -> [h]
-           | (p1,i1,m1)::(p2,i2,m2)::tl when Lazy.force m1 = Lazy.force m2 ->
-               uniq_by_msg ((p1@p2,merge_by_env (i1@i2),m2) :: tl) 
+           | (p1,i1,m1,s1)::(p2,i2,m2,s2)::tl
+             when Lazy.force m1 = Lazy.force m2 && s1 = s2 ->
+               uniq_by_msg ((p1@p2,merge_by_env (i1@i2),m2,s2) :: tl)
            | h1::tl -> h1 :: uniq_by_msg tl
          in
           List.sort choices_compare_by_msg
@@ -294,16 +325,39 @@ let rec interactive_error_interp ?(all_passes=false) (source_buffer:GSourceView.
           uniq ((o1,res) :: tl)
      | h1::tl -> h1 :: uniq tl
    in
-    List.map (fun o,l -> o,List.sort choices_compare_by_passes l)
-     (uniq (List.stable_sort choices_compare choices))
+   (* Errors in phase 3 that are not also in phase 4 are filtered out *)
+   let filter_phase_3 choices =
+    if all_passes then choices
+    else
+     let filter =
+      HExtlib.filter_map
+       (function
+           (loffset,messages) ->
+              let filtered_messages =
+               HExtlib.filter_map
+                (function
+                    [3],_,_,_ -> None
+                  | item -> Some item
+                ) messages
+              in
+               if filtered_messages = [] then
+                None
+               else
+                Some (loffset,filtered_messages))
+     in
+      filter choices
+   in
+    filter_phase_3
+     (List.map (fun o,l -> o,List.sort choices_compare_by_passes l)
+       (uniq (List.stable_sort choices_compare choices)))
   in
    match choices with
       [] -> assert false
-    | [loffset,[_,envs_and_diffs,msg]] ->
+    | [loffset,[_,envs_and_diffs,msg,significant]] ->
         let _,env,diff = List.hd envs_and_diffs in
          notify_exn
           (GrafiteDisambiguator.DisambiguationError
-            (offset,[[env,diff,loffset,msg]]));
+            (offset,[[env,diff,loffset,msg,significant]]));
     | _::_ ->
        let dialog = new disambiguationErrors () in
        dialog#check_widgets ();
@@ -321,10 +375,12 @@ let rec interactive_error_interp ?(all_passes=false) (source_buffer:GSourceView.
            | Some tp -> tp in
           let idx1,idx2,idx3 = model#get_interp_no tree_path in
           let loffset,lll = List.nth choices idx1 in
-          let _,envs_and_diffs,msg =
+          let _,envs_and_diffs,msg,significant =
            match idx2 with
               Some idx2 -> List.nth lll idx2
-            | None -> [],[],lazy "Multiple error messages. Please select one." in
+            | None ->
+                [],[],lazy "Multiple error messages. Please select one.",true
+          in
           let _,env,diff =
            match idx3 with
               Some idx3 -> List.nth envs_and_diffs idx3
@@ -336,7 +392,7 @@ let rec interactive_error_interp ?(all_passes=false) (source_buffer:GSourceView.
              ~stop:source_buffer#end_iter;
            notify_exn
             (GrafiteDisambiguator.DisambiguationError
-              (offset,[[env,diff,loffset,msg]]))
+              (offset,[[env,diff,loffset,msg,significant]]))
            ));
        let return _ =
          dialog#disambiguationErrors#destroy ();
@@ -355,7 +411,7 @@ let rec interactive_error_interp ?(all_passes=false) (source_buffer:GSourceView.
            match idx2,idx3 with
               Some idx2, Some idx3 ->
                let _,lll = List.nth choices idx1 in
-               let _,envs_and_diffs,_ = List.nth lll idx2 in
+               let _,envs_and_diffs,_,_ = List.nth lll idx2 in
                let _,_,diff = List.nth envs_and_diffs idx3 in
                 diff
             | _,_ -> assert false
@@ -722,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;
@@ -913,8 +973,8 @@ class gui () =
         if (MatitaScript.current ())#onGoingProof () then
           (MatitaScript.current ())#advance
             ~statement:("\n"
-              ^ GrafiteAstPp.pp_tactical ~term_pp:CicNotationPp.pp_term
-                ~lazy_term_pp:CicNotationPp.pp_term (A.Tactic (loc, ast)))
+              ^ GrafiteAstPp.pp_tactic ~term_pp:CicNotationPp.pp_term
+                ~lazy_term_pp:CicNotationPp.pp_term ast)
             ()
       in
       let tac_w_term ast _ =
@@ -930,7 +990,8 @@ class gui () =
       connect_button tbar#applyButton (tac_w_term (A.Apply (loc, hole)));
       connect_button tbar#exactButton (tac_w_term (A.Exact (loc, hole)));
       connect_button tbar#elimButton (tac_w_term
-        (A.Elim (loc, hole, None, None, [])));
+        (let pattern = None, [], Some CicNotationPt.UserInput in
+	A.Elim (loc, hole, None, pattern, None, [])));
       connect_button tbar#elimTypeButton (tac_w_term
         (A.ElimType (loc, hole, None, None, [])));
       connect_button tbar#splitButton (tac (A.Split loc));
@@ -952,12 +1013,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 :=
@@ -1644,18 +1720,16 @@ let interactive_string_choice
     | Some uris -> uris)
 
 let interactive_interp_choice () text prefix_len choices =
-(*  List.iter (fun (l,_,_) -> 
-   List.iter (fun l -> let start, stop = HExtlib.loc_of_floc l in
-   Printf.eprintf "(%d,%d)" start stop) l; prerr_endline "")
-   ((List.hd choices)); *)
+(*List.iter (fun l -> prerr_endline "==="; List.iter (fun (_,id,dsc) -> prerr_endline (id ^ " = " ^ dsc)) l) choices;*)
  let filter_choices filter =
   let rec is_compatible filter =
    function
       [] -> true
-    | (_,id,dsc)::tl ->
+    | ([],_,_)::tl -> is_compatible filter tl
+    | (loc::tlloc,id,dsc)::tl ->
        try
-        if List.assoc id filter = dsc then
-         is_compatible filter tl
+        if List.assoc (loc,id) filter = dsc then
+         is_compatible filter ((tlloc,id,dsc)::tl)
         else
          false
        with
@@ -1663,12 +1737,14 @@ let interactive_interp_choice () text prefix_len choices =
   in
    List.filter (fun (_,interp) -> is_compatible filter interp)
  in
- let rec get_choices id =
+ let rec get_choices loc id =
   function
      [] -> []
    | (_,he)::tl ->
-      let _,_,dsc = List.find (fun (_,id',_) -> id = id') he in
-       dsc :: (List.filter (fun dsc' -> dsc <> dsc') (get_choices id tl))
+      let _,_,dsc =
+       List.find (fun (locs,id',_) -> id = id' && List.mem loc locs) he
+      in
+       dsc :: (List.filter (fun dsc' -> dsc <> dsc') (get_choices loc id tl))
  in
  let example_interp =
   match choices with
@@ -1683,19 +1759,22 @@ let interactive_interp_choice () text prefix_len choices =
  let rec classify ids filter partial_interpretations =
   match ids with
      [] -> List.map fst partial_interpretations
-   | (locs,id,_)::tl ->
-      let choices = get_choices id partial_interpretations in
+   | ([],_,_)::tl -> classify tl filter partial_interpretations
+   | (loc::tlloc,id,dsc)::tl ->
+      let choices = get_choices loc id partial_interpretations in
       let chosen_dsc =
        match choices with
-          [dsc] -> dsc
+          [] -> prerr_endline ("NO CHOICES FOR " ^ id); assert false
+        | [dsc] -> dsc
         | _ ->
-          match ask_user id locs choices with
+          match ask_user id [loc] choices with
              [x] -> x
            | _ -> assert false
       in
-      let filter = (id,chosen_dsc)::filter in
-      let compatible_interps = filter_choices filter partial_interpretations in
-       classify tl filter compatible_interps in
+       let filter = ((loc,id),chosen_dsc)::filter in
+       let compatible_interps = filter_choices filter partial_interpretations in
+        classify ((tlloc,id,dsc)::tl) filter compatible_interps
+ in
  let enumerated_choices =
   let idx = ref ~-1 in
   List.map (fun interp -> incr idx; !idx,interp) choices