| `Warning -> self#warning (s ^ "\n")
end
-let clean_current_baseuri grafite_status =
- LibraryClean.clean_baseuris [grafite_status#baseuri]
+let clean_current_baseuri status =
+ LibraryClean.clean_baseuris [status#baseuri]
-let save_moo grafite_status =
+let save_moo status =
let script = MatitaScript.current () in
- let baseuri = grafite_status#baseuri in
+ let baseuri = status#baseuri in
match script#bos, script#eos with
| true, _ -> ()
| _, true ->
GrafiteTypes.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri)
- grafite_status
- | _ -> clean_current_baseuri grafite_status
+ status
+ | _ -> clean_current_baseuri status
;;
let ask_unsaved parent filename =
MatitaGtkMisc.toggle_callback ~check:main#ppNotationMenuItem
~callback:(function b ->
let s = s () in
- let status =
- Interpretations.toggle_active_interpretations s#grafite_status b
+ let status = Interpretations.toggle_active_interpretations s#status b
in
assert false (* MATITA 1.0 ???
s#set_grafite_status status*)
can we do? *)
notify_exn (MatitaScript.current ())#source_view exn
else raise exn);
- let disableSave () =
- (s())#assignFileName None;
- main#saveMenuItem#misc#set_sensitive false
- in
- let saveAsScript script =
- match self#chooseFile ~ok_not_exists:true () with
- | Some f ->
- HExtlib.touch f;
- script#assignFileName (Some f);
- script#saveToFile ();
- console#message ("'"^f^"' saved.\n");
- self#_enableSaveTo f
- | None -> ()
- in
- let saveScript script =
- if script#has_name then
- (script#saveToFile ();
- console#message ("'"^script#filename^"' saved.\n"))
- else saveAsScript script
- in
let loadScript () =
try
match self#chooseFile () with
MatitaScript.iter_scripts
(fun script ->
if not !cancel then
- if script#source_view#buffer#modified then
- match
- ask_unsaved main#toplevel (Filename.basename script#filename)
- with
- | `YES ->
- saveScript script;
- save_moo script#grafite_status
- | `NO -> ()
- | `CANCEL -> cancel := true
- else
- save_moo script#grafite_status);
+ if not (self#closeScript0 script) then
+ cancel := true);
if not !cancel then
GMain.Main.quit ());
connect_button main#scriptAdvanceButton advance;
connect_menu_item main#scriptJumpMenuItem jump;
connect_menu_item main#openMenuItem loadScript;
connect_menu_item main#saveMenuItem
- (fun () -> saveScript (MatitaScript.current ()));
+ (fun () -> self#saveScript (MatitaScript.current ()));
connect_menu_item main#saveAsMenuItem
- (fun () -> saveAsScript (MatitaScript.current ()));
- connect_menu_item main#newMenuItem self#newScript;
+ (fun () -> self#saveAsScript (MatitaScript.current ()));
+ 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
connect_menu_item main#normalFontSizeMenuItem
MatitaMisc.reset_font_size;
ignore (main#scriptNotebook#connect#switch_page
- (fun page -> (MatitaScript.at_page page)#activate));
+ (fun 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
| Exit -> ()
| Invalid_argument _ -> script#goto `Bottom ()
+ method private saveAsScript script =
+ match self#chooseFile ~ok_not_exists:true () with
+ | Some f ->
+ HExtlib.touch f;
+ script#assignFileName (Some f);
+ script#saveToFile ();
+ console#message ("'"^f^"' saved.\n");
+ self#_enableSaveTo f
+ | None -> ()
+
+ method private saveScript script =
+ if script#has_name then
+ (script#saveToFile ();
+ console#message ("'"^script#filename^"' saved.\n"))
+ else self#saveAsScript script
+
+ (* returns false if closure is aborted by the user *)
+ method private closeScript0 script =
+ if script#source_view#buffer#modified then
+ match
+ ask_unsaved main#toplevel (Filename.basename script#filename)
+ with
+ | `YES ->
+ self#saveScript script;
+ save_moo script#status;
+ true
+ | `NO -> true
+ | `CANCEL -> false
+ else
+ (save_moo script#status; true)
+
+ method private closeScript page script =
+ if self#closeScript0 script then
+ begin
+ MatitaScript.destroy page;
+ ignore (main#scriptNotebook#remove_page page)
+ end
+
+ method private closeCurrentScript () =
+ let page = main#scriptNotebook#current_page in
+ let script = MatitaScript.at_page page in
+ self#closeScript page script
+
method newScript () =
let scrolledWindow = GBin.scrolled_window () in
- let tab_label = GMisc.label ~text:"foo" () in
+ let hbox = GPack.hbox () 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
+ closebutton#set_image image#coerce;
let script =
MatitaScript.script
~urichooser:(fun source_view uris ->
~parent:(MatitaMisc.get_gui ())#main#toplevel ())
~parent:scrolledWindow ~tab_label ()
in
- ignore (main#scriptNotebook#prepend_page ~tab_label:tab_label#coerce scrolledWindow#coerce);
+ 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));
main#scriptNotebook#goto_page 0;
sequents_viewer#reset;
sequents_viewer#load_logo;
let browser_observer _ = MatitaMathView.refresh_all_browsers () in
- let sequents_observer grafite_status =
+ let sequents_observer status =
sequents_viewer#reset;
- match grafite_status#ng_mode with
+ match status#ng_mode with
`ProofMode ->
- sequents_viewer#nload_sequents grafite_status;
+ sequents_viewer#nload_sequents status;
(try
- script#setGoal
- (Some (Continuationals.Stack.find_goal grafite_status#stack));
let goal =
- match script#goal with
- None -> assert false
- | Some n -> n
+ Continuationals.Stack.find_goal status#stack
in
- sequents_viewer#goto_sequent grafite_status goal
- with Failure _ -> script#setGoal None);
+ sequents_viewer#goto_sequent status goal
+ with Failure _ -> ());
| `CommandMode -> sequents_viewer#load_logo
in
script#addObserver sequents_observer;
script#addObserver browser_observer
method loadScript file =
- self#newScript ();
+ let page = main#scriptNotebook#current_page in
+ let script = MatitaScript.at_page page in
+ if script#source_view#buffer#modified || script#has_name then
+ self#newScript ();
let script = MatitaScript.current () in
let source_view = script#source_view in
script#reset ();
method private _enableSaveTo file =
self#main#saveMenuItem#misc#set_sensitive true
- method console = console
- method fileSel = fileSel
- method findRepl = findRepl
+ method private console = console
+ method private fileSel = fileSel
+ method private findRepl = findRepl
method main = main
method newBrowserWin () =
dialog#check_widgets ();
dialog
- method newConfirmationDialog () =
+ method private newConfirmationDialog () =
let dialog = new confirmationDialog () in
dialog#check_widgets ();
dialog
List.iter (fun evbox -> add_key_binding key callback evbox)
keyBindingBoxes
- method setQuitCallback callback =
+ method private setQuitCallback callback =
connect_menu_item main#quitMenuItem callback;
ignore (main#toplevel#event#connect#delete
(fun _ -> callback ();true));
self#addKeyBinding GdkKeysyms._q callback
- method chooseFile ?(ok_not_exists = false) () =
+ method private chooseFile ?(ok_not_exists = false) () =
_ok_not_exists <- ok_not_exists;
_only_directory <- false;
fileSel#fileSelectionWin#show ();
(* we should check that this is a directory *)
chosen_file
- method askText ?(title = "") ?(msg = "") () =
- let dialog = new textDialog () in
- dialog#textDialog#set_title title;
- dialog#textDialogLabel#set_label msg;
- let text = ref None in
- let return v =
- text := v;
- dialog#textDialog#destroy ();
- GMain.Main.quit ()
- in
- ignore (dialog#textDialog#event#connect#delete (fun _ -> true));
- connect_button dialog#textDialogCancelButton (fun _ -> return None);
- connect_button dialog#textDialogOkButton (fun _ ->
- let text = dialog#textDialogTextView#buffer#get_text () in
- return (Some text));
- dialog#textDialog#show ();
- GtkThread.main ();
- !text
-
end
let gui () =
projects / helm.git / blobdiff