open MatitaGtkMisc
open MatitaMisc
+exception Found of int
+
let gui_instance = ref None
class type browserWin =
MatitaGtkMisc.ask_confirmation
~parent ~title:"Unsaved work!"
~message:("Your work is <b>unsaved</b>!\n\n"^
- "<i>Do you want to save the script before exiting?</i>")
+ "<i>Do you want to save the script before continuing?</i>")
()
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 *)
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 _ =
MatitaLog.error (MatitaExcPp.to_string 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 ->
(s ())#saveToFile ();
console#message ("'"^f^"' saved.\n");
in
+ let abandon_script () =
+ let status = (s ())#status in
+ if source_view#buffer#modified then
+ (match ask_unsaved main#toplevel with
+ | `YES -> saveScript ()
+ | `NO -> ()
+ | `CANCEL -> raise MatitaTypes.Cancel);
+ (match script_fname with
+ | None -> ()
+ | Some fname -> ask_and_save_moo_if_needed main#toplevel fname status);
+ in
let loadScript () =
let script = s () in
let status = script#status in
try
match self#chooseFile () with
| Some f ->
- if source_view#buffer#modified then
- begin
- match ask_unsaved main#toplevel with
- | `YES -> saveScript ()
- | `NO -> ()
- | `CANCEL -> raise MatitaTypes.Cancel
- end;
- (match script_fname with
- | None -> ()
- | Some fname ->
- ask_and_save_moo_if_needed main#toplevel fname status);
- script#reset ();
- script#assignFileName f;
- source_view#source_buffer#begin_not_undoable_action ();
- script#loadFromFile f;
- source_view#source_buffer#end_not_undoable_action ();
- console#message ("'"^f^"' loaded.\n");
- self#_enableSaveTo f
+ abandon_script ();
+ script#reset ();
+ script#assignFileName f;
+ source_view#source_buffer#begin_not_undoable_action ();
+ script#loadFromFile f;
+ source_view#source_buffer#end_not_undoable_action ();
+ console#message ("'"^f^"' loaded.\n");
+ self#_enableSaveTo f
| None -> ()
with MatitaTypes.Cancel -> ()
in
let newScript () =
+ abandon_script ();
source_view#source_buffer#begin_not_undoable_action ();
(s ())#reset ();
(s ())#template ();
connect_button main#scriptRetractButton retract;
connect_button main#scriptTopButton top;
connect_button main#scriptBottomButton bottom;
- connect_key GdkKeysyms._Down advance;
- connect_key GdkKeysyms._Up retract;
- connect_key GdkKeysyms._Home top;
- connect_key GdkKeysyms._End bottom;
connect_button main#scriptJumpButton jump;
+ connect_menu_item main#scriptAdvanceMenuItem advance;
+ connect_menu_item main#scriptRetractMenuItem retract;
+ connect_menu_item main#scriptTopMenuItem top;
+ connect_menu_item main#scriptBottomMenuItem bottom;
+ connect_menu_item main#scriptJumpMenuItem jump;
connect_menu_item main#openMenuItem loadScript;
connect_menu_item main#saveMenuItem saveScript;
connect_menu_item main#saveAsMenuItem saveAsScript;
connect_menu_item main#newMenuItem newScript;
- connect_key GdkKeysyms._period
- (fun () ->
- source_buffer#insert ~iter:(source_buffer#get_iter_at_mark `INSERT)
- ".\n";
- advance ());
- connect_key GdkKeysyms._Return
- (fun () ->
- source_buffer#insert ~iter:(source_buffer#get_iter_at_mark `INSERT)
- "\n";
- advance ());
(* script monospace font stuff *)
self#updateFontSize ();
(* debug menu *)
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
+ 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)
+ 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)
+ in
+ let ligature = get_ligature last_word 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 *)
projects / helm.git / blobdiff