X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaGui.ml;h=8eec3244d29915ff57768b0acb1f0de7961c2cc4;hb=842919f2f8ee71a5301ad962220569450340a9e9;hp=e3652a2648c7257ba5e6ecde90d7a2b5b8f17054;hpb=1fa0472bfe2ed04c7adf166fa48df687f0022226;p=helm.git diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index e3652a264..8eec3244d 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -1,4 +1,4 @@ -(* Copyright (C) 2004, HELM Team. +(* Copyright (C) 2004-2005, HELM Team. * * This file is part of HELM, an Hypertextual, Electronic * Library of Mathematics, developed at the Computer Science @@ -23,99 +23,320 @@ * http://helm.cs.unibo.it/ *) -(* -class stringListModel' uriChoiceDialog = - let tree_view = uriChoiceDialog#uriChoiceTreeView in - let column_list = new GTree.column_list in - let text_column = column_list#add Gobject.Data.string in - let list_store = GTree.list_store column_list in - let renderer = (GTree.cell_renderer_text [], ["text", text_column]) in - let view_column = GTree.view_column ~renderer () in - let _ = tree_view#set_model (Some (list_store :> GTree.model)) in - let _ = tree_view#append_column view_column in - object - method append s = - let tree_iter = list_store#append () in - list_store#set ~row:tree_iter ~column:text_column s - method clear () = list_store#clear () - end -*) - 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 "yellow" ] + 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 -class gui file = +class gui () = (* creation order _is_ relevant for windows placement *) - let toolbar = new toolBarWin ~file () in - let main = new mainWin ~file () in - let about = new aboutWin ~file () in - let fileSel = new fileSelectionWin ~file () in - let proof = new proofWin ~file () in + 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 *) - [ toolbar#toolBarEventBox; proof#proofWinEventBox; main#mainWinEventBox ] + [ main#mainWinEventBox ] in - let console = - MatitaConsole.console ~evbox:main#consoleEventBox - ~packing:main#scrolledConsole#add () + 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; c proof; c toolbar ]); - (* show/hide commands *) - toggle_visibility toolbar#toolBarWin main#showToolBarMenuItem; - toggle_visibility proof#proofWin main#showProofMenuItem; - (* "global" key bindings *) - List.iter (fun (key, callback) -> self#addKeyBinding key callback) + [ 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 ())); - ignore (about#aboutDismissButton#connect#clicked (fun _ -> - about#aboutWin#misc#hide ())); + 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#saveAsMenuItem ]; + List.iter (fun w -> w#misc#set_sensitive false) [ main#saveMenuItem ]; main#helpMenu#set_right_justified true; (* console *) - console#echo_message (sprintf "\tMatita version %s\n" - BuildTimeConf.version); - console#echo_prompt (); - console#misc#grab_focus () + 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))); + connect_button tbar#elimTypeButton (tac_w_term (A.ElimType (loc, hole))); + 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, 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; + (* quit *) + self#setQuitCallback (fun () -> exit 0); + (* log *) + MatitaLog.set_log_callback self#console#log_callback; + GtkSignal.user_handler := + (fun exn -> + MatitaLog.error + (sprintf "Uncaught exception: %s" (Printexc.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 loadScript () = + let script = s () in + match self#chooseFile () with + | Some f -> + script#reset (); + script#loadFrom f; + console#message ("'"^f^"' loaded.\n"); + self#_enableSaveTo f + | None -> () + in + let saveAsScript () = + let script = s () in + match self#chooseFile ~ok_not_exists:true () with + | Some f -> + script#saveTo f; + console#message ("'"^f^"' saved.\n"); + self#_enableSaveTo f + | None -> () + in + let saveScript () = + match script_fname with + | None -> saveAsScript () + | Some f -> + (s ())#saveTo f; + console#message ("'"^f^"' saved.\n"); + in + let newScript () = (s ())#reset (); disableSave () 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 + 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#loadFrom file; + console#message ("'"^file^"' loaded."); + self#_enableSaveTo file + + method private _enableSaveTo file = + script_fname <- Some file; + self#main#saveMenuItem#misc#set_sensitive true + - method about = about method console = console + method sourceView: GSourceView.source_view = (source_view: GSourceView.source_view) + method about = about method fileSel = fileSel method main = main - method proof = proof - method toolbar = toolbar + + 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 ~file () in + let dialog = new uriChoiceDialog () in dialog#check_widgets (); dialog method newInterpDialog () = - let dialog = new interpChoiceDialog ~file () in + let dialog = new interpChoiceDialog () in dialog#check_widgets (); dialog method newConfirmationDialog () = - let dialog = new confirmationDialog ~file () in + let dialog = new confirmationDialog () in dialog#check_widgets (); dialog method newEmptyDialog () = - let dialog = new emptyDialog ~file () in + let dialog = new emptyDialog () in dialog#check_widgets (); dialog @@ -128,7 +349,206 @@ class gui file = ignore (main#quitMenuItem#connect#activate callback); self#addKeyBinding GdkKeysyms._q callback - method setPhraseCallback = console#set_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) +