X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaGui.ml;h=f0bd8acc027f42e076eb143a8b155ae2f7150fee;hb=7a060397679753a0233139b1ba83ac83c2c49949;hp=9e8cfd86cd4c3163be5906acf735fd63df9d9c0f;hpb=9e1d0c4f6ddf36cd691ef0d3c95aaa7f694977f0;p=helm.git diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml index 9e8cfd86c..f0bd8acc0 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 @@ -380,15 +387,22 @@ class gui () = Helm_registry.get_opt_default Helm_registry.int ~default:BuildTimeConf.default_font_size "matita.font_size" in + let similarsymbols_tag_name = "similarsymbolos" in + let similarsymbols_tag = `NAME similarsymbols_tag_name in let source_buffer = source_view#source_buffer in object (self) val mutable chosen_file = None val mutable _ok_not_exists = false val mutable _only_directory = false val mutable font_size = default_font_size - val mutable next_ligatures = [] + val mutable similarsymbols = [] val clipboard = GData.clipboard Gdk.Atom.clipboard val primary = GData.clipboard Gdk.Atom.primary + + method private reset_similarsymbols = + similarsymbols <- []; + try source_buffer#delete_mark similarsymbols_tag + with GText.No_such_mark _ -> () initializer let s () = MatitaScript.current () in @@ -433,10 +447,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 () = @@ -626,7 +648,10 @@ class gui () = source_buffer#move_mark `SEL_BOUND source_buffer#end_iter); connect_menu_item main#findReplMenuItem show_find_Repl; connect_menu_item main#externalEditorMenuItem self#externalEditor; - connect_menu_item main#ligatureButton self#nextLigature; + connect_menu_item main#ligatureButton self#nextSimilarSymbol; + ignore(source_buffer#connect#after#insert_text + ~callback:(fun iter str -> + if false && str = " " then self#expand_virtual_if_any iter " ")); ignore (findRepl#findEntry#connect#activate find_forward); (* interface lockers *) let lock_world _ = @@ -680,7 +705,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 +779,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 *) @@ -790,7 +866,6 @@ class gui () = notify_exn exn else raise exn); (* script *) - ignore (source_buffer#connect#mark_set (fun _ _ -> next_ligatures <- [])); let _ = match GSourceView.source_language_from_file BuildTimeConf.lang_file with | None -> @@ -843,6 +918,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 -> () @@ -1013,58 +1090,67 @@ class gui () = method pastePattern () = source_view#buffer#insert (MatitaMathView.paste_clipboard `Pattern) - method private nextLigature () = - let iter = source_buffer#get_iter_at_mark `INSERT in - let write_ligature len s = + method private expand_virtual_if_any iter tok = + try + let len = MatitaGtkMisc.utf8_string_length tok in + let last_word = + let prev = iter#copy#backward_chars len in + prev#get_slice ~stop:(prev#copy#backward_find_char + (fun x -> Glib.Unichar.isspace x || x = Glib.Utf8.first_char "\\")) + in + let inplaceof, symb = Virtuals.symbol_of_virtual last_word in + self#reset_similarsymbols; + let s = Glib.Utf8.from_unichar symb in + let iter = source_buffer#get_iter_at_mark `INSERT in + assert(Glib.Utf8.validate s); + source_buffer#delete ~start:iter + ~stop:(iter#copy#backward_chars + (MatitaGtkMisc.utf8_string_length inplaceof + len)); + source_buffer#insert ~iter:(source_buffer#get_iter_at_mark `INSERT) + (if inplaceof.[0] = '\\' then s else (s ^ tok)) + with Virtuals.Not_a_virtual -> () + + method private nextSimilarSymbol () = + let write_similarsymbol s = + let s = Glib.Utf8.from_unichar s in + let iter = source_buffer#get_iter_at_mark `INSERT in assert(Glib.Utf8.validate s); - source_buffer#delete ~start:iter ~stop:(iter#copy#backward_chars len); - source_buffer#insert ~iter:(source_buffer#get_iter_at_mark `INSERT) s + source_buffer#delete ~start:iter ~stop:(iter#copy#backward_chars 1); + source_buffer#insert ~iter:(source_buffer#get_iter_at_mark `INSERT) s; + (try source_buffer#delete_mark similarsymbols_tag + with GText.No_such_mark _ -> ()); + ignore(source_buffer#create_mark ~name:similarsymbols_tag_name + (source_buffer#get_iter_at_mark `INSERT)); in - let get_ligature word = - let len = String.length word in - let aux_tex () = - try - for i = len - 1 downto 0 do - if HExtlib.is_alpha word.[i] then () - else - (if word.[i] = '\\' then raise (Found i) else raise (Found ~-1)) - done; - None - with Found i -> - if i = ~-1 then None else Some (String.sub word i (len - i)) - in - let aux_ligature () = - try - for i = len - 1 downto 0 do - if CicNotationLexer.is_ligature_char word.[i] then () - else raise (Found (i+1)) - done; - raise (Found 0) - with - | Found i -> - (try - Some (String.sub word i (len - i)) - with Invalid_argument _ -> None) - in - match aux_tex () with - | Some macro -> macro - | None -> (match aux_ligature () with Some l -> l | None -> word) + let new_similarsymbol = + try + let iter_ins = source_buffer#get_iter_at_mark `INSERT in + let iter_lig = source_buffer#get_iter_at_mark similarsymbols_tag in + not (iter_ins#equal iter_lig) + with GText.No_such_mark _ -> true in - (match next_ligatures with - | [] -> (* find ligatures and fill next_ligatures, then try again *) - let last_word = - iter#get_slice - ~stop:(iter#copy#backward_find_char Glib.Unichar.isspace) + if new_similarsymbol then + let last_symbol = + let i = source_buffer#get_iter_at_mark `INSERT in + Glib.Utf8.first_char (i#get_slice ~stop:(i#copy#backward_chars 1)) in - let ligature = get_ligature last_word in - (match CicNotationLexer.lookup_ligatures ligature with - | [] -> () - | hd :: tl -> - write_ligature (MatitaGtkMisc.utf8_string_length ligature) hd; - next_ligatures <- tl @ [ hd ]) - | hd :: tl -> - write_ligature 1 hd; - next_ligatures <- tl @ [ hd ]) + (match Virtuals.similar_symbols last_symbol with + | [] -> + let i = source_buffer#get_iter_at_mark `INSERT in + self#expand_virtual_if_any i "" + | hd :: next ::tl -> + let hd, tl = + if hd = last_symbol then next, tl @ [hd] else hd, (next::tl) + in + write_similarsymbol hd; + similarsymbols <- tl @ [ hd ] + | _ -> assert false) (* singleton eq classes are a non sense *) + else + match similarsymbols with + | [] -> () + | hd :: tl -> + similarsymbols <- tl @ [ hd ]; + write_similarsymbol hd method private externalEditor () = let cmd = Helm_registry.get "matita.external_editor" in @@ -1134,6 +1220,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 @@ -1166,7 +1254,6 @@ class gui () = self#check_widgets (); let combo_widget = combo#coerce in uriHBox#pack ~from:`END ~fill:true ~expand:true combo_widget; - self#toplevel#set_transient_for main#toplevel#as_window; combo#misc#grab_focus () method browserUri = combo end @@ -1377,14 +1464,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 text = Pcre.replace ~pat:"<" ~templ:"<" text in - let text = Pcre.replace ~pat:"'" ~templ:"'" text in - let text = Pcre.replace ~pat:"\"" ~templ:""" text in - let text = Pcre.replace ~pat:">" ~templ:">" text in let gui = instance () in let dialog = gui#newUriDialog () in dialog#uriEntryHBox#misc#hide (); @@ -1400,13 +1483,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; *) @@ -1508,8 +1593,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;