X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaGui.ml;h=6b1f24743295df187a4d625afa5822e7180b84be;hb=a1f4ef3daaeed7a3121a40afe55f321565669da8;hp=baf5998a5371a8f3f535aa35fc877dbba1093287;hpb=ce00fb7749b1bf3bc2e68e578bf945fdcd302926;p=helm.git

diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml
index baf5998a5..6b1f24743 100644
--- a/helm/software/matita/matitaGui.ml
+++ b/helm/software/matita/matitaGui.ml
@@ -84,17 +84,12 @@ let ask_and_save_moo_if_needed parent fname lexicon_status grafite_status =
      LibraryMisc.obj_file_of_baseuri ~must_exist:false ~baseuri
       ~writable:true in
     let save () =
-      let metadata_fname =
-       LibraryMisc.metadata_file_of_baseuri 
-         ~must_exist:false ~baseuri ~writable:true in
       let lexicon_fname =
        LibraryMisc.lexicon_file_of_baseuri 
          ~must_exist:false ~baseuri ~writable:true
       in
        GrafiteMarshal.save_moo moo_fname
         grafite_status.GrafiteTypes.moo_content_rev;
-       LibraryNoDb.save_metadata metadata_fname
-        lexicon_status.LexiconEngine.metadata;
        LexiconMarshal.save_lexicon lexicon_fname
         lexicon_status.LexiconEngine.lexicon_content_rev
     in
@@ -232,101 +227,62 @@ class interpErrorModel =
     end
 
 
-let rec interactive_error_interp ?(all_passes=false) (source_buffer:GSourceView.source_buffer) notify_exn offset errorll
+let rec interactive_error_interp ?(all_passes=false) (source_buffer:GSourceView.source_buffer) notify_exn offset errorll script_fname
 = 
+  (* hook to save a script for each disambiguation error *)
+  if false then
+   (let text =
+     source_buffer#get_text ~start:source_buffer#start_iter
+      ~stop:source_buffer#end_iter () in
+    let md5 = Digest.to_hex (Digest.string text) in
+    let filename = match script_fname with Some s -> s | None -> "unnamed.ma" in
+    let filename =
+     Filename.chop_extension filename ^ ".error." ^ md5 ^ ".ma"  in
+    let ch = open_out filename in
+     output_string ch text;
+    close_out ch
+   );
+  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 annotated_errorll () =
+    List.rev
+     (snd
+       (List.fold_left (fun (pass,res) item -> pass+1,(pass+1,item)::res) (0,[])
+         errorll)) in
+   if all_passes then annotated_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))
-     ::[]::[]
-   in
-  let choices =
-   let pass = ref 0 in
-   List.flatten
-    (List.map
-      (fun l ->
-        incr pass;
-        List.map
-         (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,_,_,_) =
-    compare p1 p2 in
-   let rec uniq =
-    function
-       [] -> []
-     | h::[] -> [h]
-     | (o1,res1)::(o2,res2)::tl when o1 = o2 ->
-        let merge_by_name errors =
-         let merge_by_env errors =
-          let choices_compare_by_env (_,e1,_) (_,e2,_) = compare e1 e2 in
-          let choices_compare_by_passes (p1,_,_) (p2,_,_) =
-           compare p1 p2 in
-          let rec uniq_by_env =
-           function
-              [] -> []
-            | h::[] -> [h]
-            | (p1,e1,_)::(p2,e2,d2)::tl when e1 = e2 ->
-                uniq_by_env ((p1@p2,e2,d2) :: tl) 
-            | h1::tl -> h1 :: uniq_by_env tl
-          in
-           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,_) =
-          compare (Lazy.force m1) (Lazy.force m2) in
-         let rec uniq_by_msg =
-          function
-             [] -> []
-           | h::[] -> [h]
-           | (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
-           (uniq_by_msg (List.stable_sort choices_compare_by_msg errors))
-        in
-         let res = merge_by_name (res1@res2) in
-          uniq ((o1,res) :: tl)
-     | h1::tl -> h1 :: uniq tl
-   in
-   (* 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))
+     let res =
+      (1,[])::(2,[])
+      ::(3,remove_non_significant (safe_list_nth errorll 2))
+      ::(4,remove_non_significant (safe_list_nth errorll 3))
+      ::(5,[])::(6,[])::[]
      in
-      filter choices
+      if List.flatten (List.map snd res) <> [] then res
+      else
+       (* all errors (if any) are not significant: we keep them *)
+       let res =
+        (1,[])::(2,[])
+        ::(3,(safe_list_nth errorll 2))
+        ::(4,(safe_list_nth errorll 3))
+        ::(5,[])::(6,[])::[]
+       in
+        if List.flatten (List.map snd 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" ;
+          annotated_errorll ()
+         end
    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
+  let choices = MatitaExcPp.compact_disambiguation_errors all_passes errorll' in
    match choices with
       [] -> assert false
     | [loffset,[_,envs_and_diffs,msg,significant]] ->
@@ -410,8 +366,8 @@ let rec interactive_error_interp ?(all_passes=false) (source_buffer:GSourceView.
         );
        connect_button dialog#disambiguationErrorsMoreErrors
         (fun _ -> return () ;
-          interactive_error_interp ~all_passes:true source_buffer notify_exn offset
-           errorll);
+          interactive_error_interp ~all_passes:true source_buffer notify_exn
+           offset errorll script_fname);
        connect_button dialog#disambiguationErrorsCancelButton fail;
        dialog#disambiguationErrors#show ();
        GtkThread.main ()
@@ -754,13 +710,19 @@ 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 script_fname
+               with
+                exc -> notify_exn exc);
               unlock_world ()
            | exc ->
               notify_exn exc;
               unlock_world ()
        in
-        worker_thread := Some (Thread.create thread_main ()) in
+       (*thread_main ();*)
+       worker_thread := Some (Thread.create thread_main ())
+      in
       let kill_worker =
        (* the following lines are from Xavier Leroy: http://alan.petitepomme.net/cwn/2005.11.08.html *)
        let interrupt = ref None in
@@ -835,6 +797,7 @@ class gui () =
                 (fun () -> MatitamakeLib.clean_development_in_bg refresh d)
               in
               ignore(clean ())));
+      (* publish button hidden, use command line 
       connect_button develList#publishButton 
         (locker (fun () -> 
           match get_devel_selected () with
@@ -843,6 +806,8 @@ class gui () =
               let publish = locker (fun () ->
                 MatitamakeLib.publish_development_in_bg refresh d) in
               ignore(publish ())));
+              *)
+      develList#publishButton#misc#hide ();
       connect_button develList#graphButton (fun () -> 
         match get_devel_selected () with
         | None -> ()
@@ -866,6 +831,8 @@ class gui () =
         | None -> true
         | Some path -> 
             let is_prefix_of d1 d2 =
+              let d1 = MatitamakeLib.normalize_path d1 in
+              let d2 = MatitamakeLib.normalize_path d2 in
               let len1 = String.length d1 in
               let len2 = String.length d2 in
               if len2 < len1 then 
@@ -937,59 +904,32 @@ class gui () =
         ignore (adj#connect#changed
                 (fun _ -> adj#set_value (adj#upper -. adj#page_size)));
       console#message (sprintf "\tMatita version %s\n" BuildTimeConf.version);
-        (* toolbar *)
-      let module A = GrafiteAst in
-      let hole = CicNotationPt.UserInput in
-      let loc = HExtlib.dummy_floc in
-      let tac ast _ =
-        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)))
-            ()
-      in
-      let tac_w_term ast _ =
-        if (MatitaScript.current ())#onGoingProof () then
-          let buf = source_buffer in
-          buf#insert ~iter:(buf#get_iter_at_mark (`NAME "locked"))
-            ("\n"
-            ^ GrafiteAstPp.pp_tactic ~term_pp:CicNotationPp.pp_term
-              ~lazy_term_pp:CicNotationPp.pp_term ast)
-      in
-      let tbar = main in
-      connect_button tbar#introsButton (tac (A.Intros (loc, None, [])));
-      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, [])));
-      connect_button tbar#elimTypeButton (tac_w_term
-        (A.ElimType (loc, hole, None, None, [])));
-      connect_button tbar#splitButton (tac (A.Split loc));
-      connect_button tbar#leftButton (tac (A.Left loc));
-      connect_button tbar#rightButton (tac (A.Right loc));
-      connect_button tbar#existsButton (tac (A.Exists loc));
-      connect_button tbar#reflexivityButton (tac (A.Reflexivity loc));
-      connect_button tbar#symmetryButton (tac (A.Symmetry loc));
-      connect_button tbar#transitivityButton
-        (tac_w_term (A.Transitivity (loc, hole)));
-      connect_button tbar#assumptionButton (tac (A.Assumption loc));
-      connect_button tbar#cutButton (tac_w_term (A.Cut (loc, None, hole)));
-      connect_button tbar#autoButton (tac (A.Auto (loc,[])));
-      MatitaGtkMisc.toggle_widget_visibility
-       ~widget:(main#tacticsButtonsHandlebox :> GObj.widget)
-       ~check:main#tacticsBarMenuItem;
+      (* TO BE REMOVED *)
+      main#tacticsButtonsHandlebox#misc#hide ();
+      main#tacticsBarMenuItem#misc#hide ();
+      main#scriptNotebook#remove_page 1;
+      main#scriptNotebook#set_show_tabs false;
+      (* / TO BE REMOVED *)
       let module Hr = Helm_registry in
-      if
-        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);
+      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 :=
@@ -1134,14 +1074,23 @@ class gui () =
       connect_menu_item main#saveMenuItem   saveScript;
       connect_menu_item main#saveAsMenuItem saveAsScript;
       connect_menu_item main#newMenuItem    newScript;
+      connect_menu_item main#showCoercionsGraphMenuItem 
+        (fun _ -> 
+          let c = MatitaMathView.cicBrowser () in
+          c#load (`About `Coercions));
+      connect_menu_item main#showAutoGuiMenuItem 
+        (fun _ -> MatitaAutoGui.auto_dialog Auto.get_auto_status);
          (* script monospace font stuff *)  
       self#updateFontSize ();
         (* debug menu *)
       main#debugMenu#misc#hide ();
-        (* status bar *)
+        (* HBUGS *)
+      main#hintNotebook#misc#hide ();
+      (*
       main#hintLowImage#set_file (image_path "matita-bulb-low.png");
       main#hintMediumImage#set_file (image_path "matita-bulb-medium.png");
       main#hintHighImage#set_file (image_path "matita-bulb-high.png");
+      *)
         (* focus *)
       self#sourceView#misc#grab_focus ();
         (* main win dimension *)
@@ -1373,11 +1322,13 @@ class gui () =
         end
       
     method setStar name b =
-      let l = main#scriptLabel in
+      let w = main#toplevel in
+      let set x = w#set_title x in
+      let name = "Matita - " ^ name in
       if b then
-        l#set_text (name ^  " *")
+        set (name ^  " *")
       else
-        l#set_text (name)
+        set (name)
         
     method private _enableSaveTo file =
       script_fname <- Some file;
@@ -1676,18 +1627,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
@@ -1695,12 +1644,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
@@ -1715,19 +1666,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