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

diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml
index 429bb6b2c..f68421e0c 100644
--- a/helm/software/matita/matitaGui.ml
+++ b/helm/software/matita/matitaGui.ml
@@ -327,11 +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,(fun _ _ _ -> Cic.Implicit None))
-                     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
@@ -801,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");
       
@@ -1486,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 =
@@ -1570,10 +1575,10 @@ let interactive_interp_choice () text prefix_len choices =
 
 let _ =
   (* disambiguator callbacks *)
-  MultiPassDisambiguator.set_choose_uris_callback
+  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 ());
-  MultiPassDisambiguator.set_choose_interp_callback (interactive_interp_choice ());
+  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;