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
| [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 ();
~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 ();
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
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 () =
f ();
unlock_world ()
with
- | GrafiteDisambiguator.DisambiguationError (offset,errorll) ->
+ | MultiPassDisambiguator.DisambiguationError (offset,errorll) ->
(try
interactive_error_interp
~all_passes:!all_disambiguation_passes source_buffer
else main#tacticsButtonsHandlebox#misc#hide ())
~check:main#menuitemPalette;
connect_button main#butImpl_intro
- (fun () -> source_buffer#insert "apply rule (⇒_i […] (…)).\n");
+ (fun () -> source_buffer#insert "apply rule (⇒_i […] (…));\n");
connect_button main#butAnd_intro
(fun () -> source_buffer#insert
"apply rule (∧_i (…) (…));\n\t[\n\t|\n\t]\n");
connect_button main#butOr_intro_left
- (fun () -> source_buffer#insert "apply rule (∨_i_l (…)).\n");
+ (fun () -> source_buffer#insert "apply rule (∨_i_l (…));\n");
connect_button main#butOr_intro_right
- (fun () -> source_buffer#insert "apply rule (∨_i_r (…)).\n");
+ (fun () -> source_buffer#insert "apply rule (∨_i_r (…));\n");
connect_button main#butNot_intro
- (fun () -> source_buffer#insert "apply rule (¬_i […] (…)).\n");
+ (fun () -> source_buffer#insert "apply rule (¬_i […] (…));\n");
connect_button main#butTop_intro
- (fun () -> source_buffer#insert "apply rule (⊤_i).\n");
+ (fun () -> source_buffer#insert "apply rule (⊤_i);\n");
connect_button main#butImpl_elim
(fun () -> source_buffer#insert
"apply rule (⇒_e (…) (…));\n\t[\n\t|\n\t]\n");
connect_button main#butAnd_elim_left
- (fun () -> source_buffer#insert "apply rule (∧_e_l (…)).\n");
+ (fun () -> source_buffer#insert "apply rule (∧_e_l (…));\n");
connect_button main#butAnd_elim_right
- (fun () -> source_buffer#insert "apply rule (∧_e_r (…)).\n");
+ (fun () -> source_buffer#insert "apply rule (∧_e_r (…));\n");
connect_button main#butOr_elim
(fun () -> source_buffer#insert
"apply rule (∨_e (…) […] (…) […] (…));\n\t[\n\t|\n\t|\n\t]\n");
(fun () -> source_buffer#insert
"apply rule (¬_e (…) (…));\n\t[\n\t|\n\t]\n");
connect_button main#butBot_elim
- (fun () -> source_buffer#insert "apply rule (⊥_e (…)).\n");
+ (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");
+ (fun () -> source_buffer#insert "apply rule (RAA […] (…));\n");
+ connect_button main#butUseLemma
+ (fun () -> source_buffer#insert "apply rule (lem #premises name …);\n");
connect_button main#butDischarge
- (fun () -> source_buffer#insert "apply rule (discharge […]).\n");
+ (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 *)
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 =
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;