(* Copyright (C) 2004-2005, HELM Team.
*
* This file is part of HELM, an Hypertextual, Electronic
* Library of Mathematics, developed at the Computer Science
* Department, University of Bologna, Italy.
*
* HELM is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License
* as published by the Free Software Foundation; either version 2
* of the License, or (at your option) any later version.
*
* HELM is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
* GNU General Public License for more details.
*
* You should have received a copy of the GNU General Public License
* along with HELM; if not, write to the Free Software
* Foundation, Inc., 59 Temple Place - Suite 330, Boston,
* MA 02111-1307, USA.
*
* For details, see the HELM World-Wide-Web page,
* http://helm.cs.unibo.it/
*)
open Printf
open MatitaGeneratedGui
open MatitaGtkMisc
open MatitaMisc
let gui_instance = ref None ;;
class type browserWin =
(* this class exists only because GEdit.combo_box_entry is not supported by
* lablgladecc :-(((( *)
object
inherit MatitaGeneratedGui.browserWin
method browserUri: GEdit.combo_box_entry
end
class console ~(buffer: GText.buffer) () =
object (self)
val error_tag = buffer#create_tag [ `FOREGROUND "red" ]
val warning_tag = buffer#create_tag [ `FOREGROUND "orange" ]
val message_tag = buffer#create_tag []
val debug_tag = buffer#create_tag [ `FOREGROUND "#888888" ]
method message s = buffer#insert ~iter:buffer#end_iter ~tags:[message_tag] s
method error s = buffer#insert ~iter:buffer#end_iter ~tags:[error_tag] s
method warning s = buffer#insert ~iter:buffer#end_iter ~tags:[warning_tag] s
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 =
match tag with
| `Debug -> self#debug (s ^ "\n")
| `Error -> self#error (s ^ "\n")
| `Message -> self#message (s ^ "\n")
| `Warning -> self#warning (s ^ "\n")
end
let clean_current_baseuri status =
try
let baseuri = MatitaTypes.get_string_option status "baseuri" in
MatitacleanLib.clean_baseuris [baseuri]
with MatitaTypes.Option_error _ -> ()
let ask_and_save_moo_if_needed parent fname status =
let save () =
MatitacLib.dump_moo_to_file fname status.MatitaTypes.moo_content_rev in
if (MatitaScript.instance ())#eos &&
status.MatitaTypes.proof_status = MatitaTypes.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?"
mooname fname)
~parent ()
in
let b =
match rc with
| `YES -> true
| `NO -> false
| `CANCEL -> raise MatitaTypes.Cancel
in
if b then
save ()
else
clean_current_baseuri status
end
else
clean_current_baseuri 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?")
()
class gui () =
(* creation order _is_ relevant for windows placement *)
let main = new mainWin () in
let about = new aboutWin () in
let fileSel = new fileSelectionWin () in
let keyBindingBoxes = (* event boxes which should receive global key events *)
[ main#mainWinEventBox ]
in
let console = new console ~buffer:main#logTextView#buffer () in
let (source_view: GSourceView.source_view) =
GSourceView.source_view
~auto_indent:true
~insert_spaces_instead_of_tabs:true ~tabs_width:2
~margin:80 ~show_margin:true
~smart_home_end:true
~packing:main#scriptScrolledWin#add
()
in
let default_font_size =
Helm_registry.get_opt_default Helm_registry.int
~default:BuildTimeConf.default_font_size "matita.font_size"
in
let source_buffer = source_view#source_buffer in
object (self)
val mutable chosen_file = None
val mutable _ok_not_exists = false
val mutable script_fname = None
val mutable font_size = default_font_size
initializer
(* glade's check widgets *)
List.iter (fun w -> w#check_widgets ())
(let c w = (w :> unit>) in
[ c about; c fileSel; c main ]);
(* key bindings *)
List.iter (* global key bindings *)
(fun (key, callback) -> self#addKeyBinding key callback)
(*
[ GdkKeysyms._F3,
toggle_win ~check:main#showProofMenuItem proof#proofWin;
GdkKeysyms._F4,
toggle_win ~check:main#showCheckMenuItem check#checkWin;
*)
[ ];
(* about win *)
ignore (about#aboutWin#event#connect#delete (fun _ -> true));
ignore (main#aboutMenuItem#connect#activate (fun _ ->
about#aboutWin#show ()));
connect_button about#aboutDismissButton (fun _ ->
about#aboutWin#misc#hide ());
about#aboutLabel#set_label (Pcre.replace ~pat:"@VERSION@"
~templ:BuildTimeConf.version about#aboutLabel#label);
(* file selection win *)
ignore (fileSel#fileSelectionWin#event#connect#delete (fun _ -> true));
ignore (fileSel#fileSelectionWin#connect#response (fun event ->
let return r =
chosen_file <- r;
fileSel#fileSelectionWin#misc#hide ();
GMain.Main.quit ()
in
match event with
| `OK ->
let fname = fileSel#fileSelectionWin#filename in
if Sys.file_exists fname then
(if is_regular fname then return (Some fname))
else
(if _ok_not_exists then return (Some fname))
| `CANCEL -> return None
| `HELP -> ()
| `DELETE_EVENT -> return None));
(* menus *)
List.iter (fun w -> w#misc#set_sensitive false) [ main#saveMenuItem ];
main#helpMenu#set_right_justified true;
(* console *)
let adj = main#logScrolledWin#vadjustment in
ignore (adj#connect#changed
(fun _ -> adj#set_value (adj#upper -. adj#page_size)));
console#message (sprintf "\tMatita version %s\n" BuildTimeConf.version);
(* toolbar *)
let module A = TacticAst in
let hole = CicAst.UserInput in
let loc = CicAst.dummy_floc in
let tac ast _ =
if (MatitaScript.instance ())#onGoingProof () then
(MatitaScript.instance ())#advance
~statement:("\n" ^ TacticAstPp.pp_tactical (A.Tactic (loc, ast))) ()
in
let tac_w_term ast _ =
if (MatitaScript.instance ())#onGoingProof () then
let buf = source_buffer in
buf#insert ~iter:(buf#get_iter_at_mark (`NAME "locked"))
("\n" ^ TacticAstPp.pp_tactic ast)
in
let tbar = self#main in
connect_button tbar#introsButton (tac (A.Intros (loc, None, [])));
connect_button tbar#applyButton (tac_w_term (A.Apply (loc, hole)));
connect_button tbar#exactButton (tac_w_term (A.Exact (loc, hole)));
connect_button tbar#elimButton (tac_w_term (A.Elim (loc, hole, None, None, [])));
connect_button tbar#elimTypeButton (tac_w_term (A.ElimType (loc, hole, None, None, [])));
connect_button tbar#splitButton (tac (A.Split loc));
connect_button tbar#leftButton (tac (A.Left loc));
connect_button tbar#rightButton (tac (A.Right loc));
connect_button tbar#existsButton (tac (A.Exists loc));
connect_button tbar#reflexivityButton (tac (A.Reflexivity loc));
connect_button tbar#symmetryButton (tac (A.Symmetry loc));
connect_button tbar#transitivityButton
(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)));
MatitaGtkMisc.toggle_widget_visibility
~widget:(self#main#tacticsButtonsHandlebox :> GObj.widget)
~check:self#main#tacticsBarMenuItem;
let module Hr = Helm_registry in
if
not (Hr.get_opt_default Hr.bool ~default:false "matita.tactics_bar")
then
self#main#tacticsBarMenuItem#set_active false;
MatitaGtkMisc.toggle_callback
~callback:(function
| true -> self#main#toplevel#fullscreen ()
| false -> self#main#toplevel#unfullscreen ())
~check:self#main#fullscreenMenuItem;
self#main#fullscreenMenuItem#set_active false;
(* log *)
MatitaLog.set_log_callback self#console#log_callback;
GtkSignal.user_handler :=
(fun exn -> MatitaLog.error (MatitaExcPp.to_string exn));
(* script *)
let _ =
match GSourceView.source_language_from_file BuildTimeConf.lang_file with
| None ->
MatitaLog.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 disableSave () =
script_fname <- None;
self#main#saveMenuItem#misc#set_sensitive false
in
let saveAsScript () =
let script = s () in
match self#chooseFile ~ok_not_exists:true () with
| Some f ->
script#assignFileName f;
script#saveToFile ();
console#message ("'"^f^"' saved.\n");
self#_enableSaveTo f
| None -> ()
in
let saveScript () =
match script_fname with
| None -> saveAsScript ()
| Some f ->
(s ())#assignFileName f;
(s ())#saveToFile ();
console#message ("'"^f^"' saved.\n");
in
let loadScript () =
let script = s () in
let status = script#status in
try
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);
match self#chooseFile () with
| Some f ->
script#reset ();
script#assignFileName f;
script#loadFromFile ();
console#message ("'"^f^"' loaded.\n");
self#_enableSaveTo f
| None -> ()
with MatitaTypes.Cancel -> ()
in
let newScript () =
(s ())#reset ();
(s ())#template ();
disableSave ();
script_fname <- None
in
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 connect_key sym f =
connect_key self#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
if source_view#buffer#modified then
begin
let rc = ask_unsaved main#toplevel in
try
match rc with
| `YES -> saveScript ();
if not source_view#buffer#modified then
begin
(match script_fname with
| None -> ()
| Some fname ->
ask_and_save_moo_if_needed
main#toplevel fname status);
GMain.Main.quit ()
end
| `NO -> GMain.Main.quit ()
| `CANCEL -> raise MatitaTypes.Cancel
with MatitaTypes.Cancel -> ()
end
else
begin
(match script_fname with
| None -> clean_current_baseuri status; GMain.Main.quit ()
| Some fname ->
try
ask_and_save_moo_if_needed main#toplevel fname status;
GMain.Main.quit ()
with MatitaTypes.Cancel -> ())
end);
connect_button self#main#scriptAdvanceButton advance;
connect_button self#main#scriptRetractButton retract;
connect_button self#main#scriptTopButton top;
connect_button self#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 self#main#scriptJumpButton jump;
connect_menu_item self#main#openMenuItem loadScript;
connect_menu_item self#main#saveMenuItem saveScript;
connect_menu_item self#main#saveAsMenuItem saveAsScript;
connect_menu_item self#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 *)
self#main#debugMenu#misc#hide ();
(* status bar *)
self#main#hintLowImage#set_file (image_path "matita-bulb-low.png");
self#main#hintMediumImage#set_file (image_path "matita-bulb-medium.png");
self#main#hintHighImage#set_file (image_path "matita-bulb-high.png");
(* focus *)
self#sourceView#misc#grab_focus ();
(* main win dimension *)
let width = Gdk.Screen.width () in
let height = Gdk.Screen.height () in
let main_w = width * 90 / 100 in
let main_h = height * 80 / 100 in
let script_w = main_w * 6 / 10 in
self#main#toplevel#resize ~width:main_w ~height:main_h;
self#main#hpaneScriptSequent#set_position script_w
method loadScript file =
let script = MatitaScript.instance () in
script#reset ();
script#assignFileName file;
if not (Sys.file_exists file) then
begin
let oc = open_out file in
let template = MatitaMisc.input_file BuildTimeConf.script_template in
output_string oc template;
close_out oc
end;
script#loadFromFile ();
console#message ("'"^file^"' loaded.");
self#_enableSaveTo file
method setStar name b =
let l = main#scriptLabel in
if b then
l#set_text (name ^ " *")
else
l#set_text (name)
method private _enableSaveTo file =
script_fname <- Some file;
self#main#saveMenuItem#misc#set_sensitive true
method console = console
method sourceView: GSourceView.source_view = (source_view: GSourceView.source_view)
method about = about
method fileSel = fileSel
method main = main
method newBrowserWin () =
object (self)
inherit browserWin ()
val combo = GEdit.combo_box_entry ()
initializer
self#check_widgets ();
let combo_widget = combo#coerce in
uriHBox#pack ~from:`END ~fill:true ~expand:true combo_widget;
combo#entry#misc#grab_focus ()
method browserUri = combo
end
method newUriDialog () =
let dialog = new uriChoiceDialog () in
dialog#check_widgets ();
dialog
method newInterpDialog () =
let dialog = new interpChoiceDialog () in
dialog#check_widgets ();
dialog
method newConfirmationDialog () =
let dialog = new confirmationDialog () in
dialog#check_widgets ();
dialog
method newEmptyDialog () =
let dialog = new emptyDialog () in
dialog#check_widgets ();
dialog
method private addKeyBinding key callback =
List.iter (fun evbox -> add_key_binding key callback evbox)
keyBindingBoxes
method setQuitCallback callback =
ignore (main#quitMenuItem#connect#activate callback);
ignore (main#toplevel#event#connect#delete
(fun _ -> callback ();true));
self#addKeyBinding GdkKeysyms._q callback
method chooseFile ?(ok_not_exists = false) () =
_ok_not_exists <- ok_not_exists;
fileSel#fileSelectionWin#show ();
GtkThread.main ();
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
method private updateFontSize () =
self#sourceView#misc#modify_font_by_name
(sprintf "%s %d" BuildTimeConf.script_font font_size)
method increaseFontSize () =
font_size <- font_size + 1;
self#updateFontSize ()
method decreaseFontSize () =
font_size <- font_size - 1;
self#updateFontSize ()
method resetFontSize () =
font_size <- default_font_size;
self#updateFontSize ()
end
let gui () =
let g = new gui () in
gui_instance := Some g;
g
let instance = singleton gui
let non p x = not (p x)
(* this is a shit and should be changed :-{ *)
let interactive_uri_choice
?(selection_mode:[`SINGLE|`MULTIPLE] = `MULTIPLE) ?(title = "")
?(msg = "") ?(nonvars_button = false) ?(hide_uri_entry=false)
?(hide_try=false) ?(ok_label="_Auto") ?(ok_action:[`SELECT|`AUTO] = `AUTO)
?copy_cb ()
~id uris
=
let gui = instance () in
let nonvars_uris = lazy (List.filter (non UriManager.uri_is_var) uris) in
if (selection_mode <> `SINGLE) &&
(Helm_registry.get_bool "matita.auto_disambiguation")
then
Lazy.force nonvars_uris
else begin
let dialog = gui#newUriDialog () in
if hide_uri_entry then
dialog#uriEntryHBox#misc#hide ();
if hide_try then
begin
dialog#uriChoiceSelectedButton#misc#hide ();
dialog#uriChoiceConstantsButton#misc#hide ();
end;
dialog#okLabel#set_label ok_label;
dialog#uriChoiceTreeView#selection#set_mode
(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 ->
dialog#copyButton#misc#show ();
connect_button dialog#copyButton
(fun _ ->
match model#easy_selection () with
| [u] -> (cb u)
| _ -> ()));
dialog#uriChoiceDialog#set_title title;
dialog#uriChoiceLabel#set_text msg;
List.iter model#easy_append (List.map UriManager.string_of_uri uris);
dialog#uriChoiceConstantsButton#misc#set_sensitive nonvars_button;
let return v =
choices := v;
dialog#uriChoiceDialog#destroy ();
GMain.Main.quit ()
in
ignore (dialog#uriChoiceDialog#event#connect#delete (fun _ -> true));
connect_button dialog#uriChoiceConstantsButton (fun _ ->
return (Some (Lazy.force nonvars_uris)));
if ok_action = `AUTO then
connect_button dialog#uriChoiceAutoButton (fun _ ->
Helm_registry.set_bool "matita.auto_disambiguation" true;
return (Some (Lazy.force nonvars_uris)))
else
connect_button dialog#uriChoiceAutoButton (fun _ ->
match model#easy_selection () with
| [] -> ()
| uris -> return (Some (List.map UriManager.uri_of_string uris)));
connect_button dialog#uriChoiceSelectedButton (fun _ ->
match model#easy_selection () with
| [] -> ()
| uris -> return (Some (List.map UriManager.uri_of_string uris)));
connect_button dialog#uriChoiceAbortButton (fun _ -> return None);
dialog#uriChoiceDialog#show ();
GtkThread.main ();
(match !choices with
| None -> raise MatitaTypes.Cancel
| Some uris -> uris)
end
class interpModel =
let cols = new GTree.column_list in
let id_col = cols#add Gobject.Data.string in
let dsc_col = cols#add Gobject.Data.string in
let interp_no_col = cols#add Gobject.Data.int in
let tree_store = GTree.tree_store cols in
let id_renderer = GTree.cell_renderer_text [], ["text", id_col] in
let dsc_renderer = GTree.cell_renderer_text [], ["text", dsc_col] in
let id_view_col = GTree.view_column ~renderer:id_renderer () in
let dsc_view_col = GTree.view_column ~renderer:dsc_renderer () in
fun tree_view choices ->
object
initializer
tree_view#set_model (Some (tree_store :> GTree.model));
ignore (tree_view#append_column id_view_col);
ignore (tree_view#append_column dsc_view_col);
let name_of_interp =
(* try to find a reasonable name for an interpretation *)
let idx = ref 0 in
fun interp ->
try
List.assoc "0" interp
with Not_found ->
incr idx; string_of_int !idx
in
tree_store#clear ();
let idx = ref ~-1 in
List.iter
(fun interp ->
incr idx;
let interp_row = tree_store#append () in
tree_store#set ~row:interp_row ~column:id_col
(name_of_interp interp);
tree_store#set ~row:interp_row ~column:interp_no_col !idx;
List.iter
(fun (id, dsc) ->
let row = tree_store#append ~parent:interp_row () in
tree_store#set ~row ~column:id_col id;
tree_store#set ~row ~column:dsc_col dsc;
tree_store#set ~row ~column:interp_no_col !idx)
interp)
choices
method get_interp_no tree_path =
let iter = tree_store#get_iter tree_path in
tree_store#get ~row:iter ~column:interp_no_col
end
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 interp_no = ref None in
let return _ =
dialog#interpChoiceDialog#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 _ ->
match !interp_no with None -> () | Some _ -> return ());
connect_button dialog#interpChoiceCancelButton fail;
ignore (dialog#interpChoiceTreeView#connect#row_activated (fun path _ ->
interp_no := Some (model#get_interp_no path);
return ()));
let selection = dialog#interpChoiceTreeView#selection in
ignore (selection#connect#changed (fun _ ->
match selection#get_selected_rows with
| [path] ->
MatitaLog.debug (sprintf "selection: %d" (model#get_interp_no path));
interp_no := Some (model#get_interp_no path)
| _ -> assert false));
dialog#interpChoiceDialog#show ();
GtkThread.main ();
(match !interp_no with Some row -> [row] | _ -> raise MatitaTypes.Cancel)