X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaGui.ml;h=ed739eefbebb8c9be4a9e5ab95f919166625a722;hb=771ee8b9d122fa963881c876e86f90531bb7434f;hp=5d223208f042f782ee409e890272a15cef3e2441;hpb=b2f2e47efe1e01df81cb7659c30eeb76f1f830da;p=helm.git
diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index 5d223208f..ed739eefb 100644
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -23,12 +23,16 @@
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open Printf
open MatitaGeneratedGui
open MatitaGtkMisc
open MatitaMisc
+exception Found of int
+
let gui_instance = ref None
class type browserWin =
@@ -51,7 +55,7 @@ class console ~(buffer: GText.buffer) () =
method debug s = buffer#insert ~iter:buffer#end_iter ~tags:[debug_tag] s
method clear () =
buffer#delete ~start:buffer#start_iter ~stop:buffer#end_iter
- method log_callback (tag: MatitaLog.log_tag) s =
+ method log_callback (tag: HLog.log_tag) s =
match tag with
| `Debug -> self#debug (s ^ "\n")
| `Error -> self#error (s ^ "\n")
@@ -59,29 +63,40 @@ class console ~(buffer: GText.buffer) () =
| `Warning -> self#warning (s ^ "\n")
end
-let clean_current_baseuri status =
+let clean_current_baseuri grafite_status =
try
- let baseuri = MatitaTypes.get_string_option status "baseuri" in
- MatitacleanLib.clean_baseuris [baseuri]
- with MatitaTypes.Option_error _ -> ()
+ let baseuri = GrafiteTypes.get_string_option grafite_status "baseuri" in
+ let basedir = Helm_registry.get "matita.basedir" in
+ LibraryClean.clean_baseuris ~basedir [baseuri]
+ with GrafiteTypes.Option_error _ -> ()
-let ask_and_save_moo_if_needed parent fname status =
+let ask_and_save_moo_if_needed parent fname lexicon_status grafite_status =
+ let basedir = Helm_registry.get "matita.basedir" in
+ let baseuri = DependenciesParser.baseuri_of_script ~include_paths:[] fname in
+ let moo_fname = LibraryMisc.obj_file_of_baseuri ~basedir ~baseuri in
let save () =
- let moo_fname = MatitaMisc.obj_file_of_script fname in
- MatitaMoo.save_moo moo_fname status.MatitaTypes.moo_content_rev in
- if (MatitaScript.instance ())#eos &&
- status.MatitaTypes.proof_status = MatitaTypes.No_proof
+ let metadata_fname =
+ LibraryMisc.metadata_file_of_baseuri ~basedir ~baseuri in
+ let lexicon_fname =
+ LibraryMisc.lexicon_file_of_baseuri ~basedir ~baseuri
+ in
+ GrafiteMarshal.save_moo moo_fname
+ grafite_status.GrafiteTypes.moo_content_rev;
+ LibraryNoDb.save_metadata metadata_fname
+ lexicon_status.LexiconEngine.metadata;
+ LexiconMarshal.save_lexicon lexicon_fname
+ lexicon_status.LexiconEngine.lexicon_content_rev
+ in
+ if (MatitaScript.current ())#eos &&
+ grafite_status.GrafiteTypes.proof_status = GrafiteTypes.No_proof
then
begin
- let mooname =
- MatitaMisc.obj_file_of_script fname
- in
let rc =
MatitaGtkMisc.ask_confirmation
~title:"A .moo can be generated"
~message:(Printf.sprintf
"%s can be generated for %s.\nShould I generate it?"
- (Filename.basename mooname) (Filename.basename fname))
+ (Filename.basename moo_fname) (Filename.basename fname))
~parent ()
in
let b =
@@ -91,20 +106,30 @@ let ask_and_save_moo_if_needed parent fname status =
| `CANCEL -> raise MatitaTypes.Cancel
in
if b then
- save ()
+ save ()
else
- clean_current_baseuri status
+ clean_current_baseuri grafite_status
end
else
- clean_current_baseuri status
+ clean_current_baseuri grafite_status
let ask_unsaved parent =
MatitaGtkMisc.ask_confirmation
~parent ~title:"Unsaved work!"
~message:("Your work is unsaved!\n\n"^
- "Do you want to save the script before exiting?")
+ "Do you want to save the script before continuing?")
()
+(** Selection handling
+ * Two clipboards are used: "clipboard" and "primary".
+ * "primary" is used by X, when you hit the middle button mouse is content is
+ * pasted between applications. In Matita this selection always contain the
+ * textual version of the selected term.
+ * "clipboard" is used inside Matita only and support ATM two different targets:
+ * "TERM" and "PATTERN", in the future other targets like "MATHMLCONTENT" may
+ * be added
+ *)
+
class gui () =
(* creation order _is_ relevant for windows placement *)
let main = new mainWin () in
@@ -137,6 +162,9 @@ 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 = []
+ val clipboard = GData.clipboard Gdk.Atom.clipboard
+ val primary = GData.clipboard Gdk.Atom.primary
initializer
(* glade's check widgets *)
@@ -218,7 +246,7 @@ class gui () =
let safe_undo =
fun () ->
(* phase 1: we save the actual status of the marks and we undo *)
- let locked_mark = `MARK ((MatitaScript.instance ())#locked_mark) in
+ let locked_mark = `MARK ((MatitaScript.current ())#locked_mark) in
let locked_iter = source_view#buffer#get_iter_at_mark locked_mark in
let locked_iter_offset = locked_iter#offset in
let mark2 =
@@ -246,7 +274,7 @@ class gui () =
if mark_iter#offset < locked_iter_offset then
begin
source_view#buffer#move_mark `INSERT ~where:mark_iter;
- (MatitaScript.instance ())#goto `Cursor ();
+ (MatitaScript.current ())#goto `Cursor ();
end;
(* phase 4: we perform again the undo. This time we are sure that
the text to undo is not locked *)
@@ -256,7 +284,7 @@ class gui () =
fun () ->
(* phase 1: we save the actual status of the marks, we redo and
we undo *)
- let locked_mark = `MARK ((MatitaScript.instance ())#locked_mark) in
+ let locked_mark = `MARK ((MatitaScript.current ())#locked_mark) in
let locked_iter = source_view#buffer#get_iter_at_mark locked_mark in
let locked_iter_offset = locked_iter#offset in
let mark2 =
@@ -284,7 +312,7 @@ class gui () =
if mark_iter#offset < locked_iter_offset then
begin
source_view#buffer#move_mark `INSERT ~where:mark_iter;
- (MatitaScript.instance ())#goto `Cursor ();
+ (MatitaScript.current ())#goto `Cursor ();
end;
(* phase 4: we perform again the redo. This time we are sure that
the text to redo is not locked *)
@@ -304,8 +332,32 @@ class gui () =
let undoMenuItem, redoMenuItem =
match menuItems with
[undo;redo;sep1;cut;copy;paste;delete;sep2;
- selectall;sep3;inputmethod;insertunicodecharacter] -> undo,redo
+ selectall;sep3;inputmethod;insertunicodecharacter] ->
+ List.iter menu#remove [ copy; cut; delete; paste ];
+ undo,redo
| _ -> assert false in
+ let add_menu_item =
+ let i = ref 2 in (* last occupied position *)
+ fun ?label ?stock () ->
+ incr i;
+ GMenu.image_menu_item ?label ?stock ~packing:(menu#insert ~pos:!i)
+ ()
+ in
+ let copy = add_menu_item ~stock:`COPY () in
+ let cut = add_menu_item ~stock:`CUT () in
+ let delete = add_menu_item ~stock:`DELETE () in
+ let paste = add_menu_item ~stock:`PASTE () in
+ let paste_pattern = add_menu_item ~label:"Paste as pattern" () in
+ copy#misc#set_sensitive self#canCopy;
+ cut#misc#set_sensitive self#canCut;
+ delete#misc#set_sensitive self#canDelete;
+ paste#misc#set_sensitive self#canPaste;
+ paste_pattern#misc#set_sensitive self#canPastePattern;
+ connect_menu_item copy self#copy;
+ connect_menu_item cut self#cut;
+ connect_menu_item delete self#delete;
+ connect_menu_item paste self#paste;
+ connect_menu_item paste_pattern self#pastePattern;
let new_undoMenuItem =
GMenu.image_menu_item
~image:(GMisc.image ~stock:`UNDO ())
@@ -326,39 +378,24 @@ class gui () =
(redoMenuItem#misc#get_flag `SENSITIVE);
menu#remove (redoMenuItem :> GMenu.menu_item);
connect_menu_item new_redoMenuItem safe_redo));
- let clipboard = GData.clipboard Gdk.Atom.clipboard in
- let text_selected () =
- (source_buffer#get_iter_at_mark `INSERT)#compare
- (source_buffer#get_iter_at_mark `SEL_BOUND) <> 0
- in
- let markup_selected () = MatitaMathView.get_selections () <> None in
+
connect_menu_item main#editMenu (fun () ->
- let text_selected = text_selected () in
- let markup_selected = markup_selected () in
- let something_selected = text_selected || markup_selected in
- main#cutMenuItem#misc#set_sensitive text_selected;
- main#copyMenuItem#misc#set_sensitive something_selected;
- main#deleteMenuItem#misc#set_sensitive text_selected;
- main#pasteMenuItem#misc#set_sensitive (clipboard#text <> None));
- connect_menu_item main#cutMenuItem (fun () ->
- source_view#buffer#cut_clipboard clipboard);
- connect_menu_item main#copyMenuItem (fun () ->
- if text_selected () then
- source_view#buffer#copy_clipboard clipboard
- else if markup_selected () then
- match MatitaMathView.get_selections () with
- | None
- | Some [] -> ()
- | Some (s :: _) -> clipboard#set_text s);
- connect_menu_item main#pasteMenuItem (fun () ->
- source_view#buffer#paste_clipboard clipboard;
- (MatitaScript.instance ())#clean_dirty_lock);
- connect_menu_item main#deleteMenuItem (fun () ->
- ignore (source_view#buffer#delete_selection ()));
+ main#copyMenuItem#misc#set_sensitive self#canCopy;
+ main#cutMenuItem#misc#set_sensitive self#canCut;
+ main#deleteMenuItem#misc#set_sensitive self#canDelete;
+ main#pasteMenuItem#misc#set_sensitive self#canPaste;
+ main#pastePatternMenuItem#misc#set_sensitive self#canPastePattern);
+ connect_menu_item main#copyMenuItem self#copy;
+ connect_menu_item main#cutMenuItem self#cut;
+ connect_menu_item main#deleteMenuItem self#delete;
+ connect_menu_item main#pasteMenuItem self#paste;
+ connect_menu_item main#pastePatternMenuItem self#pastePattern;
connect_menu_item main#selectAllMenuItem (fun () ->
source_buffer#move_mark `INSERT source_buffer#start_iter;
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 _ =
@@ -434,7 +471,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 ());
@@ -467,7 +503,7 @@ class gui () =
newDevel#toplevel#misc#hide()
end
else
- MatitaLog.error ("The selected root does not contain " ^
+ HLog.error ("The selected root does not contain " ^
match next_devel_must_contain with
| Some x -> x
| _ -> assert false));
@@ -518,18 +554,22 @@ class gui () =
(* toolbar *)
let module A = GrafiteAst in
let hole = CicNotationPt.UserInput in
- let loc = DisambiguateTypes.dummy_floc in
+ let loc = HExtlib.dummy_floc in
let tac ast _ =
- if (MatitaScript.instance ())#onGoingProof () then
- (MatitaScript.instance ())#advance
- ~statement:("\n" ^ GrafiteAstPp.pp_tactical (A.Tactic (loc, ast)))
+ if (MatitaScript.current ())#onGoingProof () then
+ (MatitaScript.current ())#advance
+ ~statement:("\n"
+ ^ GrafiteAstPp.pp_tactical ~term_pp:CicNotationPp.pp_term
+ ~lazy_term_pp:CicNotationPp.pp_term (A.Tactic (loc, ast)))
()
in
let tac_w_term ast _ =
- if (MatitaScript.instance ())#onGoingProof () then
+ if (MatitaScript.current ())#onGoingProof () then
let buf = source_buffer in
buf#insert ~iter:(buf#get_iter_at_mark (`NAME "locked"))
- ("\n" ^ GrafiteAstPp.pp_tactic ast)
+ ("\n"
+ ^ GrafiteAstPp.pp_tactic ~term_pp:CicNotationPp.pp_term
+ ~lazy_term_pp:CicNotationPp.pp_term ast)
in
let tbar = main in
connect_button tbar#introsButton (tac (A.Intros (loc, None, [])));
@@ -549,7 +589,7 @@ class gui () =
(tac_w_term (A.Transitivity (loc, hole)));
connect_button tbar#assumptionButton (tac (A.Assumption loc));
connect_button tbar#cutButton (tac_w_term (A.Cut (loc, None, hole)));
- connect_button tbar#autoButton (tac (A.Auto (loc,None,None,None)));
+ connect_button tbar#autoButton (tac (A.Auto (loc,None,None,None,None)));
MatitaGtkMisc.toggle_widget_visibility
~widget:(main#tacticsButtonsHandlebox :> GObj.widget)
~check:main#tacticsBarMenuItem;
@@ -565,23 +605,54 @@ class gui () =
~check:main#fullscreenMenuItem;
main#fullscreenMenuItem#set_active false;
(* log *)
- MatitaLog.set_log_callback self#console#log_callback;
+ HLog.set_log_callback self#console#log_callback;
GtkSignal.user_handler :=
- (fun exn ->
- if Helm_registry.get_bool "matita.catch_top_level_exn" then
- MatitaLog.error (MatitaExcPp.to_string exn)
+ (function
+ | MatitaScript.ActionCancelled -> ()
+ | exn ->
+ if not (Helm_registry.get_bool "matita.debug") then
+ 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;
+ HLog.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 ->
- MatitaLog.warn (sprintf "can't load language file %s"
+ HLog.warn (sprintf "can't load language file %s"
BuildTimeConf.lang_file)
| Some matita_lang ->
source_buffer#set_language matita_lang;
source_buffer#set_highlight true
in
- let s () = MatitaScript.instance () in
+ let s () = MatitaScript.current () in
let disableSave () =
script_fname <- None;
main#saveMenuItem#misc#set_sensitive false
@@ -604,34 +675,38 @@ class gui () =
(s ())#saveToFile ();
console#message ("'"^f^"' saved.\n");
in
+ let abandon_script () =
+ let lexicon_status = (s ())#lexicon_status in
+ let grafite_status = (s ())#grafite_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
+ lexicon_status grafite_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 ();
@@ -642,25 +717,20 @@ class gui () =
let cursor () =
source_buffer#place_cursor
(source_buffer#get_iter_at_mark (`NAME "locked")) in
- let advance _ = (MatitaScript.instance ())#advance (); cursor () in
- let retract _ = (MatitaScript.instance ())#retract (); cursor () in
- let top _ = (MatitaScript.instance ())#goto `Top (); cursor () in
- let bottom _ = (MatitaScript.instance ())#goto `Bottom (); cursor () in
- let jump _ = (MatitaScript.instance ())#goto `Cursor (); cursor () in
+ let advance _ = (MatitaScript.current ())#advance (); cursor () in
+ let retract _ = (MatitaScript.current ())#retract (); cursor () in
+ let top _ = (MatitaScript.current ())#goto `Top (); cursor () in
+ let bottom _ = (MatitaScript.current ())#goto `Bottom (); cursor () in
+ let jump _ = (MatitaScript.current ())#goto `Cursor (); cursor () in
let advance = locker (keep_focus advance) in
let retract = locker (keep_focus retract) in
let top = locker (keep_focus top) in
let bottom = locker (keep_focus bottom) in
let jump = locker (keep_focus jump) in
- let connect_key sym f =
- connect_key main#mainWinEventBox#event
- ~modifiers:[`CONTROL] ~stop:true sym f;
- connect_key self#sourceView#event
- ~modifiers:[`CONTROL] ~stop:true sym f
- in
(* quit *)
self#setQuitCallback (fun () ->
- let status = (MatitaScript.instance ())#status in
+ let lexicon_status = (MatitaScript.current ())#lexicon_status in
+ let grafite_status = (MatitaScript.current ())#grafite_status in
if source_view#buffer#modified then
begin
let rc = ask_unsaved main#toplevel in
@@ -672,8 +742,8 @@ class gui () =
(match script_fname with
| None -> ()
| Some fname ->
- ask_and_save_moo_if_needed
- main#toplevel fname status);
+ ask_and_save_moo_if_needed main#toplevel
+ fname lexicon_status grafite_status);
GMain.Main.quit ()
end
| `NO -> GMain.Main.quit ()
@@ -683,10 +753,11 @@ class gui () =
else
begin
(match script_fname with
- | None -> clean_current_baseuri status; GMain.Main.quit ()
+ | None -> clean_current_baseuri grafite_status; GMain.Main.quit ()
| Some fname ->
try
- ask_and_save_moo_if_needed main#toplevel fname status;
+ ask_and_save_moo_if_needed main#toplevel fname lexicon_status
+ grafite_status;
GMain.Main.quit ()
with MatitaTypes.Cancel -> ())
end);
@@ -694,25 +765,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 *)
@@ -733,7 +795,7 @@ class gui () =
main#hpaneScriptSequent#set_position script_w;
(* source_view *)
ignore(source_view#connect#after#paste_clipboard
- ~callback:(fun () -> (MatitaScript.instance ())#clean_dirty_lock));
+ ~callback:(fun () -> (MatitaScript.current ())#clean_dirty_lock));
(* clean_locked is set to true only "during" a PRIMARY paste
operation (i.e. by clicking with the second mouse button) *)
let clean_locked = ref false in
@@ -750,11 +812,11 @@ class gui () =
~callback:(
fun tag ~start:_ ~stop:_ ->
if !clean_locked &&
- tag#get_oid = (MatitaScript.instance ())#locked_tag#get_oid
+ tag#get_oid = (MatitaScript.current ())#locked_tag#get_oid
then
begin
clean_locked := false;
- (MatitaScript.instance ())#clean_dirty_lock;
+ (MatitaScript.current ())#clean_dirty_lock;
clean_locked := true
end));
(* math view handling *)
@@ -773,9 +835,153 @@ class gui () =
MatitaMathView.reset_font_size ();
MatitaMathView.update_font_sizes ());
MatitaMathView.reset_font_size ();
+
+ (** selections / clipboards handling *)
+
+ method markupSelected = MatitaMathView.has_selection ()
+ method private textSelected =
+ (source_buffer#get_iter_at_mark `INSERT)#compare
+ (source_buffer#get_iter_at_mark `SEL_BOUND) <> 0
+ method private somethingSelected = self#markupSelected || self#textSelected
+ method private markupStored = MatitaMathView.has_clipboard ()
+ method private textStored = clipboard#text <> None
+ method private somethingStored = self#markupStored || self#textStored
+
+ method canCopy = self#somethingSelected
+ method canCut = self#textSelected
+ method canDelete = self#textSelected
+ method canPaste = self#somethingStored
+ method canPastePattern = self#markupStored
+
+ method copy () =
+ if self#textSelected
+ then begin
+ MatitaMathView.empty_clipboard ();
+ source_view#buffer#copy_clipboard clipboard;
+ end else
+ MatitaMathView.copy_selection ()
+ method cut () =
+ source_view#buffer#cut_clipboard clipboard;
+ MatitaMathView.empty_clipboard ()
+ method delete () = ignore (source_view#buffer#delete_selection ())
+ method paste () =
+ if MatitaMathView.has_clipboard ()
+ then source_view#buffer#insert (MatitaMathView.paste_clipboard `Term)
+ else source_view#buffer#paste_clipboard clipboard;
+ (MatitaScript.current ())#clean_dirty_lock
+ 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 =
+ 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 *)
+(* let cmd =
+ let msg =
+ "External editor command:
+%f will be substitute for the script name,
+%p for the cursor position in bytes,
+%l for the execution point in bytes."
+ in
+ ask_text ~gui:self ~title:"External editor" ~msg ~multiline:false
+ ~default:(Helm_registry.get "matita.external_editor") ()
+ in *)
+ let fname = (MatitaScript.current ())#filename in
+ let slice mark =
+ source_buffer#start_iter#get_slice
+ ~stop:(source_buffer#get_iter_at_mark mark)
+ in
+ let script = MatitaScript.current () in
+ let locked = `MARK script#locked_mark in
+ let string_pos mark = string_of_int (String.length (slice mark)) in
+ let cursor_pos = string_pos `INSERT in
+ let locked_pos = string_pos locked in
+ let cmd =
+ Pcre.replace ~pat:"%f" ~templ:fname
+ (Pcre.replace ~pat:"%p" ~templ:cursor_pos
+ (Pcre.replace ~pat:"%l" ~templ:locked_pos
+ cmd))
+ in
+ let locked_before = slice locked in
+ let locked_offset = (source_buffer#get_iter_at_mark locked)#offset in
+ ignore (Unix.system cmd);
+ source_buffer#set_text (HExtlib.input_file fname);
+ let locked_iter = source_buffer#get_iter (`OFFSET locked_offset) in
+ source_buffer#move_mark locked locked_iter;
+ source_buffer#apply_tag script#locked_tag
+ ~start:source_buffer#start_iter ~stop:locked_iter;
+ let locked_after = slice locked in
+ let line = ref 0 in
+ let col = ref 0 in
+ try
+ for i = 0 to String.length locked_before - 1 do
+ if locked_before.[i] <> locked_after.[i] then begin
+ source_buffer#place_cursor
+ ~where:(source_buffer#get_iter (`LINEBYTE (!line, !col)));
+ script#goto `Cursor ();
+ raise Exit
+ end else if locked_before.[i] = '\n' then begin
+ incr line;
+ col := 0
+ end
+ done
+ with
+ | Exit -> ()
+ | Invalid_argument _ -> script#goto `Bottom ()
+
method loadScript file =
- let script = MatitaScript.instance () in
+ let script = MatitaScript.current () in
script#reset ();
script#assignFileName file;
let content =
@@ -825,8 +1031,8 @@ class gui () =
dialog#check_widgets ();
dialog
- method newInterpDialog () =
- let dialog = new interpChoiceDialog () in
+ method newRecordDialog () =
+ let dialog = new recordChoiceDialog () in
dialog#check_widgets ();
dialog
@@ -944,7 +1150,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 ->
@@ -1038,37 +1243,36 @@ class interpModel =
let interactive_interp_choice () choices =
let gui = instance () in
assert (choices <> []);
- let dialog = gui#newInterpDialog () in
- let model = new interpModel dialog#interpChoiceTreeView choices in
- let interp_len = List.length (List.hd choices) in
- dialog#interpChoiceDialog#set_title "Interpretation choice";
- dialog#interpChoiceDialogLabel#set_label "Choose an interpretation:";
+ let dialog = gui#newRecordDialog () in
+ let model = new interpModel dialog#recordChoiceTreeView choices in
+ dialog#recordChoiceDialog#set_title "Interpretation choice";
+ dialog#recordChoiceDialogLabel#set_label "Choose an interpretation:";
let interp_no = ref None in
let return _ =
- dialog#interpChoiceDialog#destroy ();
+ dialog#recordChoiceDialog#destroy ();
GMain.Main.quit ()
in
let fail _ = interp_no := None; return () in
- ignore (dialog#interpChoiceDialog#event#connect#delete (fun _ -> true));
- connect_button dialog#interpChoiceOkButton (fun _ ->
+ ignore (dialog#recordChoiceDialog#event#connect#delete (fun _ -> true));
+ connect_button dialog#recordChoiceOkButton (fun _ ->
match !interp_no with None -> () | Some _ -> return ());
- connect_button dialog#interpChoiceCancelButton fail;
- ignore (dialog#interpChoiceTreeView#connect#row_activated (fun path _ ->
+ connect_button dialog#recordChoiceCancelButton fail;
+ ignore (dialog#recordChoiceTreeView#connect#row_activated (fun path _ ->
interp_no := Some (model#get_interp_no path);
return ()));
- let selection = dialog#interpChoiceTreeView#selection in
+ let selection = dialog#recordChoiceTreeView#selection in
ignore (selection#connect#changed (fun _ ->
match selection#get_selected_rows with
| [path] -> interp_no := Some (model#get_interp_no path)
| _ -> assert false));
- dialog#interpChoiceDialog#show ();
+ dialog#recordChoiceDialog#show ();
GtkThread.main ();
(match !interp_no with Some row -> [row] | _ -> raise MatitaTypes.Cancel)
let _ =
(* disambiguator callbacks *)
- MatitaDisambiguator.set_choose_uris_callback (interactive_uri_choice ());
- MatitaDisambiguator.set_choose_interp_callback (interactive_interp_choice ());
+ GrafiteDisambiguator.set_choose_uris_callback (interactive_uri_choice ());
+ GrafiteDisambiguator.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;