formal topologies

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

diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml
index 393da7cef0e118b5307fd513482e354ea32aed20..0cbf2d89ada81b5287a9bc4bba440315410e8146 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
@@ -264,7 +264,7 @@ let rec interactive_error_interp ~all_passes
         let _,env,diff = List.hd envs_and_diffs in
          notify_exn
           (GrafiteDisambiguator.DisambiguationError
-            (offset,[[env,diff,loffset,msg,significant]]));
+            (offset,[[env,diff,lazy (loffset,Lazy.force msg),significant]]));
     | _::_ ->
        let dialog = new disambiguationErrors () in
        dialog#check_widgets ();
@@ -299,7 +299,7 @@ let rec interactive_error_interp ~all_passes
              ~stop:source_buffer#end_iter;
            notify_exn
             (GrafiteDisambiguator.DisambiguationError
-              (offset,[[env,diff,loffset,msg,significant]]))
+              (offset,[[env,diff,lazy(loffset,Lazy.force msg),significant]]))
            ));
        let return _ =
          dialog#disambiguationErrors#destroy ();
@@ -433,10 +433,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 () = 
@@ -791,8 +799,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 …);\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;