X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FmatitaGui.ml;h=5b7352d743f9cbaf4ade7b39b3af0cd85fb3cbe7;hb=5b5dca0c118dfbe3ba8f0514ef07549544eb7810;hp=7589f19f8089a878f6e6b0467f917264f967dd18;hpb=5d8d825b9bf6b3cf346ba8e81ffd0ac1e1902ecb;p=helm.git
diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml
index 7589f19f8..5b7352d74 100644
--- a/matita/matita/matitaGui.ml
+++ b/matita/matita/matitaGui.ml
@@ -31,19 +31,78 @@ open MatitaGeneratedGui
open MatitaGtkMisc
open MatitaMisc
-exception Found of int
-
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 = "")
+ ?(msg = "") ?(nonvars_button = false) ?(hide_uri_entry=false)
+ ?(hide_try=false) ?(ok_label="_Auto") ?(ok_action:[`SELECT|`AUTO] = `AUTO)
+ ?copy_cb ()
+ ~id:_ uris
+=
+ if (selection_mode <> `SINGLE) &&
+ (Helm_registry.get_opt_default Helm_registry.get_bool ~default:true "matita.auto_disambiguation")
+ then
+ uris
+ else begin
+ let dialog = new uriChoiceDialog () 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
+ (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 NReference.string_of_reference 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 uris));
+ if ok_action = `AUTO then
+ connect_button dialog#uriChoiceAutoButton (fun _ ->
+ Helm_registry.set_bool "matita.auto_disambiguation" true;
+ return (Some uris))
+ else
+ connect_button dialog#uriChoiceAutoButton (fun _ ->
+ match model#easy_selection () with
+ | [] -> ()
+ | uris -> return (Some (List.map NReference.reference_of_string uris)));
+ connect_button dialog#uriChoiceSelectedButton (fun _ ->
+ match model#easy_selection () with
+ | [] -> ()
+ | uris -> return (Some (List.map NReference.reference_of_string uris)));
+ connect_button dialog#uriChoiceAbortButton (fun _ -> return None);
+ dialog#uriChoiceDialog#show ();
+ (* CSC: old Gtk2 code. Use #run instead. Look for similar code handling
+ other dialogs *)
+ GtkThread.main ();
+ (match !choices with
+ | None -> raise MatitaTypes.Cancel
+ | Some uris -> uris)
+ 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)
@@ -66,24 +125,28 @@ class console ~(buffer: GText.buffer) () =
| `Warning -> self#warning (s ^ "\n")
end
-let clean_current_baseuri grafite_status =
- LibraryClean.clean_baseuris [grafite_status#baseuri]
+let clean_current_baseuri status =
+ LibraryClean.clean_baseuris [status#baseuri]
-let save_moo grafite_status =
- let script = MatitaScript.current () in
- let baseuri = grafite_status#baseuri 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)
- grafite_status
- | _ -> clean_current_baseuri grafite_status
+ 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 =
+let ask_unsaved parent filename =
MatitaGtkMisc.ask_confirmation
~parent ~title:"Unsaved work!"
- ~message:("Your work is unsaved!\n\n"^
+ ~message:("Script " ^ filename ^ " is modified.!\n\n"^
"Do you want to save the script before continuing?")
()
@@ -115,7 +178,7 @@ class interpErrorModel =
(let loc_row = tree_store#append () in
begin
match lll with
- [passes,envs_and_diffs,_,_] ->
+ [passes,_envs_and_diffs,_,_] ->
tree_store#set ~row:loc_row ~column:id_col
("Error location " ^ string_of_int (!idx1+1) ^
", error message " ^ string_of_int (!idx1+1) ^ ".1" ^
@@ -191,8 +254,8 @@ class interpErrorModel =
exception UseLibrary;;
-let rec interactive_error_interp ~all_passes
- (source_buffer:GSourceView2.source_buffer) notify_exn offset errorll filename
+let interactive_error_interp ~all_passes
+ (source_buffer:GSourceView3.source_buffer) notify_exn offset errorll filename
=
(* hook to save a script for each disambiguation error *)
if false then
@@ -255,10 +318,12 @@ let rec interactive_error_interp ~all_passes
(MultiPassDisambiguator.DisambiguationError
(offset,[[env,diff,lazy (loffset,Lazy.force msg),significant]]));
| _::_ ->
+ GtkThread.sync (fun _ ->
let dialog = new disambiguationErrors () in
- dialog#check_widgets ();
- if all_passes then
- dialog#disambiguationErrorsMoreErrors#misc#set_sensitive false;
+ dialog#toplevel#add_button "Fix this interpretation" `OK;
+ dialog#toplevel#add_button "Close" `DELETE_EVENT;
+ if not all_passes then
+ dialog#toplevel#add_button "More errors" `HELP; (* HELP means MORE *)
let model = new interpErrorModel dialog#treeview choices in
dialog#disambiguationErrors#set_title "Disambiguation error";
dialog#disambiguationErrorsLabel#set_label
@@ -290,125 +355,83 @@ let rec interactive_error_interp ~all_passes
(MultiPassDisambiguator.DisambiguationError
(offset,[[env,diff,lazy(loffset,Lazy.force msg),significant]]))
));
- let return _ =
- dialog#disambiguationErrors#destroy ();
- GMain.Main.quit ()
+ (match GtkThread.sync dialog#toplevel#run () with
+ | `OK ->
+ let tree_path =
+ match fst (dialog#treeview#get_cursor ()) with
+ None -> assert false
+ | Some tp -> tp in
+ let idx1,idx2,idx3 = model#get_interp_no tree_path in
+ let diff =
+ match idx2,idx3 with
+ Some idx2, Some idx3 ->
+ let _,lll = List.nth choices idx1 in
+ let _,envs_and_diffs,_,_ = List.nth lll idx2 in
+ let _,_,diff = List.nth envs_and_diffs idx3 in
+ diff
+ | _,_ -> assert false
in
- let fail _ = return () in
- ignore(dialog#disambiguationErrors#event#connect#delete (fun _ -> true));
- connect_button dialog#disambiguationErrorsOkButton
- (fun _ ->
- let tree_path =
- match fst (dialog#treeview#get_cursor ()) with
- None -> assert false
- | Some tp -> tp in
- let idx1,idx2,idx3 = model#get_interp_no tree_path in
- let diff =
- match idx2,idx3 with
- Some idx2, Some idx3 ->
- let _,lll = List.nth choices idx1 in
- let _,envs_and_diffs,_,_ = List.nth lll idx2 in
- let _,_,diff = List.nth envs_and_diffs idx3 in
- diff
- | _,_ -> assert false
- in
- let newtxt =
- String.concat "\n"
- ("" ::
- List.map
- (fun k,desc ->
- let alias =
- match k with
- | DisambiguateTypes.Id id ->
- GrafiteAst.Ident_alias (id, desc)
- | DisambiguateTypes.Symbol (symb, i)->
- GrafiteAst.Symbol_alias (symb, i, desc)
- | DisambiguateTypes.Num i ->
- GrafiteAst.Number_alias (i, desc)
- in
- GrafiteAstPp.pp_alias alias)
- diff) ^ "\n"
- in
- source_buffer#insert
- ~iter:
- (source_buffer#get_iter_at_mark
- (`NAME "beginning_of_statement")) newtxt ;
- return ()
- );
- connect_button dialog#disambiguationErrorsMoreErrors
- (fun _ -> return () ; raise UseLibrary);
- connect_button dialog#disambiguationErrorsCancelButton fail;
- dialog#disambiguationErrors#show ();
- GtkThread.main ()
-
-
-(** Selection handling
- * Two clipboards are used: "clipboard" and "primary".
- * "primary" is used by X, when you hit the middle button mouse is content is
- * pasted between applications. In Matita this selection always contain the
- * textual version of the selected term.
- * "clipboard" is used inside Matita only and support ATM two different targets:
- * "TERM" and "PATTERN", in the future other targets like "MATHMLCONTENT" may
- * be added
- *)
+ let newtxt =
+ String.concat "\n"
+ ("" ::
+ List.map
+ (fun k,desc ->
+ let alias =
+ match k with
+ | DisambiguateTypes.Id id ->
+ GrafiteAst.Ident_alias (id, desc)
+ | DisambiguateTypes.Symbol (symb, i)->
+ GrafiteAst.Symbol_alias (symb, i, desc)
+ | DisambiguateTypes.Num i ->
+ GrafiteAst.Number_alias (i, desc)
+ in
+ GrafiteAstPp.pp_alias alias)
+ diff) ^ "\n"
+ in
+ source_buffer#insert
+ ~iter:
+ (source_buffer#get_iter_at_mark
+ (`NAME "beginning_of_statement")) newtxt
+ | `HELP (* HELP MEANS MORE *) ->
+ dialog#toplevel#destroy () ;
+ raise UseLibrary
+ | `DELETE_EVENT -> ()
+ | _ -> assert false) ;
+ dialog#toplevel#destroy ()
+ ) ()
class gui () =
(* creation order _is_ relevant for windows placement *)
let main = new mainWin () in
- let fileSel = new fileSelectionWin () in
+ let sequents_viewer =
+ MatitaMathView.sequentsViewer_instance main#sequentsNotebook in
let findRepl = new findReplWin () 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: GSourceView2.source_view) =
- GSourceView2.source_view
- ~auto_indent:true
- ~insert_spaces_instead_of_tabs:true ~tab_width:2
- ~right_margin_position:80 ~show_right_margin:true
- ~smart_home_end:`AFTER
- ~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 similarsymbols_tag_name = "similarsymbolos" in
- let similarsymbols_tag = `NAME similarsymbols_tag_name in
- let source_buffer = source_view#source_buffer in
object (self)
val mutable chosen_file = None
val mutable _ok_not_exists = false
val mutable _only_directory = false
- val mutable font_size = default_font_size
- val mutable similarsymbols = []
- val mutable similarsymbols_orig = []
- val clipboard = GData.clipboard Gdk.Atom.clipboard
- val primary = GData.clipboard Gdk.Atom.primary
+ val mutable current_page = -1
- method private reset_similarsymbols =
- similarsymbols <- [];
- similarsymbols_orig <- [];
- try source_buffer#delete_mark similarsymbols_tag
- with GText.No_such_mark _ -> ()
-
initializer
let s () = MatitaScript.current () in
- (* glade's check widgets *)
- List.iter (fun w -> w#check_widgets ())
- (let c w = (w :> 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
@@ -434,6 +457,7 @@ class gui () =
~website:"http://matita.cs.unibo.it"
()
in
+ ignore(about_dialog#event#connect#delete (fun _ -> true));
ignore(about_dialog#connect#response (fun _ ->about_dialog#misc#hide ()));
connect_menu_item main#contentsMenuItem (fun () ->
if 0 = Sys.command "which gnome-help" then
@@ -456,28 +480,30 @@ class gui () =
in
let hide_find_Repl () = findRepl#toplevel#misc#hide () in
let find_forward _ =
+ let source_view = (s ())#source_view in
let highlight start end_ =
- source_buffer#move_mark `INSERT ~where:start;
- source_buffer#move_mark `SEL_BOUND ~where:end_;
+ source_view#source_buffer#move_mark `INSERT ~where:start;
+ source_view#source_buffer#move_mark `SEL_BOUND ~where:end_;
source_view#scroll_mark_onscreen `INSERT
in
let text = findRepl#findEntry#text in
- let iter = source_buffer#get_iter `SEL_BOUND in
+ let iter = source_view#source_buffer#get_iter `SEL_BOUND in
match iter#forward_search text with
| None ->
- (match source_buffer#start_iter#forward_search text with
+ (match source_view#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 source_view = (s ())#source_view in
let text = findRepl#replaceEntry#text in
- let ins = source_buffer#get_iter `INSERT in
- let sel = source_buffer#get_iter `SEL_BOUND in
+ let ins = source_view#source_buffer#get_iter `INSERT in
+ let sel = source_view#source_buffer#get_iter `SEL_BOUND in
if ins#compare sel < 0 then
begin
- ignore(source_buffer#delete_selection ());
- source_buffer#insert text
+ ignore(source_view#source_buffer#delete_selection ());
+ source_view#source_buffer#insert text
end
in
connect_button findRepl#findButton find_forward;
@@ -485,175 +511,51 @@ class gui () =
connect_button findRepl#cancelButton (fun _ -> hide_find_Repl ());
ignore(findRepl#toplevel#event#connect#delete
~callback:(fun _ -> hide_find_Repl ();true));
- let safe_undo =
- fun () ->
- (* phase 1: we save the actual status of the marks and we undo *)
- let locked_mark = `MARK ((MatitaScript.current ())#locked_mark) in
- let locked_iter = source_view#buffer#get_iter_at_mark locked_mark in
- let locked_iter_offset = locked_iter#offset in
- let mark2 =
- `MARK
- (source_view#buffer#create_mark ~name:"lock_point"
- ~left_gravity:true locked_iter) in
- source_view#source_buffer#undo ();
- (* phase 2: we save the cursor position and we redo, restoring
- the previous status of all the marks *)
- let cursor_iter = source_view#buffer#get_iter_at_mark `INSERT in
- let mark =
- `MARK
- (source_view#buffer#create_mark ~name:"undo_point"
- ~left_gravity:true cursor_iter)
- in
- source_view#source_buffer#redo ();
- let mark_iter = source_view#buffer#get_iter_at_mark mark in
- let mark2_iter = source_view#buffer#get_iter_at_mark mark2 in
- let mark2_iter = mark2_iter#set_offset locked_iter_offset in
- source_view#buffer#move_mark locked_mark ~where:mark2_iter;
- source_view#buffer#delete_mark mark;
- source_view#buffer#delete_mark mark2;
- (* phase 3: if after the undo the cursor was in the locked area,
- then we move it there again and we perform a goto *)
- if mark_iter#offset < locked_iter_offset then
- begin
- source_view#buffer#move_mark `INSERT ~where:mark_iter;
- (MatitaScript.current ())#goto `Cursor ();
- end;
- (* phase 4: we perform again the undo. This time we are sure that
- the text to undo is not locked *)
- source_view#source_buffer#undo ();
- source_view#misc#grab_focus () in
- let safe_redo =
- fun () ->
- (* phase 1: we save the actual status of the marks, we redo and
- we undo *)
- let locked_mark = `MARK ((MatitaScript.current ())#locked_mark) in
- let locked_iter = source_view#buffer#get_iter_at_mark locked_mark in
- let locked_iter_offset = locked_iter#offset in
- let mark2 =
- `MARK
- (source_view#buffer#create_mark ~name:"lock_point"
- ~left_gravity:true locked_iter) in
- source_view#source_buffer#redo ();
- source_view#source_buffer#undo ();
- (* phase 2: we save the cursor position and we restore
- the previous status of all the marks *)
- let cursor_iter = source_view#buffer#get_iter_at_mark `INSERT in
- let mark =
- `MARK
- (source_view#buffer#create_mark ~name:"undo_point"
- ~left_gravity:true cursor_iter)
- in
- let mark_iter = source_view#buffer#get_iter_at_mark mark in
- let mark2_iter = source_view#buffer#get_iter_at_mark mark2 in
- let mark2_iter = mark2_iter#set_offset locked_iter_offset in
- source_view#buffer#move_mark locked_mark ~where:mark2_iter;
- source_view#buffer#delete_mark mark;
- source_view#buffer#delete_mark mark2;
- (* phase 3: if after the undo the cursor is in the locked area,
- then we move it there again and we perform a goto *)
- if mark_iter#offset < locked_iter_offset then
- begin
- source_view#buffer#move_mark `INSERT ~where:mark_iter;
- (MatitaScript.current ())#goto `Cursor ();
- end;
- (* phase 4: we perform again the redo. This time we are sure that
- the text to redo is not locked *)
- source_view#source_buffer#redo ();
- source_view#misc#grab_focus ()
- in
- connect_menu_item main#undoMenuItem safe_undo;
-(*CSC: XXX
- ignore(source_view#source_buffer#connect#can_undo
- ~callback:main#undoMenuItem#misc#set_sensitive);
-*) main#undoMenuItem#misc#set_sensitive true;
- connect_menu_item main#redoMenuItem safe_redo;
-(*CSC: XXX
- ignore(source_view#source_buffer#connect#can_redo
- ~callback:main#redoMenuItem#misc#set_sensitive);
-*) main#redoMenuItem#misc#set_sensitive true;
- ignore(source_view#connect#after#populate_popup
- ~callback:(fun pre_menu ->
- let menu = new GMenu.menu pre_menu in
- let menuItems = menu#children in
- let undoMenuItem, redoMenuItem =
- match menuItems with
- [undo;redo;sep1;cut;copy;paste;delete;sep2;
- selectall;sep3;inputmethod;insertunicodecharacter] ->
- List.iter menu#remove [ copy; cut; delete; paste ];
- undo,redo
- | _ -> assert false in
- let add_menu_item =
- let i = ref 2 in (* last occupied position *)
- fun ?label ?stock () ->
- incr i;
- GMenu.image_menu_item ?label ?stock ~packing:(menu#insert ~pos:!i)
- ()
- in
- let copy = add_menu_item ~stock:`COPY () in
- let cut = add_menu_item ~stock:`CUT () in
- let delete = add_menu_item ~stock:`DELETE () in
- let paste = add_menu_item ~stock:`PASTE () in
- let paste_pattern = add_menu_item ~label:"Paste as pattern" () in
- copy#misc#set_sensitive self#canCopy;
- cut#misc#set_sensitive self#canCut;
- delete#misc#set_sensitive self#canDelete;
- paste#misc#set_sensitive self#canPaste;
- paste_pattern#misc#set_sensitive self#canPastePattern;
- connect_menu_item copy self#copy;
- connect_menu_item cut self#cut;
- connect_menu_item delete self#delete;
- connect_menu_item paste self#paste;
- connect_menu_item paste_pattern self#pastePattern;
- let new_undoMenuItem =
- GMenu.image_menu_item
- ~image:(GMisc.image ~stock:`UNDO ())
- ~use_mnemonic:true
- ~label:"_Undo"
- ~packing:(menu#insert ~pos:0) () in
- new_undoMenuItem#misc#set_sensitive
- (undoMenuItem#misc#get_flag `SENSITIVE);
- menu#remove (undoMenuItem :> GMenu.menu_item);
- connect_menu_item new_undoMenuItem safe_undo;
- let new_redoMenuItem =
- GMenu.image_menu_item
- ~image:(GMisc.image ~stock:`REDO ())
- ~use_mnemonic:true
- ~label:"_Redo"
- ~packing:(menu#insert ~pos:1) () in
- new_redoMenuItem#misc#set_sensitive
- (redoMenuItem#misc#get_flag `SENSITIVE);
- menu#remove (redoMenuItem :> GMenu.menu_item);
- connect_menu_item new_redoMenuItem safe_redo));
-
+ connect_menu_item main#undoMenuItem
+ (fun () -> (MatitaScript.current ())#safe_undo);
+ main#undoMenuItem#misc#set_sensitive false;
+ connect_menu_item main#redoMenuItem
+ (fun () -> (MatitaScript.current ())#safe_redo);
+ main#redoMenuItem#misc#set_sensitive false;
connect_menu_item main#editMenu (fun () ->
- main#copyMenuItem#misc#set_sensitive self#canCopy;
- main#cutMenuItem#misc#set_sensitive self#canCut;
- main#deleteMenuItem#misc#set_sensitive self#canDelete;
- main#pasteMenuItem#misc#set_sensitive self#canPaste;
- main#pastePatternMenuItem#misc#set_sensitive self#canPastePattern);
- connect_menu_item main#copyMenuItem self#copy;
- connect_menu_item main#cutMenuItem self#cut;
- connect_menu_item main#deleteMenuItem self#delete;
- connect_menu_item main#pasteMenuItem self#paste;
- connect_menu_item main#pastePatternMenuItem self#pastePattern;
+ main#copyMenuItem#misc#set_sensitive
+ (MatitaScript.current ())#canCopy;
+ main#cutMenuItem#misc#set_sensitive
+ (MatitaScript.current ())#canCut;
+ main#deleteMenuItem#misc#set_sensitive
+ (MatitaScript.current ())#canDelete;
+ main#pasteMenuItem#misc#set_sensitive
+ (MatitaScript.current ())#canPaste;
+ main#pastePatternMenuItem#misc#set_sensitive
+ (MatitaScript.current ())#canPastePattern);
+ connect_menu_item main#copyMenuItem
+ (fun () -> (MatitaScript.current ())#copy ());
+ connect_menu_item main#cutMenuItem
+ (fun () -> (MatitaScript.current ())#cut ());
+ connect_menu_item main#deleteMenuItem
+ (fun () -> (MatitaScript.current ())#delete ());
+ connect_menu_item main#pasteMenuItem
+ (fun () -> (MatitaScript.current ())#paste ());
+ connect_menu_item main#pastePatternMenuItem
+ (fun () -> (MatitaScript.current ())#pastePattern ());
connect_menu_item main#selectAllMenuItem (fun () ->
- source_buffer#move_mark `INSERT source_buffer#start_iter;
- source_buffer#move_mark `SEL_BOUND source_buffer#end_iter);
+ let source_view = (s ())#source_view in
+ source_view#source_buffer#move_mark `INSERT source_view#source_buffer#start_iter;
+ source_view#source_buffer#move_mark `SEL_BOUND source_view#source_buffer#end_iter);
connect_menu_item main#findReplMenuItem show_find_Repl;
connect_menu_item main#externalEditorMenuItem self#externalEditor;
- connect_menu_item main#ligatureButton self#nextSimilarSymbol;
- ignore(source_buffer#connect#after#insert_text
- ~callback:(fun iter str ->
- if main#menuitemAutoAltL#active && (str = " " || str = "\n") then
- ignore(self#expand_virtual_if_any iter str)));
+ connect_menu_item main#ligatureButton
+ (fun () -> (MatitaScript.current ())#nextSimilarSymbol);
ignore (findRepl#findEntry#connect#activate find_forward);
(* interface lockers *)
let lock_world _ =
+ let source_view = (s ())#source_view in
main#buttonsToolbar#misc#set_sensitive false;
main#scriptMenu#misc#set_sensitive false;
source_view#set_editable false
in
let unlock_world _ =
+ let source_view = (s ())#source_view in
main#buttonsToolbar#misc#set_sensitive true;
main#scriptMenu#misc#set_sensitive true;
source_view#set_editable true;
@@ -661,7 +563,7 @@ class gui () =
GtkThread.sync (fun () -> ()) ()
in
let worker_thread = ref None in
- let notify_exn exn =
+ let notify_exn (source_view : GSourceView3.source_view) exn =
let floc, msg = MatitaExcPp.to_string exn in
begin
match floc with
@@ -672,56 +574,64 @@ class gui () =
let locked_mark = script#locked_mark in
let error_tag = script#error_tag in
let baseoffset =
- (source_buffer#get_iter_at_mark (`MARK locked_mark))#offset in
+ (source_view#source_buffer#get_iter_at_mark (`MARK locked_mark))#offset in
let x' = baseoffset + x in
let y' = baseoffset + y in
- let x_iter = source_buffer#get_iter (`OFFSET x') in
- let y_iter = source_buffer#get_iter (`OFFSET y') in
- source_buffer#apply_tag error_tag ~start:x_iter ~stop:y_iter;
+ let x_iter = source_view#source_buffer#get_iter (`OFFSET x') in
+ let y_iter = source_view#source_buffer#get_iter (`OFFSET y') in
+ source_view#source_buffer#apply_tag error_tag ~start:x_iter ~stop:y_iter;
let id = ref None in
- id := Some (source_buffer#connect#changed ~callback:(fun () ->
- source_buffer#remove_tag error_tag
- ~start:source_buffer#start_iter
- ~stop:source_buffer#end_iter;
+ id := Some (source_view#source_buffer#connect#changed ~callback:(fun () ->
+ source_view#source_buffer#remove_tag error_tag
+ ~start:source_view#source_buffer#start_iter
+ ~stop:source_view#source_buffer#end_iter;
match !id with
| None -> assert false (* a race condition occurred *)
| Some id ->
- (new GObj.gobject_ops source_buffer#as_buffer)#disconnect id));
- source_buffer#place_cursor
- (source_buffer#get_iter (`OFFSET x'));
+ source_view#source_buffer#misc#disconnect id));
+ source_view#source_buffer#place_cursor
+ (source_view#source_buffer#get_iter (`OFFSET x'));
end;
HLog.error msg in
- let locker f () =
+ let locker f script =
+ let source_view = script#source_view in
let thread_main =
fun () ->
lock_world ();
let saved_use_library= !MultiPassDisambiguator.use_library in
try
MultiPassDisambiguator.use_library := !all_disambiguation_passes;
- f ();
+ prerr_endline "PRIMA";
+ f script;
MultiPassDisambiguator.use_library := saved_use_library;
- unlock_world ()
+ prerr_endline "DOPO";
+ unlock_world () ;
+ prerr_endline "FINE";
with
| MultiPassDisambiguator.DisambiguationError (offset,errorll) ->
+ prerr_endline "EXC1";
(try
interactive_error_interp
- ~all_passes:!all_disambiguation_passes source_buffer
- notify_exn offset errorll (s())#filename
+ ~all_passes:!all_disambiguation_passes source_view#source_buffer
+ (notify_exn source_view) offset errorll (s())#filename
with
| UseLibrary ->
MultiPassDisambiguator.use_library := true;
- (try f ()
+ (try f script
with
| MultiPassDisambiguator.DisambiguationError (offset,errorll) ->
- interactive_error_interp ~all_passes:true source_buffer
- notify_exn offset errorll (s())#filename
+ interactive_error_interp ~all_passes:true source_view#source_buffer
+ (notify_exn source_view) offset errorll (s())#filename
| exc ->
- notify_exn exc);
- | exc -> notify_exn exc);
+ notify_exn source_view exc);
+ | exc -> notify_exn source_view exc);
MultiPassDisambiguator.use_library := saved_use_library;
- unlock_world ()
+ prerr_endline "DOPO1";
+ unlock_world ();
+ prerr_endline "FINE1"
| exc ->
- (try notify_exn exc with Sys.Break as e -> notify_exn e);
+ (try notify_exn source_view exc
+ with Sys.Break as e -> notify_exn source_view e);
unlock_world ()
in
(*thread_main ();*)
@@ -746,39 +656,12 @@ class gui () =
match !worker_thread with
None -> assert false
| Some t -> interrupt := Some (Thread.id t) in
- let keep_focus f =
- fun () ->
+ let keep_focus f (script: MatitaScript.script) =
try
- f (); source_view#misc#grab_focus ()
+ f script; script#source_view#misc#grab_focus ()
with
- exc -> source_view#misc#grab_focus (); raise exc in
+ exc -> script#source_view#misc#grab_focus (); raise exc in
- (* 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
- begin
- if HExtlib.is_regular fname && not (_only_directory) then
- return (Some fname)
- else if _only_directory && HExtlib.is_dir fname then
- return (Some fname)
- end
- else
- begin
- if _ok_not_exists then
- return (Some fname)
- end
- | `CANCEL -> return None
- | `HELP -> ()
- | `DELETE_EVENT -> return None));
(* menus *)
List.iter (fun w -> w#misc#set_sensitive false) [ main#saveMenuItem ];
(* console *)
@@ -794,48 +677,48 @@ class gui () =
else main#tacticsButtonsHandlebox#misc#hide ())
~check:main#menuitemPalette;
connect_button main#butImpl_intro
- (fun () -> source_buffer#insert "apply rule (â#i [â¦] (â¦));\n");
+ (fun () -> (s ())#source_view#source_buffer#insert "apply rule (â#i [â¦] (â¦));\n");
connect_button main#butAnd_intro
- (fun () -> source_buffer#insert
+ (fun () -> (s ())#source_view#source_buffer#insert
"apply rule (â§#i (â¦) (â¦));\n\t[\n\t|\n\t]\n");
connect_button main#butOr_intro_left
- (fun () -> source_buffer#insert "apply rule (â¨#i_l (â¦));\n");
+ (fun () -> (s ())#source_view#source_buffer#insert "apply rule (â¨#i_l (â¦));\n");
connect_button main#butOr_intro_right
- (fun () -> source_buffer#insert "apply rule (â¨#i_r (â¦));\n");
+ (fun () -> (s ())#source_view#source_buffer#insert "apply rule (â¨#i_r (â¦));\n");
connect_button main#butNot_intro
- (fun () -> source_buffer#insert "apply rule (¬#i [â¦] (â¦));\n");
+ (fun () -> (s ())#source_view#source_buffer#insert "apply rule (¬#i [â¦] (â¦));\n");
connect_button main#butTop_intro
- (fun () -> source_buffer#insert "apply rule (â¤#i);\n");
+ (fun () -> (s ())#source_view#source_buffer#insert "apply rule (â¤#i);\n");
connect_button main#butImpl_elim
- (fun () -> source_buffer#insert
+ (fun () -> (s ())#source_view#source_buffer#insert
"apply rule (â#e (â¦) (â¦));\n\t[\n\t|\n\t]\n");
connect_button main#butAnd_elim_left
- (fun () -> source_buffer#insert "apply rule (â§#e_l (â¦));\n");
+ (fun () -> (s ())#source_view#source_buffer#insert "apply rule (â§#e_l (â¦));\n");
connect_button main#butAnd_elim_right
- (fun () -> source_buffer#insert "apply rule (â§#e_r (â¦));\n");
+ (fun () -> (s ())#source_view#source_buffer#insert "apply rule (â§#e_r (â¦));\n");
connect_button main#butOr_elim
- (fun () -> source_buffer#insert
+ (fun () -> (s ())#source_view#source_buffer#insert
"apply rule (â¨#e (â¦) [â¦] (â¦) [â¦] (â¦));\n\t[\n\t|\n\t|\n\t]\n");
connect_button main#butNot_elim
- (fun () -> source_buffer#insert
+ (fun () -> (s ())#source_view#source_buffer#insert
"apply rule (¬#e (â¦) (â¦));\n\t[\n\t|\n\t]\n");
connect_button main#butBot_elim
- (fun () -> source_buffer#insert "apply rule (â¥#e (â¦));\n");
+ (fun () -> (s ())#source_view#source_buffer#insert "apply rule (â¥#e (â¦));\n");
connect_button main#butRAA
- (fun () -> source_buffer#insert "apply rule (RAA [â¦] (â¦));\n");
+ (fun () -> (s ())#source_view#source_buffer#insert "apply rule (RAA [â¦] (â¦));\n");
connect_button main#butUseLemma
- (fun () -> source_buffer#insert "apply rule (lem #premises name â¦);\n");
+ (fun () -> (s ())#source_view#source_buffer#insert "apply rule (lem #premises name â¦);\n");
connect_button main#butDischarge
- (fun () -> source_buffer#insert "apply rule (discharge [â¦]);\n");
+ (fun () -> (s ())#source_view#source_buffer#insert "apply rule (discharge [â¦]);\n");
connect_button main#butForall_intro
- (fun () -> source_buffer#insert "apply rule (â#i {â¦} (â¦));\n");
+ (fun () -> (s ())#source_view#source_buffer#insert "apply rule (â#i {â¦} (â¦));\n");
connect_button main#butForall_elim
- (fun () -> source_buffer#insert "apply rule (â#e {â¦} (â¦));\n");
+ (fun () -> (s ())#source_view#source_buffer#insert "apply rule (â#e {â¦} (â¦));\n");
connect_button main#butExists_intro
- (fun () -> source_buffer#insert "apply rule (â#i {â¦} (â¦));\n");
+ (fun () -> (s ())#source_view#source_buffer#insert "apply rule (â#i {â¦} (â¦));\n");
connect_button main#butExists_elim
- (fun () -> source_buffer#insert
+ (fun () -> (s ())#source_view#source_buffer#insert
"apply rule (â#e (â¦) {â¦} [â¦] (â¦));\n\t[\n\t|\n\t]\n");
@@ -848,10 +731,9 @@ class gui () =
MatitaGtkMisc.toggle_callback ~check:main#ppNotationMenuItem
~callback:(function b ->
let s = s () in
- let status =
- Interpretations.toggle_active_interpretations s#grafite_status b
+ let _status = Interpretations.toggle_active_interpretations s#status b
in
- assert false (* MATITA1.0 ???
+ assert false (* MATITA 1.0 ???
s#set_grafite_status status*)
);
MatitaGtkMisc.toggle_callback ~check:main#hideCoercionsMenuItem
@@ -862,103 +744,47 @@ class gui () =
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
| exn ->
if not (Helm_registry.get_bool "matita.debug") then
- notify_exn exn
+ (* MatitaScript.current is problably wrong, but what else
+ can we do? *)
+ notify_exn (MatitaScript.current ())#source_view exn
else raise exn);
- (* script *)
- let _ =
- source_buffer#set_language (Some MatitaGtkMisc.matita_lang);
- source_buffer#set_highlight_syntax true
- in
- let disableSave () =
- (s())#assignFileName None;
- main#saveMenuItem#misc#set_sensitive false
- in
- let saveAsScript () =
- let script = s () in
- match self#chooseFile ~ok_not_exists:true () with
- | Some f ->
- HExtlib.touch f;
- script#assignFileName (Some f);
- script#saveToFile ();
- console#message ("'"^f^"' saved.\n");
- self#_enableSaveTo f
- | None -> ()
- in
- let saveScript () =
- let script = s () in
- if script#has_name then
- (script#saveToFile ();
- console#message ("'"^script#filename^"' saved.\n"))
- else saveAsScript ()
- in
- let abandon_script () =
- let grafite_status = (s ())#grafite_status in
- if source_view#buffer#modified then
- (match ask_unsaved main#toplevel with
- | `YES -> saveScript ()
- | `NO -> ()
- | `CANCEL -> raise MatitaTypes.Cancel);
- save_moo grafite_status
- in
let loadScript () =
- let script = s () in
try
match self#chooseFile () with
- | Some f ->
- abandon_script ();
- script#reset ();
- script#assignFileName (Some f);
- source_view#source_buffer#begin_not_undoable_action ();
- script#loadFromFile f;
- source_view#source_buffer#end_not_undoable_action ();
- source_view#buffer#move_mark `INSERT source_view#buffer#start_iter;
- source_view#buffer#place_cursor source_view#buffer#start_iter;
- console#message ("'"^f^"' loaded.\n");
- self#_enableSaveTo f
+ | Some f -> self#loadScript f
| None -> ()
with MatitaTypes.Cancel -> ()
in
- let newScript () =
- abandon_script ();
- source_view#source_buffer#begin_not_undoable_action ();
- (s ())#reset ();
- (s ())#template ();
- source_view#source_buffer#end_not_undoable_action ();
- disableSave ()
- in
let cursor () =
- source_buffer#place_cursor
- (source_buffer#get_iter_at_mark (`NAME "locked")) in
- let advance _ = (MatitaScript.current ())#advance (); cursor () in
- let retract _ = (MatitaScript.current ())#retract (); cursor () in
- let top _ = (MatitaScript.current ())#goto `Top (); cursor () in
- let bottom _ = (MatitaScript.current ())#goto `Bottom (); cursor () in
- let jump _ = (MatitaScript.current ())#goto `Cursor (); cursor () in
- let advance = locker (keep_focus advance) in
- let retract = locker (keep_focus retract) in
- let top = locker (keep_focus top) in
- let bottom = locker (keep_focus bottom) in
- let jump = locker (keep_focus jump) in
+ let source_view = (s ())#source_view in
+ source_view#source_buffer#place_cursor
+ (source_view#source_buffer#get_iter_at_mark (`NAME "locked")) in
+ let advance (script: MatitaScript.script) = script#advance (); cursor () in
+ let retract (script: MatitaScript.script) = script#retract (); cursor () in
+ let top (script: MatitaScript.script) = script#goto `Top (); cursor () in
+ let bottom (script: MatitaScript.script) = script#goto `Bottom (); cursor () in
+ let jump (script: MatitaScript.script) = script#goto `Cursor (); cursor () in
+ let advance () = locker (keep_focus advance) (MatitaScript.current ()) in
+ let retract () = locker (keep_focus retract) (MatitaScript.current ()) in
+ let top () = locker (keep_focus top) (MatitaScript.current ()) in
+ let bottom () = locker (keep_focus bottom) (MatitaScript.current ()) in
+ let jump () = locker (keep_focus jump) (MatitaScript.current ()) in
(* quit *)
self#setQuitCallback (fun () ->
- let script = MatitaScript.current () in
- if source_view#buffer#modified then
- match ask_unsaved main#toplevel with
- | `YES ->
- saveScript ();
- save_moo script#grafite_status;
- GMain.Main.quit ()
- | `NO -> GMain.Main.quit ()
- | `CANCEL -> ()
- else
- (save_moo script#grafite_status;
- GMain.Main.quit ()));
+ let cancel = ref false in
+ MatitaScript.iter_scripts
+ (fun script ->
+ if not !cancel then
+ if not (self#closeScript0 script) then
+ cancel := true);
+ if not !cancel then
+ GMain.Main.quit ());
connect_button main#scriptAdvanceButton advance;
connect_button main#scriptRetractButton retract;
connect_button main#scriptTopButton top;
@@ -971,27 +797,20 @@ class gui () =
connect_menu_item main#scriptBottomMenuItem bottom;
connect_menu_item main#scriptJumpMenuItem jump;
connect_menu_item main#openMenuItem loadScript;
- connect_menu_item main#saveMenuItem saveScript;
- connect_menu_item main#saveAsMenuItem saveAsScript;
- connect_menu_item main#newMenuItem newScript;
+ connect_menu_item main#saveMenuItem
+ (fun () -> self#saveScript (MatitaScript.current ()));
+ connect_menu_item main#saveAsMenuItem
+ (fun () -> self#saveAsScript (MatitaScript.current ()));
+ 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));
- (* script monospace font stuff *)
- self#updateFontSize ();
+ (fun _ -> MatitaMathView.cicBrowser (Some (`About `TeX)));
(* debug menu *)
main#debugMenu#misc#hide ();
(* HBUGS *)
@@ -1001,8 +820,6 @@ class gui () =
main#hintMediumImage#set_file (image_path "matita-bulb-medium.png");
main#hintHighImage#set_file (image_path "matita-bulb-high.png");
*)
- (* focus *)
- self#sourceView#misc#grab_focus ();
(* main win dimension *)
let width = Gdk.Screen.width ~screen:(Gdk.Screen.default ()) () in
let height = Gdk.Screen.height ~screen:(Gdk.Screen.default ()) () in
@@ -1014,177 +831,29 @@ class gui () =
let script_w = main_w * 6 / 10 in
main#toplevel#resize ~width:main_w ~height:main_h;
main#hpaneScriptSequent#set_position script_w;
- (* source_view *)
- ignore(source_view#connect#after#paste_clipboard
- ~callback:(fun () -> (MatitaScript.current ())#clean_dirty_lock));
- (* clean_locked is set to true only "during" a PRIMARY paste
- operation (i.e. by clicking with the second mouse button) *)
- let clean_locked = ref false in
- ignore(source_view#event#connect#button_press
- ~callback:
- (fun button ->
- if GdkEvent.Button.button button = 2 then
- clean_locked := true;
- false
- ));
- ignore(source_view#event#connect#button_release
- ~callback:(fun button -> clean_locked := false; false));
- ignore(source_view#buffer#connect#after#apply_tag
- ~callback:(
- fun tag ~start:_ ~stop:_ ->
- if !clean_locked &&
- tag#get_oid = (MatitaScript.current ())#locked_tag#get_oid
- then
- begin
- clean_locked := false;
- (MatitaScript.current ())#clean_dirty_lock;
- clean_locked := true
- end));
(* math view handling *)
connect_menu_item main#newCicBrowserMenuItem (fun () ->
- ignore(MatitaMathView.cicBrowser ()));
- connect_menu_item main#increaseFontSizeMenuItem (fun () ->
- self#increaseFontSize ();
- MatitaMisc.increase_font_size ();
- MatitaMathView.update_font_sizes ());
- connect_menu_item main#decreaseFontSizeMenuItem (fun () ->
- self#decreaseFontSize ();
- MatitaMisc.decrease_font_size ();
- MatitaMathView.update_font_sizes ());
- connect_menu_item main#normalFontSizeMenuItem (fun () ->
- self#resetFontSize ();
- MatitaMisc.reset_font_size ();
- MatitaMathView.update_font_sizes ());
- MatitaMisc.reset_font_size ();
-
- (** selections / clipboards handling *)
-
- method markupSelected = MatitaMathView.has_selection ()
- method private textSelected =
- (source_buffer#get_iter_at_mark `INSERT)#compare
- (source_buffer#get_iter_at_mark `SEL_BOUND) <> 0
- method private somethingSelected = self#markupSelected || self#textSelected
- method private markupStored = MatitaMathView.has_clipboard ()
- method private textStored = clipboard#text <> None
- method private somethingStored = self#markupStored || self#textStored
-
- method canCopy = self#somethingSelected
- method canCut = self#textSelected
- method canDelete = self#textSelected
- method canPaste = self#somethingStored
- method canPastePattern = self#markupStored
-
- method copy () =
- if self#textSelected
- then begin
- MatitaMathView.empty_clipboard ();
- source_view#buffer#copy_clipboard clipboard;
- end else
- MatitaMathView.copy_selection ()
- method cut () =
- source_view#buffer#cut_clipboard clipboard;
- MatitaMathView.empty_clipboard ()
- method delete () = ignore (source_view#buffer#delete_selection ())
- method paste () =
- if MatitaMathView.has_clipboard ()
- then source_view#buffer#insert (MatitaMathView.paste_clipboard `Term)
- else source_view#buffer#paste_clipboard clipboard;
- (MatitaScript.current ())#clean_dirty_lock
- method pastePattern () =
- source_view#buffer#insert (MatitaMathView.paste_clipboard `Pattern)
-
- method private expand_virtual_if_any iter tok =
- try
- let len = MatitaGtkMisc.utf8_string_length tok in
- let last_word =
- let prev = iter#copy#backward_chars len in
- prev#get_slice ~stop:(prev#copy#backward_find_char
- (fun x -> Glib.Unichar.isspace x || x = Glib.Utf8.first_char "\\"))
- in
- let inplaceof, symb = Virtuals.symbol_of_virtual last_word in
- self#reset_similarsymbols;
- let s = Glib.Utf8.from_unichar symb in
- assert(Glib.Utf8.validate s);
- source_buffer#delete ~start:iter
- ~stop:(iter#copy#backward_chars
- (MatitaGtkMisc.utf8_string_length inplaceof + len));
- source_buffer#insert ~iter
- (if inplaceof.[0] = '\\' then s else (s ^ tok));
- true
- with Virtuals.Not_a_virtual -> false
-
- val similar_memory = Hashtbl.create 97
- val mutable old_used_memory = false
-
- method private nextSimilarSymbol () =
- let write_similarsymbol s =
- let s = Glib.Utf8.from_unichar s in
- let iter = source_buffer#get_iter_at_mark `INSERT in
- assert(Glib.Utf8.validate s);
- source_buffer#delete ~start:iter ~stop:(iter#copy#backward_chars 1);
- source_buffer#insert ~iter:(source_buffer#get_iter_at_mark `INSERT) s;
- (try source_buffer#delete_mark similarsymbols_tag
- with GText.No_such_mark _ -> ());
- ignore(source_buffer#create_mark ~name:similarsymbols_tag_name
- (source_buffer#get_iter_at_mark `INSERT));
- in
- let new_similarsymbol =
- try
- let iter_ins = source_buffer#get_iter_at_mark `INSERT in
- let iter_lig = source_buffer#get_iter_at_mark similarsymbols_tag in
- not (iter_ins#equal iter_lig)
- with GText.No_such_mark _ -> true
- in
- if new_similarsymbol then
- (if not(self#expand_virtual_if_any (source_buffer#get_iter_at_mark `INSERT) "")then
- let last_symbol =
- let i = source_buffer#get_iter_at_mark `INSERT in
- Glib.Utf8.first_char (i#get_slice ~stop:(i#copy#backward_chars 1))
- in
- (match Virtuals.similar_symbols last_symbol with
- | [] -> ()
- | eqclass ->
- similarsymbols_orig <- eqclass;
- let is_used =
- try Hashtbl.find similar_memory similarsymbols_orig
- with Not_found ->
- let is_used = List.map (fun x -> x,false) eqclass in
- Hashtbl.add similar_memory eqclass is_used;
- is_used
- in
- let hd, next, tl =
- let used, unused =
- List.partition (fun s -> List.assoc s is_used) eqclass
- in
- match used @ unused with a::b::c -> a,b,c | _ -> assert false
- in
- let hd, tl =
- if hd = last_symbol then next, tl @ [hd] else hd, (next::tl)
- in
- old_used_memory <- List.assoc hd is_used;
- let is_used =
- (hd,true) :: List.filter (fun (x,_) -> x <> hd) is_used
- in
- Hashtbl.replace similar_memory similarsymbols_orig is_used;
- write_similarsymbol hd;
- similarsymbols <- tl @ [ hd ]))
- else
- match similarsymbols with
- | [] -> ()
- | hd :: tl ->
- let is_used = Hashtbl.find similar_memory similarsymbols_orig in
- let last = HExtlib.list_last tl in
- let old_used_for_last = old_used_memory in
- old_used_memory <- List.assoc hd is_used;
- let is_used =
- (hd, true) :: (last,old_used_for_last) ::
- List.filter (fun (x,_) -> x <> last && x <> hd) is_used
- in
- Hashtbl.replace similar_memory similarsymbols_orig is_used;
- similarsymbols <- tl @ [ hd ];
- write_similarsymbol hd
+ 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 ->
+ self#save_page ();
+ current_page <- page;
+ let script = MatitaScript.at_page page in
+ script#activate;
+ main#undoMenuItem#misc#set_sensitive
+ script#source_view#source_buffer#can_undo ;
+ main#redoMenuItem#misc#set_sensitive
+ script#source_view#source_buffer#can_redo ;
+ main#saveMenuItem#misc#set_sensitive script#has_name))
method private externalEditor () =
+ let script = MatitaScript.current () in
+ let source_view = script#source_view in
let cmd = Helm_registry.get "matita.external_editor" in
(* ZACK uncomment to enable interactive ask of external editor command *)
(* let cmd =
@@ -1197,11 +866,10 @@ class gui () =
ask_text ~gui:self ~title:"External editor" ~msg ~multiline:false
~default:(Helm_registry.get "matita.external_editor") ()
in *)
- let script = MatitaScript.current () in
let fname = script#filename in
let slice mark =
- source_buffer#start_iter#get_slice
- ~stop:(source_buffer#get_iter_at_mark mark)
+ source_view#source_buffer#start_iter#get_slice
+ ~stop:(source_view#source_buffer#get_iter_at_mark mark)
in
let locked = `MARK script#locked_mark in
let string_pos mark = string_of_int (String.length (slice mark)) in
@@ -1214,21 +882,21 @@ class gui () =
cmd))
in
let locked_before = slice locked in
- let locked_offset = (source_buffer#get_iter_at_mark locked)#offset in
+ let locked_offset = (source_view#source_buffer#get_iter_at_mark locked)#offset in
ignore (Unix.system cmd);
- source_buffer#set_text (HExtlib.input_file fname);
- let locked_iter = source_buffer#get_iter (`OFFSET locked_offset) in
- source_buffer#move_mark locked locked_iter;
- source_buffer#apply_tag script#locked_tag
- ~start:source_buffer#start_iter ~stop:locked_iter;
+ source_view#source_buffer#set_text (HExtlib.input_file fname);
+ let locked_iter = source_view#source_buffer#get_iter (`OFFSET locked_offset) in
+ source_view#source_buffer#move_mark locked locked_iter;
+ source_view#source_buffer#apply_tag script#locked_tag
+ ~start:source_view#source_buffer#start_iter ~stop:locked_iter;
let locked_after = slice locked in
let line = ref 0 in
let col = ref 0 in
try
for i = 0 to String.length locked_before - 1 do
if locked_before.[i] <> locked_after.[i] then begin
- source_buffer#place_cursor
- ~where:(source_buffer#get_iter (`LINEBYTE (!line, !col)));
+ source_view#source_buffer#place_cursor
+ ~where:(source_view#source_buffer#get_iter (`LINEBYTE (!line, !col)));
script#goto `Cursor ();
raise Exit
end else if locked_before.[i] = '\n' then begin
@@ -1240,8 +908,98 @@ class gui () =
| Exit -> ()
| Invalid_argument _ -> script#goto `Bottom ()
+ method private saveAsScript script =
+ match self#chooseFile ~ok_not_exists:true () with
+ | Some f ->
+ HExtlib.touch f;
+ script#assignFileName (Some f);
+ script#saveToFile ();
+ console#message ("'"^f^"' saved.\n");
+ self#_enableSaveTo f
+ | None -> ()
+
+ method private saveScript script =
+ if script#has_name then
+ (script#saveToFile ();
+ console#message ("'"^script#filename^"' saved.\n"))
+ else self#saveAsScript script
+
+ (* returns false if closure is aborted by the user *)
+ method private closeScript0 script =
+ if script#source_view#buffer#modified then
+ match
+ ask_unsaved main#toplevel (Filename.basename script#filename)
+ with
+ | `YES ->
+ self#saveScript script;
+ save_moo script#status;
+ true
+ | `NO -> true
+ | `DELETE_EVENT -> false
+ else
+ (save_moo script#status; true)
+
+ method private closeScript page script =
+ if self#closeScript0 script then
+ begin
+ MatitaScript.destroy page;
+ ignore (main#scriptNotebook#remove_page page)
+ end
+
+ method private closeCurrentScript () =
+ let page = main#scriptNotebook#current_page 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 _ =
+ 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
+ closebutton#set_image image#coerce;
+ 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 scrolledWindow#coerce) script));
+ main#scriptNotebook#goto_page 0;
+ sequents_viewer#reset;
+ sequents_viewer#load_logo;
+ let browser_observer _ = MatitaMathView.refresh_all_browsers () in
+ let sequents_observer status =
+ sequents_viewer#reset;
+ match status#ng_mode with
+ `ProofMode ->
+ sequents_viewer#nload_sequents status;
+ (try
+ let goal =
+ Continuationals.Stack.find_goal status#stack
+ in
+ sequents_viewer#goto_sequent status goal
+ with Failure _ -> ());
+ | `CommandMode -> sequents_viewer#load_logo
+ in
+ script#addObserver sequents_observer;
+ script#addObserver browser_observer
+
method loadScript file =
- let script = MatitaScript.current () in
+ let page = main#scriptNotebook#current_page in
+ let script = MatitaScript.at_page page in
+ if script#source_view#buffer#modified || script#has_name then
+ self#newScript ();
+ let script = MatitaScript.current () in
+ let source_view = script#source_view in
script#reset ();
script#assignFileName (Some file);
let file = script#filename in
@@ -1256,185 +1014,79 @@ class gui () =
source_view#buffer#place_cursor source_view#buffer#start_iter;
console#message ("'"^file^"' loaded.");
self#_enableSaveTo file
-
- method private _enableSaveTo file =
+
+ method private _enableSaveTo _file =
self#main#saveMenuItem#misc#set_sensitive true
- method console = console
- method sourceView: GSourceView2.source_view =
- (source_view: GSourceView2.source_view)
- method fileSel = fileSel
- method findRepl = findRepl
+ method private console = console
+ 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 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 setQuitCallback callback =
+ method private setQuitCallback callback =
connect_menu_item main#quitMenuItem 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;
- _only_directory <- false;
- fileSel#fileSelectionWin#show ();
- GtkThread.main ();
- chosen_file
+ method private chooseFileOrDir ok_not_exists only_directory =
+ let fileSel = GWindow.file_chooser_dialog
+ ~action:`OPEN
+ ~title:"Select file"
+ ~modal:true
+ ~type_hint:`DIALOG
+ ~position:`CENTER
+ () in
+ fileSel#add_select_button_stock `OPEN `OK;
+ fileSel#add_button_stock `CANCEL `CANCEL;
+ ignore (fileSel#set_current_folder(Sys.getcwd ())) ;
+ let res =
+ let rec aux () =
+ match fileSel#run () with
+ | `OK ->
+ (match fileSel#filename with
+ None -> aux ()
+ | Some fname ->
+ if Sys.file_exists fname then
+ begin
+ if HExtlib.is_regular fname && not (only_directory) then
+ Some fname
+ else if only_directory && HExtlib.is_dir fname then
+ Some fname
+ else
+ aux ()
+ end
+ else if ok_not_exists then Some fname else aux ())
+ | `CANCEL -> None
+ | `DELETE_EVENT -> None in
+ aux () in
+ fileSel#destroy () ;
+ res
+
+ method private chooseFile ?(ok_not_exists = false) () =
+ self#chooseFileOrDir ok_not_exists false
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
+ self#chooseFileOrDir ok_not_exists true
- 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;
- MatitaMisc.set_gui g;
- g
+ let rg = (g :> MatitaGuiTypes.gui) in
+ MatitaMisc.set_gui rg;
+ g#newScript ();
+ rg
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
- 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
- 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
- (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 NReference.string_of_reference 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 uris));
- if ok_action = `AUTO then
- connect_button dialog#uriChoiceAutoButton (fun _ ->
- Helm_registry.set_bool "matita.auto_disambiguation" true;
- return (Some uris))
- else
- connect_button dialog#uriChoiceAutoButton (fun _ ->
- match model#easy_selection () with
- | [] -> ()
- | uris -> return (Some (List.map NReference.reference_of_string uris)));
- connect_button dialog#uriChoiceSelectedButton (fun _ ->
- match model#easy_selection () with
- | [] -> ()
- | uris -> return (Some (List.map NReference.reference_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
@@ -1485,68 +1137,65 @@ class interpModel =
let interactive_string_choice
- text prefix_len ?(title = "") ?(msg = "") () ~id locs uris
+ 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 ^ "" ^
- escape_pango_markup str2 ^ "" ^
- colorize stop tl
- in
+ GtkThread.sync (fun _ ->
+ 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 [] 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 ^ "" ^
+ escape_pango_markup str2 ^ "" ^
+ 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;
+ connect_button dialog#uriChoiceForwardButton (fun _ ->
+ match model#easy_selection () with
+ | [] -> ()
+ | uris -> choices := uris; dialog#toplevel#response `OK);
+ connect_button dialog#uriChoiceAbortButton (fun _ -> dialog#toplevel#response `DELETE_EVENT);
+ dialog#uriChoiceDialog#show ();
+ let res =
+ match dialog#toplevel#run () with
+ | `DELETE_EVENT -> dialog#toplevel#destroy() ; raise MatitaTypes.Cancel
+ | `OK -> !choices
+ | _ -> assert false in
+ dialog#toplevel#destroy () ;
+ res) ()
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;*)
@@ -1613,10 +1262,8 @@ let interactive_interp_choice () text prefix_len choices =
let _ =
(* disambiguator callbacks *)
Disambiguate.set_choose_uris_callback
- (fun ~selection_mode ?ok ?(enable_button_for_non_vars=false) ~title ~msg ->
+ (fun ~selection_mode ?ok ?enable_button_for_non_vars:(_=false) ~title ~msg ->
interactive_uri_choice ~selection_mode ?ok_label:ok ~title ~msg ());
Disambiguate.set_choose_interp_callback (interactive_interp_choice ());
(* gtk initialization *)
- GtkMain.Rc.add_default_file BuildTimeConf.gtkrc_file; (* loads gtk rc *)
- ignore (GMain.Main.init ())
-
+ GtkMain.Rc.add_default_file BuildTimeConf.gtkrc_file (* loads gtk rc *)