X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaGui.ml;h=f68421e0cfe5483c7be23a2f989d42352852c5bc;hb=13d4e55242328a66818327bea40d72a964c5d756;hp=8bc226ed4a4bdbbbf33292d7afaa3a4f75c6f406;hpb=c99a38b6539be1eb667cced1eed2db3fc75e3162;p=helm.git

diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml
index 8bc226ed4..f68421e0c 100644
--- 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,17 @@ 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 =
+                   match k with
+                   | DisambiguateTypes.Id id ->
+                       LexiconAst.Ident_alias (id, desc)
+                   | DisambiguateTypes.Symbol (symb, i)-> 
+                       LexiconAst.Symbol_alias (symb, i, desc)
+                   | DisambiguateTypes.Num i ->
+                       LexiconAst.Number_alias (i, desc)
+                  in
+                   LexiconAstPp.pp_alias alias)
                 diff) ^ "\n"
            in
             source_buffer#insert
@@ -433,10 +440,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 +695,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 +807,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 +1492,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 +1575,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 ());
+  Disambiguate.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 ());
+  Disambiguate.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;