X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaGui.ml;h=f68421e0cfe5483c7be23a2f989d42352852c5bc;hb=13d4e55242328a66818327bea40d72a964c5d756;hp=55b044ba44662b286493d077229d9ced6b82955c;hpb=68f3812e06c04ddd664e86dbfd3a1c32f96a22d1;p=helm.git
diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml
index 55b044ba4..f68421e0c 100644
--- a/helm/software/matita/matitaGui.ml
+++ b/helm/software/matita/matitaGui.ml
@@ -42,7 +42,7 @@ class type browserWin =
* lablgladecc :-(((( *)
object
inherit MatitaGeneratedGui.browserWin
- method browserUri: GEdit.combo_box_entry
+ method browserUri: GEdit.entry
end
class console ~(buffer: GText.buffer) () =
@@ -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
@@ -754,9 +769,60 @@ class gui () =
ignore (adj#connect#changed
(fun _ -> adj#set_value (adj#upper -. adj#page_size)));
console#message (sprintf "\tMatita version %s\n" BuildTimeConf.version);
- (* TO BE REMOVED *)
+ (* natural deduction palette *)
main#tacticsButtonsHandlebox#misc#hide ();
- main#tacticsBarMenuItem#misc#hide ();
+ MatitaGtkMisc.toggle_callback
+ ~callback:(fun b ->
+ if b then main#tacticsButtonsHandlebox#misc#show ()
+ else main#tacticsButtonsHandlebox#misc#hide ())
+ ~check:main#menuitemPalette;
+ connect_button main#butImpl_intro
+ (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");
+ connect_button main#butOr_intro_right
+ (fun () -> source_buffer#insert "apply rule (â¨_i_r (â¦));\n");
+ connect_button main#butNot_intro
+ (fun () -> source_buffer#insert "apply rule (¬_i [â¦] (â¦));\n");
+ connect_button main#butTop_intro
+ (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");
+ connect_button main#butAnd_elim_right
+ (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");
+ connect_button main#butNot_elim
+ (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");
+ connect_button main#butRAA
+ (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");
+
+ 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 *)
main#scriptNotebook#remove_page 1;
main#scriptNotebook#set_show_tabs false;
(* / TO BE REMOVED *)
@@ -843,6 +909,8 @@ class gui () =
source_view#source_buffer#begin_not_undoable_action ();
script#loadFromFile f;
source_view#source_buffer#end_not_undoable_action ();
+ source_view#buffer#move_mark `INSERT source_view#buffer#start_iter;
+ source_view#buffer#place_cursor source_view#buffer#start_iter;
console#message ("'"^f^"' loaded.\n");
self#_enableSaveTo f
| None -> ()
@@ -907,31 +975,12 @@ class gui () =
(fun _ -> MatitaAutoGui.auto_dialog Auto.get_auto_status);
connect_menu_item main#showTermGrammarMenuItem
(fun _ ->
- let w = GWindow.window ~resizable:true
- ~position:`CENTER_ON_PARENT
- ~title:"Terms grammar" ~width:640 ~height:400 () in
- w#set_transient_for (main#toplevel#as_window);
- let s = GBin.scrolled_window () in
- (w :> GContainer.container)#add (s :> GObj.widget);
- let t = GText.view () in
- t#buffer#insert (Print_grammar.ebnf_of_term ());
- s#add (t:>GObj.widget);
- w#show ());
+ let c = MatitaMathView.cicBrowser () in
+ c#load (`About `Grammar));
connect_menu_item main#showUnicodeTable
(fun _ ->
- let w = GWindow.window ~resizable:true
- ~position:`CENTER_ON_PARENT
- ~title:"Tex/UTF8 table" ~width:640 ~height:400 () in
- w#set_transient_for (main#toplevel#as_window);
- let s = GBin.scrolled_window () in
- (w :> GContainer.container)#add (s :> GObj.widget);
- let t = GTree.view () in
- let m = new MatitaGtkMisc.multiStringListModel ~cols:2 t in
- List.iter (fun (k,vs) ->
- m#easy_mappend [k;String.concat " " vs])
- (Utf8Macro.pp_table ());
- s#add (t:>GObj.widget);
- w#show ());
+ let c = MatitaMathView.cicBrowser () in
+ c#load (`About `TeX));
(* script monospace font stuff *)
self#updateFontSize ();
(* debug menu *)
@@ -981,7 +1030,7 @@ class gui () =
end));
(* math view handling *)
connect_menu_item main#newCicBrowserMenuItem (fun () ->
- ignore (MatitaMathView.cicBrowser ()));
+ ignore(MatitaMathView.cicBrowser ()));
connect_menu_item main#increaseFontSizeMenuItem (fun () ->
self#increaseFontSize ();
MatitaMathView.increase_font_size ();
@@ -1153,6 +1202,8 @@ class gui () =
source_view#source_buffer#begin_not_undoable_action ();
script#loadFromFile content;
source_view#source_buffer#end_not_undoable_action ();
+ source_view#buffer#move_mark `INSERT source_view#buffer#start_iter;
+ source_view#buffer#place_cursor source_view#buffer#start_iter;
console#message ("'"^file^"' loaded.");
self#_enableSaveTo file
@@ -1180,12 +1231,12 @@ class gui () =
method newBrowserWin () =
object (self)
inherit browserWin ()
- val combo = GEdit.combo_box_entry ()
+ val combo = GEdit.entry ()
initializer
self#check_widgets ();
let combo_widget = combo#coerce in
uriHBox#pack ~from:`END ~fill:true ~expand:true combo_widget;
- combo#entry#misc#grab_focus ()
+ combo#misc#grab_focus ()
method browserUri = combo
end
@@ -1250,7 +1301,8 @@ class gui () =
method private updateFontSize () =
self#sourceView#misc#modify_font_by_name
- (sprintf "%s %d" BuildTimeConf.script_font font_size)
+ (sprintf "%s %d" BuildTimeConf.script_font font_size);
+ MatitaAutoGui.set_font_size font_size
method increaseFontSize () =
font_size <- font_size + 1;
@@ -1394,9 +1446,10 @@ class interpModel =
tree_store#get ~row:iter ~column:interp_no_col
end
+
let interactive_string_choice
text prefix_len ?(title = "") ?(msg = "") () ~id locs uris
-=
+=
let gui = instance () in
let dialog = gui#newUriDialog () in
dialog#uriEntryHBox#misc#hide ();
@@ -1412,13 +1465,15 @@ let interactive_string_choice
let rec colorize acc_len = function
| [] ->
let floc = HExtlib.floc_of_loc (acc_len,hack_len) in
- fst(MatitaGtkMisc.utf8_parsed_text text floc)
+ escape_pango_markup (fst(MatitaGtkMisc.utf8_parsed_text text floc))
| he::tl ->
let start, stop = HExtlib.loc_of_floc he in
let floc1 = HExtlib.floc_of_loc (acc_len,start) in
let str1,_=MatitaGtkMisc.utf8_parsed_text text floc1 in
let str2,_ = MatitaGtkMisc.utf8_parsed_text text he in
- str1 ^ "" ^ str2 ^ "" ^ colorize stop tl
+ escape_pango_markup str1 ^ "" ^
+ escape_pango_markup str2 ^ "" ^
+ colorize stop tl
in
(* List.iter (fun l -> let start, stop = HExtlib.loc_of_floc l in
Printf.eprintf "(%d,%d)" start stop) locs; *)
@@ -1520,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;