Bug fixed: pretty-printing of aliases when the OK button is pressed in the

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

diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml
index 393da7cef0e118b5307fd513482e354ea32aed20..5200a21baf371011478d6e840da52f61d3dd74f2 100644 (file)
--- a/helm/software/matita/matitaGui.ml
+++ b/helm/software/matita/matitaGui.ml
@@ -220,7 +220,7 @@ let rec interactive_error_interp ~all_passes
   assert (List.flatten errorll <> []);
   let errorll' =
    let remove_non_significant =
-     List.filter (fun (_env,_diff,_loc,_msg,significant) -> significant) in
+     List.filter (fun (_env,_diff,_loc_msg,significant) -> significant) in
    let annotated_errorll () =
     List.rev
      (snd
@@ -263,8 +263,8 @@ let rec interactive_error_interp ~all_passes
     | [loffset,[_,envs_and_diffs,msg,significant]] ->
         let _,env,diff = List.hd envs_and_diffs in
          notify_exn
-          (GrafiteDisambiguator.DisambiguationError
-            (offset,[[env,diff,loffset,msg,significant]]));
+          (MultiPassDisambiguator.DisambiguationError
+            (offset,[[env,diff,lazy (loffset,Lazy.force msg),significant]]));
     | _::_ ->
        let dialog = new disambiguationErrors () in
        dialog#check_widgets ();
@@ -298,8 +298,8 @@ let rec interactive_error_interp ~all_passes
              ~start:source_buffer#start_iter
              ~stop:source_buffer#end_iter;
            notify_exn
-            (GrafiteDisambiguator.DisambiguationError
-              (offset,[[env,diff,loffset,msg,significant]]))
+            (MultiPassDisambiguator.DisambiguationError
+              (offset,[[env,diff,lazy(loffset,Lazy.force msg),significant]]))
            ));
        let return _ =
          dialog#disambiguationErrors#destroy ();
@@ -327,10 +327,9 @@ let rec interactive_error_interp ~all_passes
             String.concat "\n"
              ("" ::
                List.map
-                (fun k,value ->
-                  DisambiguatePp.pp_environment
-                   (DisambiguateTypes.Environment.add k value
-                     DisambiguateTypes.Environment.empty))
+                (fun k,desc -> 
+                  let alias = DisambiguatePp.alias_of_domain_and_desc k desc in
+                   LexiconAstPp.pp_alias alias)
                 diff) ^ "\n"
            in
             source_buffer#insert
@@ -433,10 +432,18 @@ class gui () =
       in
       ignore(about_dialog#connect#response (fun _ ->about_dialog#misc#hide ()));
       connect_menu_item main#contentsMenuItem (fun () ->
-        let cmd =
-          sprintf "gnome-help ghelp://%s/C/matita.xml &" BuildTimeConf.help_dir
-        in
-        ignore (Sys.command cmd));
+        if 0 = Sys.command "which gnome-help" then
+          let cmd =
+            sprintf "gnome-help ghelp://%s/C/matita.xml &" BuildTimeConf.help_dir
+          in
+           ignore (Sys.command cmd)
+        else
+          MatitaGtkMisc.report_error ~title:"help system error"
+           ~message:(
+              "The program gnome-help is not installed\n\n"^
+              "To browse the user manal it is necessary to install "^
+              "the gnome help syste (also known as yelp)") 
+           ~parent:main#toplevel ());
       connect_menu_item main#aboutMenuItem about_dialog#present;
         (* findRepl win *)
       let show_find_Repl () = 
@@ -680,7 +687,7 @@ class gui () =
            f ();
            unlock_world ()
           with
-           | GrafiteDisambiguator.DisambiguationError (offset,errorll) ->
+           | MultiPassDisambiguator.DisambiguationError (offset,errorll) ->
               (try
                 interactive_error_interp 
                  ~all_passes:!all_disambiguation_passes source_buffer
@@ -791,8 +798,21 @@ class gui () =
         (fun () -> source_buffer#insert "apply rule (⊥_e (…));\n");
       connect_button main#butRAA
         (fun () -> source_buffer#insert "apply rule (RAA […] (…));\n");
-      connect_button main#butStart
-        (fun () -> source_buffer#insert "apply rule (prove (…));\n");
+      connect_button main#butUseLemma
+        (fun () -> source_buffer#insert "apply rule (lem #premises name …);\n");
+      connect_button main#butDischarge
+        (fun () -> source_buffer#insert "apply rule (discharge […]);\n");
+      
+      connect_button main#butForall_intro
+        (fun () -> source_buffer#insert "apply rule (∀_i {…} (…));\n");
+      connect_button main#butForall_elim
+        (fun () -> source_buffer#insert "apply rule (∀_e {…} (…));\n");
+      connect_button main#butExists_intro
+        (fun () -> source_buffer#insert "apply rule (∃_i {…} (…));\n");
+      connect_button main#butExists_elim
+        (fun () -> source_buffer#insert 
+          "apply rule (∃_e (…) {…} […] (…));\n\t[\n\t|\n\t]\n");
+
     
       (* TO BE REMOVED *)
       main#scriptNotebook#remove_page 1;
@@ -1464,7 +1484,6 @@ let interactive_string_choice
     let txt,_ = MatitaGtkMisc.utf8_parsed_text txt
       (HExtlib.floc_of_loc (prefix_len,MatitaGtkMisc.utf8_string_length txt))
     in
-  prerr_endline ("txt:" ^ txt);
     dialog#uriChoiceLabel#set_label txt;
     List.iter model#easy_append uris;
     let return v =
@@ -1548,8 +1567,10 @@ let interactive_interp_choice () text prefix_len choices =
 
 let _ =
   (* disambiguator callbacks *)
-  GrafiteDisambiguator.set_choose_uris_callback (interactive_uri_choice ());
-  GrafiteDisambiguator.set_choose_interp_callback (interactive_interp_choice ());
+  MultiPassDisambiguator.set_choose_uris_callback
+   (fun ~selection_mode ?ok ?(enable_button_for_non_vars=false) ~title ~msg ->
+     interactive_uri_choice ~selection_mode ?ok_label:ok ~title ~msg ());
+  MultiPassDisambiguator.set_choose_interp_callback (interactive_interp_choice ());
   (* gtk initialization *)
   GtkMain.Rc.add_default_file BuildTimeConf.gtkrc_file; (* loads gtk rc *)
   GMathView.add_configuration_path BuildTimeConf.gtkmathview_conf;