let clean_current_baseuri status =
LibraryClean.clean_baseuris [status#baseuri]
-let save_moo status =
- let script = MatitaScript.current () in
+let save_moo0 ~do_clean script status =
let baseuri = status#baseuri in
match script#bos, script#eos with
| true, _ -> ()
| _, true ->
GrafiteTypes.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri)
status
- | _ -> clean_current_baseuri status
+ | _ -> if do_clean then clean_current_baseuri status
+;;
+
+let save_moo status =
+ let script = MatitaScript.current () in
+ save_moo0 ~do_clean:true script status
;;
let ask_unsaved parent filename =
val mutable chosen_file = None
val mutable _ok_not_exists = false
val mutable _only_directory = false
+ val mutable current_page = -1
initializer
let s () = MatitaScript.current () in
(* key bindings *)
List.iter (* global key bindings *)
- (fun (key, callback) -> self#addKeyBinding key callback)
+ (fun (key, modifiers, callback) ->
+ self#addKeyBinding key ~modifiers callback)
(*
[ GdkKeysyms._F3,
toggle_win ~check:main#showProofMenuItem proof#proofWin;
GdkKeysyms._F4,
toggle_win ~check:main#showCheckMenuItem check#checkWin;
*)
- [ ];
+ [
+ GdkKeysyms._Page_Down, [`CONTROL], main#scriptNotebook#next_page;
+ GdkKeysyms._Page_Up, [`CONTROL], main#scriptNotebook#previous_page
+ ];
(* about win *)
let parse_txt_file file =
let ch = open_in (BuildTimeConf.runtime_base_dir ^ "/" ^ file) in
MatitaGtkMisc.toggle_callback ~check:main#ppNotationMenuItem
~callback:(function b ->
let s = s () in
- let status = Interpretations.toggle_active_interpretations s#status b
+ let _status = Interpretations.toggle_active_interpretations s#status b
in
assert false (* MATITA 1.0 ???
s#set_grafite_status status*)
main#unicodeAsTexMenuItem#set_active
(Helm_registry.get_bool "matita.paste_unicode_as_tex");
(* log *)
- HLog.set_log_callback self#console#log_callback;
+ HLog.set_log_callback (fun tag msg -> GtkThread.async (self#console#log_callback tag) msg);
GtkSignal.user_handler :=
(function
| MatitaScript.ActionCancelled s -> HLog.error s
MatitaMisc.decrease_font_size;
connect_menu_item main#normalFontSizeMenuItem
MatitaMisc.reset_font_size;
- ignore (main#scriptNotebook#connect#switch_page
- (fun page ->
- let script = MatitaScript.at_page page in
- script#activate;
- main#saveMenuItem#misc#set_sensitive script#has_name))
+ ignore (main#scriptNotebook#connect#switch_page (fun page ->
+ self#save_page ();
+ current_page <- page;
+ let script = MatitaScript.at_page page in
+ script#activate;
+ main#saveMenuItem#misc#set_sensitive script#has_name))
method private externalEditor () =
let script = MatitaScript.current () in
let script = MatitaScript.at_page page in
self#closeScript page script
+ method private save_page () =
+ if current_page >= 0 then
+ let old_script = MatitaScript.at_page current_page in
+ save_moo0 ~do_clean:false old_script old_script#status
+
method newScript () =
+ self#save_page ();
let scrolledWindow = GBin.scrolled_window () in
let hbox = GPack.hbox () in
let tab_label = GMisc.label ~text:"foo" ~packing:hbox#pack () in
method private findRepl = findRepl
method main = main
- method private addKeyBinding key callback =
- List.iter (fun evbox -> add_key_binding key callback evbox)
+ method private addKeyBinding key ?modifiers callback =
+(* List.iter (fun evbox -> add_key_binding key callback evbox) *)
+ List.iter (fun evbox -> connect_key evbox#event key ?modifiers callback)
keyBindingBoxes
method private setQuitCallback callback =