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 ac34052c134d5e3da486aa18c29ca8e5fde8c20e..5200a21baf371011478d6e840da52f61d3dd74f2 100644 (file)
--- a/helm/software/matita/matitaGui.ml
+++ b/helm/software/matita/matitaGui.ml
@@ -263,7 +263,7 @@ 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
+          (MultiPassDisambiguator.DisambiguationError
             (offset,[[env,diff,lazy (loffset,Lazy.force msg),significant]]));
     | _::_ ->
        let dialog = new disambiguationErrors () in
@@ -298,7 +298,7 @@ let rec interactive_error_interp ~all_passes
              ~start:source_buffer#start_iter
              ~stop:source_buffer#end_iter;
            notify_exn
-            (GrafiteDisambiguator.DisambiguationError
+            (MultiPassDisambiguator.DisambiguationError
               (offset,[[env,diff,lazy(loffset,Lazy.force msg),significant]]))
            ));
        let return _ =
@@ -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
@@ -792,7 +799,7 @@ class gui () =
       connect_button main#butRAA
         (fun () -> source_buffer#insert "apply rule (RAA […] (…));\n");
       connect_button main#butUseLemma
-        (fun () -> source_buffer#insert "apply rule (lem …);\n");
+        (fun () -> source_buffer#insert "apply rule (lem #premises name …);\n");
       connect_button main#butDischarge
         (fun () -> source_buffer#insert "apply rule (discharge […]);\n");
       
@@ -1477,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 =
@@ -1561,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;