X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaGui.ml;h=7f4571c557ac4f29f0b909b8347bad205ac006d6;hb=9449ec60150ea2326d7b54ad9c4f51e36d06bb65;hp=5d9d87c865dd045743d59c8d14d876aa2d3e7760;hpb=691ab989638ff10484d96b3308b509fecd9ec1c3;p=helm.git diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml index 5d9d87c86..7f4571c55 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,9 +327,10 @@ let rec interactive_error_interp ~all_passes String.concat "\n" ("" :: List.map - (fun k,value -> + (fun k,value -> DisambiguatePp.pp_environment - (DisambiguateTypes.Environment.add k value + (DisambiguateTypes.Environment.add k + (value,(fun _ _ _ -> Cic.Implicit None)) DisambiguateTypes.Environment.empty)) diff) ^ "\n" in @@ -433,10 +434,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 +689,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 +763,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 +903,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,18 +969,12 @@ class gui () = (fun _ -> MatitaAutoGui.auto_dialog Auto.get_auto_status); connect_menu_item main#showTermGrammarMenuItem (fun _ -> - let w = MatitaGtkMisc.new_search_win "Terms grammar" (Print_grammar.ebnf_of_term ()) in - w#toplevel#set_transient_for (main#toplevel#as_window); - w#toplevel#show ()); + let c = MatitaMathView.cicBrowser () in + c#load (`About `Grammar)); connect_menu_item main#showUnicodeTable (fun _ -> - let text = String.concat "\n" - (List.map (fun (k,vs) -> "\t" ^ k ^ "\t" ^ String.concat ", " vs) - (Utf8Macro.pp_table ())) - in - let w = MatitaGtkMisc.new_search_win "Tex/UTF8 table" text in - w#toplevel#set_transient_for (main#toplevel#as_window); - w#toplevel#show ()); + let c = MatitaMathView.cicBrowser () in + c#load (`About `TeX)); (* script monospace font stuff *) self#updateFontSize (); (* debug menu *) @@ -968,7 +1024,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 (); @@ -1140,6 +1196,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 @@ -1167,12 +1225,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 @@ -1237,7 +1295,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; @@ -1381,9 +1440,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 (); @@ -1399,13 +1459,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; *) @@ -1424,6 +1486,7 @@ 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 = @@ -1507,8 +1570,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;