X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaGui.ml;h=ed739eefbebb8c9be4a9e5ab95f919166625a722;hb=771ee8b9d122fa963881c876e86f90531bb7434f;hp=e4c1072425026c00b3889048fe0d61dddfd66635;hpb=0ac236dda6f80f6dc86a7f12d8c88b25e64e3251;p=helm.git
diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index e4c107242..ed739eefb 100644
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -23,6 +23,8 @@
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open Printf
open MatitaGeneratedGui
@@ -61,30 +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
+ let baseuri = GrafiteTypes.get_string_option grafite_status "baseuri" in
let basedir = Helm_registry.get "matita.basedir" in
LibraryClean.clean_baseuris ~basedir [baseuri]
- with MatitaTypes.Option_error _ -> ()
+ 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 ~basedir fname in
+ 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
- status.MatitaTypes.moo_content_rev in
+ 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 &&
- status.MatitaTypes.proof_status = MatitaTypes.No_proof
+ grafite_status.GrafiteTypes.proof_status = GrafiteTypes.No_proof
then
begin
- let mooname = MatitaMisc.obj_file_of_script ~basedir 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 =
@@ -94,12 +106,12 @@ 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
@@ -108,6 +120,16 @@ let ask_unsaved parent =
"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
@@ -141,6 +163,8 @@ class gui () =
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 *)
@@ -308,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 ())
@@ -330,35 +378,18 @@ 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.current ())#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);
@@ -523,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.current ())#onGoingProof () then
(MatitaScript.current ())#advance
- ~statement:("\n" ^ GrafiteAstPp.pp_tactical (A.Tactic (loc, ast)))
+ ~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.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, [])));
@@ -572,7 +607,9 @@ class gui () =
(* log *)
HLog.set_log_callback self#console#log_callback;
GtkSignal.user_handler :=
- (fun exn ->
+ (function
+ | MatitaScript.ActionCancelled -> ()
+ | exn ->
if not (Helm_registry.get_bool "matita.debug") then
let floc, msg = MatitaExcPp.to_string exn in
begin
@@ -639,7 +676,8 @@ class gui () =
console#message ("'"^f^"' saved.\n");
in
let abandon_script () =
- let status = (s ())#status in
+ 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 ()
@@ -647,7 +685,9 @@ class gui () =
| `CANCEL -> raise MatitaTypes.Cancel);
(match script_fname with
| None -> ()
- | Some fname -> ask_and_save_moo_if_needed main#toplevel fname status);
+ | Some fname ->
+ ask_and_save_moo_if_needed main#toplevel fname
+ lexicon_status grafite_status);
in
let loadScript () =
let script = s () in
@@ -687,15 +727,10 @@ class gui () =
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.current ())#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
@@ -707,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 ()
@@ -718,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);
@@ -799,6 +835,42 @@ 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
@@ -1199,8 +1271,8 @@ let interactive_interp_choice () choices =
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;