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
match !id with
| None -> assert false (* a race condition occurred *)
| Some id ->
- (new GObj.gobject_ops source_view#source_buffer#as_buffer)#disconnect id));
+ source_view#source_buffer#misc#disconnect id));
source_view#source_buffer#place_cursor
(source_view#source_buffer#get_iter (`OFFSET x'));
end;
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
connect_menu_item main#newMenuItem self#newScript;
connect_menu_item main#closeMenuItem self#closeCurrentScript;
connect_menu_item main#showCoercionsGraphMenuItem
- (fun _ ->
- let c = MatitaMathView.cicBrowser () in
- c#load (`About `Coercions));
+ (fun _ -> MatitaMathView.cicBrowser (Some (`About `Coercions)));
connect_menu_item main#showHintsDbMenuItem
- (fun _ ->
- let c = MatitaMathView.cicBrowser () in
- c#load (`About `Hints));
+ (fun _ -> MatitaMathView.cicBrowser (Some (`About `Hints)));
connect_menu_item main#showTermGrammarMenuItem
- (fun _ ->
- let c = MatitaMathView.cicBrowser () in
- c#load (`About `Grammar));
+ (fun _ -> MatitaMathView.cicBrowser (Some (`About `Grammar)));
connect_menu_item main#showUnicodeTable
- (fun _ ->
- let c = MatitaMathView.cicBrowser () in
- c#load (`About `TeX));
+ (fun _ -> MatitaMathView.cicBrowser (Some (`About `TeX)));
(* debug menu *)
main#debugMenu#misc#hide ();
(* HBUGS *)
main#hpaneScriptSequent#set_position script_w;
(* math view handling *)
connect_menu_item main#newCicBrowserMenuItem (fun () ->
- ignore(MatitaMathView.cicBrowser ()));
+ ignore(MatitaMathView.cicBrowser None));
connect_menu_item main#increaseFontSizeMenuItem
MatitaMisc.increase_font_size;
connect_menu_item main#decreaseFontSizeMenuItem
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));
- self#newScript ()
+ 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 newScript () =
+ 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
+ let tab_label = GMisc.label ~text:"foo" ~packing:hbox#pack () in
let _ =
GMisc.label ~text:"" ~packing:(hbox#pack ~expand:true ~fill:true) () in
let closebutton =
GButton.button ~relief:`NONE ~packing:hbox#pack () in
- let image =
- GMisc.image ~stock:`CLOSE ~icon_size:`MENU () in
+ let image = GMisc.image ~stock:`CLOSE ~icon_size:`MENU () in
closebutton#set_image image#coerce;
let script = MatitaScript.script ~parent:scrolledWindow ~tab_label () in
ignore (main#scriptNotebook#prepend_page ~tab_label:hbox#coerce
scrolledWindow#coerce);
ignore (closebutton#connect#clicked (fun () ->
- self#closeScript (main#scriptNotebook#page_num hbox#coerce) script));
+ self#closeScript
+ (main#scriptNotebook#page_num scrolledWindow#coerce) script));
main#scriptNotebook#goto_page 0;
sequents_viewer#reset;
sequents_viewer#load_logo;
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 =
let gui () =
let g = new gui () in
- MatitaMisc.set_gui g;
- g
+ let rg = (g :> MatitaGuiTypes.gui) in
+ MatitaMisc.set_gui rg;
+ g#newScript ();
+ rg
let instance = singleton gui
projects / helm.git / blobdiff