...

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

diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml
index 8bc226ed4a4bdbbbf33292d7afaa3a4f75c6f406..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 () =