let all_disambiguation_passes = ref false
-let gui_instance = ref None
-
(* this is a shit and should be changed :-{ *)
let interactive_uri_choice
?(selection_mode:[`SINGLE|`MULTIPLE] = `MULTIPLE) ?(title = "")
?copy_cb ()
~id uris
=
- let gui = MatitaMisc.get_gui () in
if (selection_mode <> `SINGLE) &&
(Helm_registry.get_opt_default Helm_registry.get_bool ~default:true "matita.auto_disambiguation")
then
uris
else begin
- let dialog = gui#newUriDialog () in
+ let dialog = new uriChoiceDialog () in
if hide_uri_entry then
dialog#uriEntryHBox#misc#hide ();
if hide_try then
end
-class type browserWin =
- (* this class exists only because GEdit.combo_box_entry is not supported by
- * lablgladecc :-(((( *)
-object
- inherit MatitaGeneratedGui.browserWin
- method browserUri: GEdit.entry
-end
-
class console ~(buffer: GText.buffer) () =
object (self)
val error_tag = buffer#create_tag [ `FOREGROUND "red" ]
let clean_current_baseuri status =
LibraryClean.clean_baseuris [status#baseuri]
-let save_moo status =
- let script = MatitaScript.current () in
+let save_moo0 ~do_clean script status =
let baseuri = status#baseuri in
match script#bos, script#eos with
| true, _ -> ()
| _, true ->
GrafiteTypes.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri)
status
- | _ -> clean_current_baseuri status
+ | _ -> if do_clean then clean_current_baseuri status
+;;
+
+let save_moo status =
+ let script = MatitaScript.current () in
+ save_moo0 ~do_clean:true script status
;;
let ask_unsaved parent filename =
(offset,[[env,diff,lazy (loffset,Lazy.force msg),significant]]));
| _::_ ->
let dialog = new disambiguationErrors () in
- dialog#check_widgets ();
if all_passes then
dialog#disambiguationErrorsMoreErrors#misc#set_sensitive false;
let model = new interpErrorModel dialog#treeview choices in
val mutable chosen_file = None
val mutable _ok_not_exists = false
val mutable _only_directory = false
+ val mutable current_page = -1
initializer
let s () = MatitaScript.current () in
- (* glade's check widgets *)
- List.iter (fun w -> w#check_widgets ())
- (let c w = (w :> <check_widgets: unit -> unit>) in
- [ c fileSel; c main; c findRepl]);
(* key bindings *)
List.iter (* global key bindings *)
- (fun (key, callback) -> self#addKeyBinding key callback)
+ (fun (key, modifiers, callback) ->
+ self#addKeyBinding key ~modifiers callback)
(*
[ GdkKeysyms._F3,
toggle_win ~check:main#showProofMenuItem proof#proofWin;
GdkKeysyms._F4,
toggle_win ~check:main#showCheckMenuItem check#checkWin;
*)
- [ ];
+ [
+ GdkKeysyms._Page_Down, [`CONTROL], main#scriptNotebook#next_page;
+ GdkKeysyms._Page_Up, [`CONTROL], main#scriptNotebook#previous_page
+ ];
(* about win *)
let parse_txt_file file =
let ch = open_in (BuildTimeConf.runtime_base_dir ^ "/" ^ file) in
match !id with
| None -> assert false (* a race condition occurred *)
| Some id ->
- (new GObj.gobject_ops source_view#source_buffer#as_buffer)#disconnect id));
+ source_view#source_buffer#misc#disconnect id));
source_view#source_buffer#place_cursor
(source_view#source_buffer#get_iter (`OFFSET x'));
end;
MatitaGtkMisc.toggle_callback ~check:main#ppNotationMenuItem
~callback:(function b ->
let s = s () in
- let status = Interpretations.toggle_active_interpretations s#status b
+ let _status = Interpretations.toggle_active_interpretations s#status b
in
assert false (* MATITA 1.0 ???
s#set_grafite_status status*)
main#unicodeAsTexMenuItem#set_active
(Helm_registry.get_bool "matita.paste_unicode_as_tex");
(* log *)
- HLog.set_log_callback self#console#log_callback;
+ HLog.set_log_callback (fun tag msg -> GtkThread.async (self#console#log_callback tag) msg);
GtkSignal.user_handler :=
(function
| MatitaScript.ActionCancelled s -> HLog.error s
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
- c#load (`About `Coercions));
+ (fun _ -> MatitaMathView.cicBrowser (Some (`About `Coercions)));
connect_menu_item main#showHintsDbMenuItem
- (fun _ ->
- let c = MatitaMathView.cicBrowser () in
- c#load (`About `Hints));
+ (fun _ -> MatitaMathView.cicBrowser (Some (`About `Hints)));
connect_menu_item main#showTermGrammarMenuItem
- (fun _ ->
- let c = MatitaMathView.cicBrowser () in
- c#load (`About `Grammar));
+ (fun _ -> MatitaMathView.cicBrowser (Some (`About `Grammar)));
connect_menu_item main#showUnicodeTable
- (fun _ ->
- let c = MatitaMathView.cicBrowser () in
- c#load (`About `TeX));
+ (fun _ -> MatitaMathView.cicBrowser (Some (`About `TeX)));
(* debug menu *)
main#debugMenu#misc#hide ();
(* HBUGS *)
main#hpaneScriptSequent#set_position script_w;
(* math view handling *)
connect_menu_item main#newCicBrowserMenuItem (fun () ->
- ignore(MatitaMathView.cicBrowser ()));
+ ignore(MatitaMathView.cicBrowser None));
connect_menu_item main#increaseFontSizeMenuItem
MatitaMisc.increase_font_size;
connect_menu_item main#decreaseFontSizeMenuItem
MatitaMisc.decrease_font_size;
connect_menu_item main#normalFontSizeMenuItem
MatitaMisc.reset_font_size;
- ignore (main#scriptNotebook#connect#switch_page
- (fun page ->
- let script = MatitaScript.at_page page in
- script#activate;
- main#saveMenuItem#misc#set_sensitive script#has_name));
+ ignore (main#scriptNotebook#connect#switch_page (fun page ->
+ self#save_page ();
+ current_page <- 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
let script = MatitaScript.at_page page in
self#closeScript page script
+ method private save_page () =
+ if current_page >= 0 then
+ let old_script = MatitaScript.at_page current_page in
+ save_moo0 ~do_clean:false old_script old_script#status
+
method newScript () =
+ self#save_page ();
let scrolledWindow = GBin.scrolled_window () in
let hbox = GPack.hbox () in
- let tab_label = GMisc.label ~text:"foo"
- ~packing:hbox#pack () 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
+ let image = GMisc.image ~stock:`CLOSE ~icon_size:`MENU () in
closebutton#set_image image#coerce;
- let script =
- MatitaScript.script
- ~urichooser:(fun source_view uris ->
- try
- interactive_uri_choice ~selection_mode:`SINGLE
- ~title:"Matita: URI chooser"
- ~msg:"Select the URI" ~hide_uri_entry:true
- ~hide_try:true ~ok_label:"_Apply" ~ok_action:`SELECT
- ~copy_cb:(fun s -> source_view#buffer#insert ("\n"^s^"\n"))
- () ~id:"boh?" uris
- with MatitaTypes.Cancel -> [])
- ~ask_confirmation:
- (fun ~title ~message ->
- MatitaGtkMisc.ask_confirmation ~title ~message
- ~parent:(MatitaMisc.get_gui ())#main#toplevel ())
- ~parent:scrolledWindow ~tab_label ()
- in
+ let script = MatitaScript.script ~parent:scrolledWindow ~tab_label () in
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));
+ self#closeScript
+ (main#scriptNotebook#page_num scrolledWindow#coerce) script));
main#scriptNotebook#goto_page 0;
sequents_viewer#reset;
sequents_viewer#load_logo;
method private findRepl = findRepl
method main = main
- method newBrowserWin () =
- object (self)
- inherit browserWin ()
- val combo = GEdit.entry ()
- initializer
- self#check_widgets ();
- let combo_widget = combo#coerce in
- uriHBox#pack ~from:`END ~fill:true ~expand:true combo_widget;
- combo#misc#grab_focus ()
- method browserUri = combo
- end
-
- method newUriDialog () =
- let dialog = new uriChoiceDialog () in
- dialog#check_widgets ();
- dialog
-
- method private 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)
+ method private addKeyBinding key ?modifiers callback =
+(* List.iter (fun evbox -> add_key_binding key callback evbox) *)
+ List.iter (fun evbox -> connect_key evbox#event key ?modifiers callback)
keyBindingBoxes
method private setQuitCallback callback =
let gui () =
let g = new gui () in
- gui_instance := Some g;
- MatitaMisc.set_gui g;
- g
+ let rg = (g :> MatitaGuiTypes.gui) in
+ MatitaMisc.set_gui rg;
+ g#newScript ();
+ rg
let instance = singleton gui
let interactive_string_choice
text prefix_len ?(title = "") ?(msg = "") () ~id locs uris
=
- let gui = instance () in
- let dialog = gui#newUriDialog () in
- dialog#uriEntryHBox#misc#hide ();
- dialog#uriChoiceSelectedButton#misc#hide ();
- dialog#uriChoiceAutoButton#misc#hide ();
- dialog#uriChoiceConstantsButton#misc#hide ();
- dialog#uriChoiceTreeView#selection#set_mode
- (`SINGLE :> Gtk.Tags.selection_mode);
- let model = new stringListModel dialog#uriChoiceTreeView in
- let choices = ref None in
- dialog#uriChoiceDialog#set_title title;
- let hack_len = MatitaGtkMisc.utf8_string_length text in
- let rec colorize acc_len = function
- | [] ->
- let floc = HExtlib.floc_of_loc (acc_len,hack_len) in
- escape_pango_markup (fst(MatitaGtkMisc.utf8_parsed_text text floc))
- | he::tl ->
- let start, stop = HExtlib.loc_of_floc he in
- let floc1 = HExtlib.floc_of_loc (acc_len,start) in
- let str1,_=MatitaGtkMisc.utf8_parsed_text text floc1 in
- let str2,_ = MatitaGtkMisc.utf8_parsed_text text he in
- escape_pango_markup str1 ^ "<b>" ^
- escape_pango_markup str2 ^ "</b>" ^
- colorize stop tl
- in
+ let dialog = new uriChoiceDialog () in
+ dialog#uriEntryHBox#misc#hide ();
+ dialog#uriChoiceSelectedButton#misc#hide ();
+ dialog#uriChoiceAutoButton#misc#hide ();
+ dialog#uriChoiceConstantsButton#misc#hide ();
+ dialog#uriChoiceTreeView#selection#set_mode
+ (`SINGLE :> Gtk.Tags.selection_mode);
+ let model = new stringListModel dialog#uriChoiceTreeView in
+ let choices = ref None in
+ dialog#uriChoiceDialog#set_title title;
+ let hack_len = MatitaGtkMisc.utf8_string_length text in
+ let rec colorize acc_len = function
+ | [] ->
+ let floc = HExtlib.floc_of_loc (acc_len,hack_len) in
+ escape_pango_markup (fst(MatitaGtkMisc.utf8_parsed_text text floc))
+ | he::tl ->
+ let start, stop = HExtlib.loc_of_floc he in
+ let floc1 = HExtlib.floc_of_loc (acc_len,start) in
+ let str1,_=MatitaGtkMisc.utf8_parsed_text text floc1 in
+ let str2,_ = MatitaGtkMisc.utf8_parsed_text text he in
+ escape_pango_markup str1 ^ "<b>" ^
+ escape_pango_markup str2 ^ "</b>" ^
+ colorize stop tl
+ in
(* List.iter (fun l -> let start, stop = HExtlib.loc_of_floc l in
- Printf.eprintf "(%d,%d)" start stop) locs; *)
- let locs =
- List.sort
- (fun loc1 loc2 ->
- fst (HExtlib.loc_of_floc loc1) - fst (HExtlib.loc_of_floc loc2))
- locs
- in
+ Printf.eprintf "(%d,%d)" start stop) locs; *)
+ let locs =
+ List.sort
+ (fun loc1 loc2 ->
+ fst (HExtlib.loc_of_floc loc1) - fst (HExtlib.loc_of_floc loc2))
+ locs
+ in
(* prerr_endline "XXXXXXXXXXXXXXXXXXXX";
- List.iter (fun l -> let start, stop = HExtlib.loc_of_floc l in
- Printf.eprintf "(%d,%d)" start stop) locs;
- prerr_endline "XXXXXXXXXXXXXXXXXXXX2"; *)
- dialog#uriChoiceLabel#set_use_markup true;
- let txt = colorize 0 locs in
- let txt,_ = MatitaGtkMisc.utf8_parsed_text txt
- (HExtlib.floc_of_loc (prefix_len,MatitaGtkMisc.utf8_string_length txt))
- in
- dialog#uriChoiceLabel#set_label txt;
- List.iter model#easy_append uris;
- let return v =
- choices := v;
- dialog#uriChoiceDialog#destroy ();
- GMain.Main.quit ()
- in
- ignore (dialog#uriChoiceDialog#event#connect#delete (fun _ -> true));
- connect_button dialog#uriChoiceForwardButton (fun _ ->
- match model#easy_selection () with
- | [] -> ()
- | uris -> return (Some uris));
- connect_button dialog#uriChoiceAbortButton (fun _ -> return None);
- dialog#uriChoiceDialog#show ();
- GtkThread.main ();
- (match !choices with
- | None -> raise MatitaTypes.Cancel
- | Some uris -> uris)
+ List.iter (fun l -> let start, stop = HExtlib.loc_of_floc l in
+ Printf.eprintf "(%d,%d)" start stop) locs;
+ prerr_endline "XXXXXXXXXXXXXXXXXXXX2"; *)
+ dialog#uriChoiceLabel#set_use_markup true;
+ let txt = colorize 0 locs in
+ let txt,_ = MatitaGtkMisc.utf8_parsed_text txt
+ (HExtlib.floc_of_loc (prefix_len,MatitaGtkMisc.utf8_string_length txt))
+ in
+ dialog#uriChoiceLabel#set_label txt;
+ List.iter model#easy_append uris;
+ let return v =
+ choices := v;
+ dialog#uriChoiceDialog#destroy ();
+ GMain.Main.quit ()
+ in
+ ignore (dialog#uriChoiceDialog#event#connect#delete (fun _ -> true));
+ connect_button dialog#uriChoiceForwardButton (fun _ ->
+ match model#easy_selection () with
+ | [] -> ()
+ | uris -> return (Some uris));
+ connect_button dialog#uriChoiceAbortButton (fun _ -> return None);
+ dialog#uriChoiceDialog#show ();
+ GtkThread.main ();
+ (match !choices with
+ | None -> raise MatitaTypes.Cancel
+ | Some uris -> uris)
let interactive_interp_choice () text prefix_len choices =
(*List.iter (fun l -> prerr_endline "==="; List.iter (fun (_,id,dsc) -> prerr_endline (id ^ " = " ^ dsc)) l) choices;*)
projects / helm.git / blobdiff