X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaGui.ml;h=3ea6b4f87f8f33d2d1953d305473a8b1254ae681;hb=8653d506aacaf019deb3438bd4681ad1000061bd;hp=589da7dcc8e9adb6eed32d161a7b9b583ec23b33;hpb=e89367d2ad0e194c547a4e84cac87b7a48b69600;p=helm.git diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index 589da7dcc..3ea6b4f87 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -29,6 +29,8 @@ open MatitaGeneratedGui open MatitaGtkMisc open MatitaMisc +exception Found of int + let gui_instance = ref None class type browserWin = @@ -137,6 +139,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 +363,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 _ = @@ -435,7 +439,6 @@ class gui () = (fun () -> develList#toplevel#misc#hide()); ignore(develList#toplevel#event#connect#delete (fun _ -> develList#toplevel#misc#hide();true)); - let selected_devel = ref None in connect_menu_item main#developmentsMenuItem (fun () -> refresh_devels_win ();develList#toplevel#misc#show ()); @@ -570,9 +573,38 @@ class gui () = GtkSignal.user_handler := (fun exn -> if not (Helm_registry.get_bool "matita.debug") then - MatitaLog.error (MatitaExcPp.to_string exn) + let floc, msg = MatitaExcPp.to_string exn in + begin + match floc with + None -> () + | Some floc -> + let (x, y) = HExtlib.loc_of_floc floc in + let script = MatitaScript.current () in + let locked_mark = script#locked_mark in + let error_tag = script#error_tag in + let baseoffset = + (source_buffer#get_iter_at_mark (`MARK locked_mark))#offset in + let x' = baseoffset + x in + let y' = baseoffset + y in + let x_iter = source_buffer#get_iter (`OFFSET x') in + let y_iter = source_buffer#get_iter (`OFFSET y') in + source_buffer#apply_tag error_tag ~start:x_iter ~stop:y_iter; + let id = ref None in + id := Some (source_buffer#connect#changed ~callback:(fun () -> + source_buffer#remove_tag error_tag + ~start:source_buffer#start_iter + ~stop:source_buffer#end_iter; + match !id with + | None -> assert false (* a race condition occurred *) + | Some id -> + (new GObj.gobject_ops source_buffer#as_buffer)#disconnect id)); + source_buffer#place_cursor + (source_buffer#get_iter (`OFFSET x')); + end; + MatitaLog.error msg 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 -> @@ -618,7 +650,6 @@ class gui () = in let loadScript () = let script = s () in - let status = script#status in try match self#chooseFile () with | Some f -> @@ -697,25 +728,16 @@ class gui () = 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 *) @@ -777,6 +799,58 @@ 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 + 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 *) @@ -1003,7 +1077,6 @@ let interactive_uri_choice (selection_mode :> Gtk.Tags.selection_mode); let model = new stringListModel dialog#uriChoiceTreeView in let choices = ref None in - let nonvars = ref false in (match copy_cb with | None -> () | Some cb -> @@ -1099,7 +1172,6 @@ let interactive_interp_choice () choices = assert (choices <> []); let dialog = gui#newRecordDialog () in let model = new interpModel dialog#recordChoiceTreeView choices in - let interp_len = List.length (List.hd choices) in dialog#recordChoiceDialog#set_title "Interpretation choice"; dialog#recordChoiceDialogLabel#set_label "Choose an interpretation:"; let interp_no = ref None in