class console ~(buffer: GText.buffer) () =
object (self)
val error_tag = buffer#create_tag [ `FOREGROUND "red" ]
- val warning_tag = buffer#create_tag [ `FOREGROUND "yellow" ]
+ 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
let main = new mainWin () in
let about = new aboutWin () in
let fileSel = new fileSelectionWin () in
+ let findRepl = new findReplWin () in
+ let develList = new develListWin () in
+ let newDevel = new newDevelopmentWin () in
let keyBindingBoxes = (* event boxes which should receive global key events *)
[ main#mainWinEventBox ]
in
object (self)
val mutable chosen_file = None
val mutable _ok_not_exists = false
+ val mutable _only_directory = false
val mutable script_fname = None
val mutable font_size = default_font_size
+ val mutable next_devel_must_contain = None
initializer
(* glade's check widgets *)
List.iter (fun w -> w#check_widgets ())
(let c w = (w :> <check_widgets: unit -> unit>) in
- [ c about; c fileSel; c main ]);
+ [ c about; c fileSel; c main; c findRepl]);
(* key bindings *)
List.iter (* global key bindings *)
(fun (key, callback) -> self#addKeyBinding key callback)
about#aboutWin#misc#hide ());
about#aboutLabel#set_label (Pcre.replace ~pat:"@VERSION@"
~templ:BuildTimeConf.version about#aboutLabel#label);
+ (* findRepl win *)
+ let show_find_Repl () =
+ findRepl#toplevel#misc#show ();
+ findRepl#toplevel#misc#grab_focus ()
+ in
+ let hide_find_Repl () = findRepl#toplevel#misc#hide () in
+ let find_forward _ =
+ let highlight start end_ =
+ source_buffer#move_mark `INSERT ~where:start;
+ source_buffer#move_mark `SEL_BOUND ~where:end_
+ in
+ let text = findRepl#findEntry#text in
+ let iter = source_buffer#get_iter `SEL_BOUND in
+ match iter#forward_search text with
+ | None ->
+ (match source_buffer#start_iter#forward_search text with
+ | None -> ()
+ | Some (start,end_) -> highlight start end_)
+ | Some (start,end_) -> highlight start end_
+ in
+ let replace _ =
+ let text = findRepl#replaceEntry#text in
+ let ins = source_buffer#get_iter `INSERT in
+ let sel = source_buffer#get_iter `SEL_BOUND in
+ if ins#compare sel < 0 then
+ begin
+ ignore(source_buffer#delete_selection ());
+ source_buffer#insert text
+ end
+ in
+ connect_button findRepl#findButton find_forward;
+ connect_button findRepl#findReplButton replace;
+ connect_button findRepl#cancelButton (fun _ -> hide_find_Repl ());
+ ignore(findRepl#toplevel#event#connect#delete
+ ~callback:(fun _ -> hide_find_Repl ();true));
+ ignore(self#main#findReplMenuItem#connect#activate
+ ~callback:show_find_Repl);
+ ignore (findRepl#findEntry#connect#activate ~callback:find_forward);
+ (* developments win *)
+ let model =
+ new MatitaGtkMisc.multiStringListModel
+ ~cols:2 develList#developmentsTreeview
+ in
+ let refresh_devels_win () =
+ model#list_store#clear ();
+ List.iter
+ (fun (name, root) -> model#easy_mappend [name;root])
+ (MatitamakeLib.list_known_developments ())
+ in
+ let get_devel_selected () =
+ match model#easy_mselection () with
+ | [[name;_]] -> MatitamakeLib.development_for_name name
+ | _ -> assert false
+ in
+ connect_button develList#newButton
+ (fun () ->
+ next_devel_must_contain <- None;
+ newDevel#toplevel#misc#show());
+ connect_button develList#deleteButton
+ (fun () ->
+ (match get_devel_selected () with
+ | None -> ()
+ | Some d -> MatitamakeLib.destroy_development d);
+ refresh_devels_win ());
+ let refresh () =
+ while Glib.Main.pending () do
+ ignore(Glib.Main.iteration false);
+ done
+ in
+ connect_button develList#buildButton
+ (fun () ->
+ match get_devel_selected () with
+ | None -> ()
+ | Some d -> ignore(MatitamakeLib.build_development_in_bg refresh d));
+ connect_button develList#cleanButton
+ (fun () ->
+ match get_devel_selected () with
+ | None -> ()
+ | Some d -> ignore(MatitamakeLib.clean_development_in_bg refresh d));
+ connect_button develList#closeButton
+ (fun () -> develList#toplevel#misc#hide());
+ ignore(develList#toplevel#event#connect#delete
+ (fun _ -> develList#toplevel#misc#hide();true));
+ let selected_devel = ref None in
+ connect_menu_item self#main#developmentsMenuItem
+ (fun () -> refresh_devels_win ();develList#toplevel#misc#show ());
+
+ (* add development win *)
+ let check_if_root_contains root =
+ match next_devel_must_contain with
+ | None -> true
+ | Some path ->
+ let is_prefix_of d1 d2 =
+ let len1 = String.length d1 in
+ let len2 = String.length d2 in
+ if len2 < len1 then
+ false
+ else
+ let pref = String.sub d2 0 len1 in
+ pref = d1
+ in
+ is_prefix_of root path
+ in
+ connect_button newDevel#addButton
+ (fun () ->
+ let name = newDevel#nameEntry#text in
+ let root = newDevel#rootEntry#text in
+ if check_if_root_contains root then
+ begin
+ ignore (MatitamakeLib.initialize_development name root);
+ refresh_devels_win ();
+ newDevel#nameEntry#set_text "";
+ newDevel#rootEntry#set_text "";
+ newDevel#toplevel#misc#hide()
+ end
+ else
+ MatitaLog.error ("The selected root does not contain " ^
+ match next_devel_must_contain with
+ | Some x -> x
+ | _ -> assert false));
+ connect_button newDevel#chooseRootButton
+ (fun () ->
+ let path = self#chooseDir () in
+ match path with
+ | Some path -> newDevel#rootEntry#set_text path
+ | None -> ());
+ connect_button newDevel#cancelButton
+ (fun () -> newDevel#toplevel#misc#hide ());
+ ignore(newDevel#toplevel#event#connect#delete
+ (fun _ -> newDevel#toplevel#misc#hide();true));
+
(* file selection win *)
ignore (fileSel#fileSelectionWin#event#connect#delete (fun _ -> true));
ignore (fileSel#fileSelectionWin#connect#response (fun event ->
| `OK ->
let fname = fileSel#fileSelectionWin#filename in
if Sys.file_exists fname then
- (if is_regular fname then return (Some fname))
+ begin
+ if is_regular fname && not(_only_directory) then
+ return (Some fname)
+ else if _only_directory && is_dir fname then
+ return (Some fname)
+ end
else
- (if _ok_not_exists then return (Some fname))
+ begin
+ if _ok_not_exists then
+ return (Some fname)
+ end
| `CANCEL -> return None
| `HELP -> ()
| `DELETE_EVENT -> return None));
main#helpMenu#set_right_justified true;
(* console *)
let adj = main#logScrolledWin#vadjustment in
- ignore (adj#connect#changed
+ 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 module A = GrafiteAst in
+ let hole = CicNotationPt.UserInput in
+ let loc = Disambiguate.dummy_floc in
let tac ast _ =
if (MatitaScript.instance ())#onGoingProof () then
(MatitaScript.instance ())#advance
- ~statement:("\n" ^ TacticAstPp.pp_tactical (A.Tactic (loc, ast))) ()
+ ~statement:("\n" ^ GrafiteAstPp.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)
+ ("\n" ^ GrafiteAstPp.pp_tactic ast)
in
let tbar = self#main in
connect_button tbar#introsButton (tac (A.Intros (loc, None, [])));
source_buffer#place_cursor
(source_buffer#get_iter_at_mark (`NAME "locked"))
in
+ let lock_world _ =
+ main#buttonsToolbar#misc#set_sensitive false;
+ source_view#set_editable false
+ in
+ let unlock_world _ =
+ main#buttonsToolbar#misc#set_sensitive true;
+ source_view#set_editable true
+ 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 locker f =
+ fun () ->
+ lock_world ();
+ try f ();unlock_world () with exc -> unlock_world (); raise exc
+ in
+ let advance = locker advance in
+ let retract = locker retract in
+ let top = locker top in
+ let bottom = locker bottom in
+ let jump = locker jump in
let connect_key sym f =
connect_key self#main#mainWinEventBox#event
~modifiers:[`CONTROL] ~stop:true sym f;
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
+ self#main#hpaneScriptSequent#set_position script_w;
+ (* source_view *)
+ ignore(source_view#connect#after#paste_clipboard
+ ~callback:(fun () -> (MatitaScript.instance ())#clean_dirty_lock))
method loadScript file =
let script = MatitaScript.instance () in
method sourceView: GSourceView.source_view = (source_view: GSourceView.source_view)
method about = about
method fileSel = fileSel
+ method findRepl = findRepl
method main = main
+ method develList = develList
+ method newDevel = newDevel
method newBrowserWin () =
object (self)
method chooseFile ?(ok_not_exists = false) () =
_ok_not_exists <- ok_not_exists;
+ _only_directory <- false;
fileSel#fileSelectionWin#show ();
GtkThread.main ();
chosen_file
+ method private chooseDir ?(ok_not_exists = false) () =
+ _ok_not_exists <- ok_not_exists;
+ _only_directory <- true;
+ fileSel#fileSelectionWin#show ();
+ GtkThread.main ();
+ (* we should check that this is a directory *)
+ chosen_file
+
+ method createDevelopment ~containing =
+ next_devel_must_contain <- containing;
+ newDevel#toplevel#misc#show()
+
method askText ?(title = "") ?(msg = "") () =
let dialog = new textDialog () in
dialog#textDialog#set_title title;
projects / helm.git / blobdiff