From 215cb34e905e846d37c873224df1ec30bf81ba87 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Fri, 4 Nov 2005 14:03:06 +0000 Subject: [PATCH] added support for expansion of ligatures ALT-L will trigger it --- helm/matita/matita.glade | 43 ++++++++++++++++++++++++---------------- helm/matita/matitaGui.ml | 27 +++++++++++++++++++++++++ 2 files changed, 53 insertions(+), 17 deletions(-) diff --git a/helm/matita/matita.glade b/helm/matita/matita.glade index 3c664c43c..6b951b21d 100644 --- a/helm/matita/matita.glade +++ b/helm/matita/matita.glade @@ -877,7 +877,7 @@ - + True gtk-new 1 @@ -898,7 +898,7 @@ - + True gtk-open 1 @@ -919,7 +919,7 @@ - + True gtk-save 1 @@ -940,7 +940,7 @@ - + True gtk-save-as 1 @@ -961,7 +961,7 @@ - + True gtk-execute 1 @@ -988,7 +988,7 @@ - + True gtk-quit 1 @@ -1023,7 +1023,7 @@ - + True gtk-undo 1 @@ -1045,7 +1045,7 @@ - + True gtk-redo 1 @@ -1072,7 +1072,7 @@ - + True gtk-cut 1 @@ -1093,7 +1093,7 @@ - + True gtk-copy 1 @@ -1114,7 +1114,7 @@ - + True gtk-paste 1 @@ -1134,7 +1134,7 @@ True - + True gtk-delete 1 @@ -1175,7 +1175,7 @@ - + True gtk-find-and-replace 1 @@ -1194,6 +1194,15 @@ + + + True + Next ligature + True + + + + True @@ -1265,7 +1274,7 @@ - + True gtk-zoom-in 1 @@ -1287,7 +1296,7 @@ - + True gtk-zoom-out 1 @@ -1308,7 +1317,7 @@ - + True gtk-zoom-100 1 @@ -1360,7 +1369,7 @@ True - + True gtk-about 1 diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index 589da7dcc..dc3fb07ce 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -137,6 +137,7 @@ class gui () = val mutable script_fname = None val mutable font_size = default_font_size val mutable next_devel_must_contain = None + val mutable next_ligatures = [] initializer (* glade's check widgets *) @@ -360,6 +361,7 @@ 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; ignore (findRepl#findEntry#connect#activate find_forward); (* interface lockers *) let lock_world _ = @@ -573,6 +575,7 @@ class gui () = MatitaLog.error (MatitaExcPp.to_string exn) else raise exn); (* script *) + let _ = source_buffer#connect#changed (fun _ -> next_ligatures <- []) in let _ = match GSourceView.source_language_from_file BuildTimeConf.lang_file with | None -> @@ -777,6 +780,30 @@ class gui () = MatitaMathView.update_font_sizes ()); MatitaMathView.reset_font_size (); + method private nextLigature () = + let iter = source_buffer#get_iter_at_mark `INSERT in + let write_ligature len s = + source_buffer#delete ~start:iter ~stop:(iter#copy#backward_chars len); + source_buffer#insert ~iter:(source_buffer#get_iter_at_mark `INSERT) s + in + (match next_ligatures with + | [] -> (* find ligatures and fill next_ligatures, then try again *) + let last_word = iter#get_slice ~stop:iter#copy#backward_word_start in + let len = String.length last_word in + let i = ref (len - 1) in + while !i >= 0 && CicNotationLexer.is_ligature_char last_word.[!i] do + decr i + done; + let ligature = String.sub last_word (!i + 1) (len - (!i + 1)) in + (match CicNotationLexer.lookup_ligatures ligature with + | [] -> () + | hd :: tl -> + write_ligature (String.length ligature) hd; + next_ligatures <- tl @ [ hd ]) + | hd :: tl -> + write_ligature 1 hd; + next_ligatures <- tl @ [ hd ]) + method private externalEditor () = let cmd = Helm_registry.get "matita.external_editor" in (* ZACK uncomment to enable interactive ask of external editor command *) -- 2.39.2