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" ]
object (self)
val mutable chosen_file = None
val mutable _ok_not_exists = false
-
+ val mutable script_fname = None
+
initializer
(* glade's check widgets *)
List.iter (fun w -> w#check_widgets ())
(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));
+ connect_button tbar#autoButton (tac (A.Auto (loc,None)));
(* quit *)
self#setQuitCallback (fun () -> exit 0);
(* log *)
(sprintf "Uncaught exception: %s" (Printexc.to_string exn)));
(* script *)
let s () = MatitaScript.instance () in
- let script_fname = ref None in
- let enable_save_to f =
- script_fname := Some f;
- self#main#saveMenuItem#misc#set_sensitive true
- in
- let disable_save () =
- script_fname := None;
+ 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; enable_save_to f
+ | Some f ->
+ script#reset ();
+ script#loadFrom f;
+ console#message ("'"^f^"' loaded.");
+ self#_enableSaveTo f
| None -> ()
in
let saveAsScript () =
let script = s () in
match self#chooseFile ~ok_not_exists:true () with
- | Some f -> script#saveTo f; enable_save_to f
+ | Some f ->
+ script#saveTo f;
+ console#message ("'"^f^"' saved.\n");
+ self#_enableSaveTo f
| None -> ()
in
let saveScript () =
- match !script_fname with
+ match script_fname with
| None -> saveAsScript ()
- | Some f -> (s ())#saveTo f
+ | Some f ->
+ (s ())#saveTo f;
+ console#message ("'"^f^"' saved.\n");
in
- let newScript () = (s ())#reset (); disable_save () in
+ let newScript () = (s ())#reset (); disableSave () in
let cursor () =
let buf = self#main#scriptTextView#buffer in
buf#place_cursor (buf#get_iter_at_mark (`NAME "locked"))
let buf = self#main#scriptTextView#buffer in
buf#insert ~iter:(buf#get_iter_at_mark `INSERT) "\n";
advance ());
+ (* script monospace font stuff *)
+ let font =
+ Helm_registry.get_opt_default Helm_registry.get
+ BuildTimeConf.default_script_font "matita.script_font"
+ in
+(* let monospace_tag =
+ self#main#scriptTextView#buffer#create_tag [`FONT_DESC font]
+ in *)
+ self#main#scriptTextView#misc#modify_font_by_name font;
+(* let _ =
+ self#main#scriptTextView#buffer#connect#changed ~callback:(fun _ ->
+ let start, stop = self#main#scriptTextView#buffer#bounds in
+ self#main#scriptTextView#buffer#apply_tag monospace_tag start stop)
+ in *)
(* debug menu *)
self#main#debugMenu#misc#hide ();
(* status bar *)
- self#main#hintLowImage#set_file "icons/matita-bulb-low.png";
- self#main#hintMediumImage#set_file "icons/matita-bulb-medium.png";
- self#main#hintHighImage#set_file "icons/matita-bulb-high.png";
+ 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#main#scriptTextView#misc#grab_focus ()
+ self#main#scriptTextView#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 / 2 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 console = console
method main = main
method newBrowserWin () =
- let win = new browserWin () in
- win#check_widgets ();
- win
+ object (self)
+ inherit browserWin ()
+ val combo = GEdit.combo_box_entry ()
+ initializer
+ self#check_widgets ();
+ let combo_widget = combo#coerce in
+ uriHBox#add combo_widget
+ method browserUri = combo
+ end
method newUriDialog () =
let dialog = new uriChoiceDialog () in
String.sub s (String.length s - 4) 4 = ".var"
with Invalid_argument _ -> false
+(* this is a shit and should be changed :-{ *)
let interactive_uri_choice
?(selection_mode:[`SINGLE|`MULTIPLE] = `MULTIPLE) ?(title = "")
- ?(msg = "") ?(nonvars_button = false) ()
+ ?(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
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 uris;
ignore (dialog#uriChoiceDialog#event#connect#delete (fun _ -> true));
connect_button dialog#uriChoiceConstantsButton (fun _ ->
return (Some (Lazy.force nonvars_uris)));
- connect_button dialog#uriChoiceAutoButton (fun _ ->
- Helm_registry.set_bool "matita.auto_disambiguation" true;
- 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 uris));
connect_button dialog#uriChoiceSelectedButton (fun _ ->
match model#easy_selection () with
| [] -> ()
projects / helm.git / blobdiff