summaryrefslogtreecommitdiff
path: root/ide/coqide.ml
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
commit5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch)
tree631ad791a7685edafeb1fb2e8faeedc8379318ae /ide/coqide.ml
parentda178a880e3ace820b41d38b191d3785b82991f5 (diff)
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'ide/coqide.ml')
-rw-r--r--ide/coqide.ml4012
1 files changed, 1803 insertions, 2209 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml
index cc147d5e..201fbe47 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -7,123 +7,23 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: coqide.ml 12104 2009-04-24 18:10:10Z notin $ *)
+(* $Id$ *)
open Preferences
open Vernacexpr
open Coq
+open Gtk_parsing
open Ideutils
-
-let cb_ = ref None
-let cb () = ((Option.get !cb_):GData.clipboard)
-let last_cb_content = ref ""
-let (message_view:GText.view option ref) = ref None
-let (proof_view:GText.view option ref) = ref None
-
-let (_notebook:GPack.notebook option ref) = ref None
-let notebook () = Option.get !_notebook
+type ide_info = {
+ start : GText.mark;
+ stop : GText.mark;
+}
-let update_notebook_pos () =
- let pos =
- match !current.vertical_tabs, !current.opposite_tabs with
- | false, false -> `TOP
- | false, true -> `BOTTOM
- | true , false -> `LEFT
- | true , true -> `RIGHT
- in
- (notebook ())#set_tab_pos pos
-
-(* Tabs contain the name of the edited file and 2 status informations:
- Saved state + Focused proof buffer *)
-let decompose_tab w =
- let vbox = new GPack.box ((Gobject.try_cast w "GtkBox"):Gtk.box Gtk.obj) in
- let l = vbox#children in
- match l with
- | [img;lbl] ->
- let img = new GMisc.image
- ((Gobject.try_cast img#as_widget "GtkImage"):
- Gtk.image Gtk.obj)
- in
- let lbl = GMisc.label_cast lbl in
- vbox,img,lbl
- | _ -> assert false
-
-let set_tab_label i n =
- let nb = notebook () in
- let _,_,lbl = decompose_tab (nb#get_tab_label(nb#get_nth_page i))#as_widget
- in
- lbl#set_use_markup true;
- (* lbl#set_text n *) lbl#set_label n
-
-
-let set_tab_image ~icon i =
- let nb = notebook () in
- let _,img,_ = decompose_tab (nb#get_tab_label(nb#get_nth_page i))#as_widget
- in
- img#set_icon_size `SMALL_TOOLBAR;
- img#set_stock icon
-
-let set_current_tab_image ~icon = set_tab_image ~icon (notebook())#current_page
-
-let set_current_tab_label n = set_tab_label (notebook())#current_page n
-
-let get_tab_label i =
- let nb = notebook () in
- let _,_,lbl = decompose_tab (nb#get_tab_label(nb#get_nth_page i))#as_widget
- in
- lbl#text
-
-let get_full_tab_label i =
- let nb = notebook () in
- let _,_,lbl = decompose_tab (nb#get_tab_label(nb#get_nth_page i))#as_widget
- in
- lbl
-
-let get_current_tab_label () = get_tab_label (notebook())#current_page
-
-let get_current_page () =
- let i = (notebook())#current_page in
- (notebook())#get_nth_page i
-
-(* This function must remove "focused proof" decoration *)
-let reset_tab_label i =
- set_tab_label i (get_tab_label i)
-
-let to_do_on_page_switch = ref []
-
-module Vector = struct
- exception Found of int
- type 'a t = ('a option) array ref
- let create () = ref [||]
- let length t = Array.length !t
- let get t i = Option.get (Array.get !t i)
- let set t i v = Array.set !t i (Some v)
- let remove t i = Array.set !t i None
- let append t e = t := Array.append !t [|Some e|]; (Array.length !t)-1
- let iter f t = Array.iter (function | None -> () | Some x -> f x) !t
- let find_or_fail f t =
- let test i = function | None -> () | Some e -> if f e then raise (Found i) in
- Array.iteri test t
-
- let exists f t =
- let l = Array.length !t in
- let rec test i =
- (i < l) && (((!t.(i) <> None) && f (Option.get !t.(i))) || test (i+1))
- in
- test 0
-end
-type 'a viewable_script =
- {view : Undo.undoable_view;
- mutable analyzed_view : 'a option;
- }
-
-
-class type analyzed_views=
+class type analyzed_views=
object('self)
val mutable act_id : GtkSignal.id option
- val current_all : 'self viewable_script
val mutable deact_id : GtkSignal.id option
val input_buffer : GText.buffer
val input_view : Undo.undoable_view
@@ -133,6 +33,7 @@ object('self)
val message_view : GText.view
val proof_buffer : GText.buffer
val proof_view : GText.view
+ val cmd_stack : (ide_info * Coq.reset_info) Stack.t
val mutable is_active : bool
val mutable read_only : bool
val mutable filename : string option
@@ -145,7 +46,6 @@ object('self)
method add_detached_view : GWindow.window -> unit
method remove_detached_view : GWindow.window -> unit
- method view : Undo.undoable_view
method filename : string option
method stats : Unix.stats option
method set_filename : string option -> unit
@@ -184,7 +84,7 @@ object('self)
method send_to_coq :
bool -> bool -> string ->
bool -> bool -> bool ->
- (bool*(reset_info*(Util.loc * Vernacexpr.vernac_expr))) option
+ (bool*reset_info) option
method set_message : string -> unit
method show_pm_goal : unit
method show_goals : unit
@@ -192,37 +92,132 @@ object('self)
method undo_last_step : unit
method help_for_keyword : unit -> unit
method complete_at_offset : int -> bool
-
- method blaster : unit -> unit
end
-let (input_views:analyzed_views viewable_script Vector.t) = Vector.create ()
+
+type viewable_script =
+ {script : Undo.undoable_view;
+ tab_label : GMisc.label;
+ mutable filename : string;
+ mutable encoding : string;
+ proof_view : GText.view;
+ message_view : GText.view;
+ analyzed_view : analyzed_views;
+ command_stack : (ide_info * Coq.reset_info) Stack.t;
+ }
+
+
+let notebook_page_of_session {script=script;tab_label=bname;proof_view=proof;message_view=message} =
+ let session_paned =
+ GPack.paned `HORIZONTAL ~border_width:5 () in
+ let script_frame =
+ GBin.frame ~shadow_type:`IN ~packing:session_paned#add1 () in
+ let script_scroll =
+ GBin.scrolled_window ~vpolicy:`AUTOMATIC ~hpolicy:`AUTOMATIC ~packing:script_frame#add () in
+ let state_paned =
+ GPack.paned `VERTICAL ~packing:session_paned#add2 () in
+ let proof_frame =
+ GBin.frame ~shadow_type:`IN ~packing:state_paned#add1 () in
+ let proof_scroll =
+ GBin.scrolled_window ~vpolicy:`AUTOMATIC ~hpolicy:`AUTOMATIC ~packing:proof_frame#add () in
+ let message_frame =
+ GBin.frame ~shadow_type:`IN ~packing:state_paned#add2 () in
+ let message_scroll =
+ GBin.scrolled_window ~vpolicy:`AUTOMATIC ~hpolicy:`AUTOMATIC ~packing:message_frame#add () in
+ let session_tab =
+ GPack.hbox ~homogeneous:false () in
+ let img =
+ GMisc.image ~packing:session_tab#pack ~icon_size:`SMALL_TOOLBAR () in
+ let _ =
+ script#buffer#connect#modified_changed
+ ~callback:(fun () -> if script#buffer#modified
+ then img#set_stock `SAVE
+ else img#set_stock `YES) in
+ let _ =
+ session_paned#misc#connect#size_allocate
+ (let old_paned_width = ref 2 in
+ let old_paned_height = ref 2 in
+ (fun {Gtk.width=paned_width;Gtk.height=paned_height} ->
+ if !old_paned_width <> paned_width || !old_paned_height <> paned_height then (
+ session_paned#set_position (session_paned#position * paned_width / !old_paned_width);
+ state_paned#set_position (state_paned#position * paned_height / !old_paned_height);
+ old_paned_width := paned_width;
+ old_paned_height := paned_height;
+ ))) in
+ script_scroll#add script#coerce;
+ proof_scroll#add proof#coerce;
+ message_scroll#add message#coerce;
+ session_tab#pack bname#coerce;
+ img#set_stock `YES;
+ session_paned#set_position 1;
+ state_paned#set_position 1;
+ (Some session_tab#coerce,None,session_paned#coerce)
+
+let session_notebook =
+ Typed_notebook.create notebook_page_of_session ~border_width:2 ~show_border:false ~scrollable:true ()
+
+let active_view = ref (~-1)
+
+let on_active_view f =
+ if !active_view < 0
+ then failwith "no active view !"
+ else f (session_notebook#get_nth_term !active_view)
+
+let cb = GData.clipboard Gdk.Atom.primary
+
+
+let last_cb_content = ref ""
-let signals_to_crash = [Sys.sigabrt; Sys.sigalrm; Sys.sigfpe; Sys.sighup;
- Sys.sigill; Sys.sigpipe; Sys.sigquit;
+let update_notebook_pos () =
+ let pos =
+ match !current.vertical_tabs, !current.opposite_tabs with
+ | false, false -> `TOP
+ | false, true -> `BOTTOM
+ | true , false -> `LEFT
+ | true , true -> `RIGHT
+ in
+ session_notebook#set_tab_pos pos
+
+
+let set_active_view i =
+ prerr_endline "entering set_active_view";
+ (try on_active_view (fun {tab_label=lbl} -> lbl#set_text lbl#text) with _ -> ());
+ session_notebook#goto_page i;
+ let s = session_notebook#current_term in
+ s.tab_label#set_use_markup true;
+ s.tab_label#set_label ("<span background=\"light green\">"^s.tab_label#text^"</span>");
+ active_view := i;
+ prerr_endline "exiting set_active_view"
+
+
+
+let to_do_on_page_switch = ref []
+
+
+let signals_to_crash = [Sys.sigabrt; Sys.sigalrm; Sys.sigfpe; Sys.sighup;
+ Sys.sigill; Sys.sigpipe; Sys.sigquit;
(* Sys.sigsegv; Sys.sigterm;*) Sys.sigusr2]
let crash_save i =
(* ignore (Unix.sigprocmask Unix.SIG_BLOCK signals_to_crash);*)
Pervasives.prerr_endline "Trying to save all buffers in .crashcoqide files";
- let count = ref 0 in
- Vector.iter
- (function {view=view; analyzed_view = Some av } ->
- (let filename = match av#filename with
- | None ->
- incr count;
+ let count = ref 0 in
+ List.iter
+ (function {script=view; analyzed_view = av } ->
+ (let filename = match av#filename with
+ | None ->
+ incr count;
"Unnamed_coqscript_"^(string_of_int !count)^".crashcoqide"
| Some f -> f^".crashcoqide"
in
- try
+ try
if try_export filename (view#buffer#get_text ()) then
Pervasives.prerr_endline ("Saved "^filename)
else Pervasives.prerr_endline ("Could not save "^filename)
with _ -> Pervasives.prerr_endline ("Could not save "^filename))
- | _ -> Pervasives.prerr_endline "Unanalyzed view found. Please report."
)
- input_views;
+ session_notebook#pages;
Pervasives.prerr_endline "Done. Please report.";
if i <> 127 then exit i
@@ -240,9 +235,9 @@ let coq_computing = Mutex.create ()
(* To prevent Coq from interrupting during undoing...*)
let coq_may_stop = Mutex.create ()
-let break () =
+let break () =
prerr_endline "User break received:";
- if not (Mutex.try_lock coq_computing) then
+ if not (Mutex.try_lock coq_computing) then
begin
prerr_endline " trying to stop computation:";
if Mutex.try_lock coq_may_stop then begin
@@ -256,225 +251,110 @@ let break () =
prerr_endline " ignored (not computing)"
end
-let do_if_not_computing text f x =
- let threaded_task () =
- if Mutex.try_lock coq_computing
- then
- begin
- let w = Blaster_window.blaster_window () in
- if not (Mutex.try_lock w#lock) then
- begin
- break ();
- let lck = Mutex.create () in
- Mutex.lock lck;
- prerr_endline "Waiting on blaster...";
- Condition.wait w#blaster_killed lck;
- prerr_endline "Waiting on blaster ok";
- Mutex.unlock lck
- end
- else
- Mutex.unlock w#lock;
- let idle =
- Glib.Timeout.add ~ms:300
- ~callback:(fun () -> async !pulse ();true) in
- begin
- prerr_endline "Getting lock";
- try
- f x;
- Glib.Timeout.remove idle;
- prerr_endline "Releasing lock";
- Mutex.unlock coq_computing;
- with e ->
- Glib.Timeout.remove idle;
- prerr_endline "Releasing lock (on error)";
- Mutex.unlock coq_computing;
- raise e
- end
- end
- else
- prerr_endline
- "Discarded order (computations are ongoing)"
- in
- prerr_endline ("Launching thread " ^ text);
- ignore (Thread.create threaded_task ())
-
-let add_input_view tv =
- Vector.append input_views tv
-
-let get_input_view i =
- if 0 <= i && i < Vector.length input_views
- then
- Vector.get input_views i
- else raise Not_found
-
-let active_view = ref None
-
-let get_active_view () = Vector.get input_views (Option.get !active_view)
-
-let set_active_view i =
- (match !active_view with None -> () | Some i ->
- reset_tab_label i);
- (notebook ())#goto_page i;
- let txt = get_current_tab_label () in
- set_current_tab_label ("<span background=\"light green\">"^txt^"</span>");
- active_view := Some i
-
-let set_current_view i = (notebook ())#goto_page i
-
-let kill_input_view i =
- let v = Vector.get input_views i in
- (match v.analyzed_view with
- | Some v -> v#kill_detached_views ()
- | None -> ());
- v.view#destroy ();
- v.analyzed_view <- None;
- Vector.remove input_views i
-
-let get_current_view_page () = (notebook ())#current_page
-let get_current_view () = Vector.get input_views (notebook ())#current_page
-let remove_current_view_page () =
- let c = (notebook ())#current_page in
- kill_input_view c;
- ((notebook ())#get_nth_page c)#misc#hide ()
-
-let is_word_char c =
- (* TODO: avoid num and prime at the head of a word *)
- Glib.Unichar.isalnum c || c = underscore || c = prime
-
-let starts_word it =
- prerr_endline ("Starts word ? '"^(Glib.Utf8.from_unichar it#char)^"'");
- (not it#copy#nocopy#backward_char ||
- (let c = it#backward_char#char in
- not (is_word_char c)))
-
-let ends_word it =
- (not it#copy#nocopy#forward_char ||
- let c = it#forward_char#char in
- not (is_word_char c)
- )
-
-let inside_word it =
- let c = it#char in
- not (starts_word it) &&
- not (ends_word it) &&
- is_word_char c
-
-let is_on_word_limit it = inside_word it || ends_word it
-
-let rec find_word_start it =
- prerr_endline "Find word start";
- if not it#nocopy#backward_char then
- (prerr_endline "find_word_start: cannot backward"; it)
- else if is_word_char it#char
- then find_word_start it
- else (it#nocopy#forward_char;
- prerr_endline ("Word start at: "^(string_of_int it#offset));it)
-let find_word_start (it:GText.iter) = find_word_start it#copy
-
-let rec find_word_end it =
- prerr_endline "Find word end";
- if let c = it#char in c<>0 && is_word_char c
- then begin
- ignore (it#nocopy#forward_char);
- find_word_end it
- end else (prerr_endline ("Word end at: "^(string_of_int it#offset));it)
-let find_word_end it = find_word_end it#copy
-
-
-let get_word_around it =
- let start = find_word_start it in
- let stop = find_word_end it in
- start,stop
-
-
-let rec complete_backward w (it:GText.iter) =
- prerr_endline "Complete backward...";
- match it#backward_search w with
- | None -> (prerr_endline "backward_search failed";None)
- | Some (start,stop) ->
- prerr_endline ("complete_backward got a match:"^(string_of_int start#offset)^(string_of_int stop#offset));
- if starts_word start then
- let ne = find_word_end stop in
- if ne#compare stop = 0
- then complete_backward w start
- else Some (start,stop,ne)
- else complete_backward w start
-
-let rec complete_forward w (it:GText.iter) =
- prerr_endline "Complete forward...";
- match it#forward_search w with
- | None -> None
- | Some (start,stop) ->
- if starts_word start then
- let ne = find_word_end stop in
- if ne#compare stop = 0 then
- complete_forward w stop
- else Some (stop,stop,ne)
- else complete_forward w stop
+let do_if_not_computing text f x =
+ if Mutex.try_lock coq_computing then
+ let threaded_task () =
+ prerr_endline "Getting lock";
+ try
+ f x;
+ prerr_endline "Releasing lock";
+ Mutex.unlock coq_computing;
+ with e ->
+ prerr_endline "Releasing lock (on error)";
+ Mutex.unlock coq_computing;
+ raise e
+ in
+ prerr_endline ("Launching thread " ^ text);
+ ignore (Glib.Timeout.add ~ms:300 ~callback:
+ (fun () -> if Mutex.try_lock coq_computing
+ then (Mutex.unlock coq_computing; false)
+ else (pbar#pulse (); true)));
+ ignore (Thread.create threaded_task ())
+ else
+ prerr_endline
+ "Discarded order (computations are ongoing)"
+
+(* XXX - 1 appel *)
+let kill_input_view i =
+ let v = session_notebook#get_nth_term i in
+ v.analyzed_view#kill_detached_views ();
+ v.script#destroy ();
+ v.tab_label#destroy ();
+ v.proof_view#destroy ();
+ v.message_view#destroy ();
+ session_notebook#remove_page i
+(*
+(* XXX - beaucoups d'appels, a garder *)
+let get_current_view =
+ focused_session
+ *)
+let remove_current_view_page () =
+ let c = session_notebook#current_page in
+ kill_input_view c
+
(* Reset this to None on page change ! *)
let (last_completion:(string*int*int*bool) option ref) = ref None
-let () = to_do_on_page_switch :=
+let () = to_do_on_page_switch :=
(fun i -> last_completion := None)::!to_do_on_page_switch
let rec complete input_buffer w (offset:int) =
- match !last_completion with
+ match !last_completion with
| Some (lw,loffset,lpos,backward)
when lw=w && loffset=offset ->
begin
let iter = input_buffer#get_iter (`OFFSET lpos) in
- if backward then
+ if backward then
match complete_backward w iter with
- | None ->
- last_completion :=
+ | None ->
+ last_completion :=
Some (lw,loffset,
- (find_word_end
+ (find_word_end
(input_buffer#get_iter (`OFFSET loffset)))#offset ,
- false);
+ false);
None
- | Some (ss,start,stop) as result ->
- last_completion :=
+ | Some (ss,start,stop) as result ->
+ last_completion :=
Some (w,offset,ss#offset,true);
result
else
match complete_forward w iter with
- | None ->
+ | None ->
last_completion := None;
None
- | Some (ss,start,stop) as result ->
- last_completion :=
+ | Some (ss,start,stop) as result ->
+ last_completion :=
Some (w,offset,ss#offset,false);
result
end
| _ -> begin
match complete_backward w (input_buffer#get_iter (`OFFSET offset)) with
- | None ->
- last_completion :=
+ | None ->
+ last_completion :=
Some (w,offset,(find_word_end (input_buffer#get_iter
(`OFFSET offset)))#offset,false);
complete input_buffer w offset
- | Some (ss,start,stop) as result ->
+ | Some (ss,start,stop) as result ->
last_completion := Some (w,offset,ss#offset,true);
result
end
-
+
let get_current_word () =
- let av = Option.get ((get_current_view ()).analyzed_view) in
- match (cb ())#text with
- | None ->
+ match session_notebook#current_term,cb#text with
+ | {script=script; analyzed_view=av;},None ->
prerr_endline "None selected";
let it = av#get_insert in
let start = find_word_start it in
let stop = find_word_end start in
- av#view#buffer#move_mark `SEL_BOUND start;
- av#view#buffer#move_mark `INSERT stop;
- av#view#buffer#get_text ~slice:true ~start ~stop ()
- | Some t ->
+ script#buffer#move_mark `SEL_BOUND start;
+ script#buffer#move_mark `INSERT stop;
+ script#buffer#get_text ~slice:true ~start ~stop ()
+ | _,Some t ->
prerr_endline "Some selected";
prerr_endline t;
t
-
+
let input_channel b ic =
let buf = String.create 1024 and len = ref 0 in
@@ -488,142 +368,6 @@ let with_file handler name ~f =
try f ic; close_in ic with e -> close_in ic; raise e
with Sys_error s -> handler s
-type info = {start:GText.mark;
- stop:GText.mark;
- ast:Util.loc * Vernacexpr.vernac_expr;
- reset_info:Coq.reset_info
- }
-
-exception Size of int
-let (processed_stack:info Stack.t) = Stack.create ()
-let push x = Stack.push x processed_stack
-let pop () = try Stack.pop processed_stack with Stack.Empty -> raise (Size 0)
-let top () = try Stack.top processed_stack with Stack.Empty -> raise (Size 0)
-let is_empty () = Stack.is_empty processed_stack
-
-(* push a new Coq phrase *)
-
-let update_on_end_of_segment id =
- let lookup_section = function
- | { reset_info = ResetAtSegmentStart id',_,_ } when id = id' -> raise Exit
- | { reset_info = _,_,r } -> r := false
- in
- try Stack.iter lookup_section processed_stack with Exit -> ()
-
-let push_phrase reset_info start_of_phrase_mark end_of_phrase_mark ast =
- let x = {start = start_of_phrase_mark;
- stop = end_of_phrase_mark;
- ast = ast;
- reset_info = reset_info
- } in
- begin
- match snd ast with
- | VernacEndSegment (_,id) ->
- prerr_endline "Updating on end of segment 1";
- update_on_end_of_segment id
- | _ -> ()
- end;
- push x
-
-
-let repush_phrase reset_info x =
- let x = { x with reset_info = reset_info } in
- begin
- match snd x.ast with
- | VernacEndSegment (_,id) ->
- prerr_endline "Updating on end of segment 2";
- update_on_end_of_segment id
- | _ -> ()
- end;
- push x
-
-type backtrack =
-| BacktrackToNextActiveMark
-| BacktrackToMark of reset_mark
-| BacktrackToModSec of Names.identifier
-| NoBacktrack
-
-let add_undo = function (n,a,b,p,l as x) -> if p = 0 then (n+1,a,b,p,l) else x
-let add_abort = function
- | (n,a,b,0,l) -> (0,a+1,b,0,l)
- | (n,a,b,p,l) -> (n,a,b,p-1,l)
-let add_qed q (n,a,b,p,l as x) =
- if q = 0 then x else (n,a,BacktrackToNextActiveMark,p+q,l)
-let add_backtrack (n,a,b,p,l) b' = (n,a,b',p,l)
-
-let update_proofs (n,a,b,p,cur_lems) prev_lems =
- let ncommon = List.length (Util.list_intersect cur_lems prev_lems) in
- let openproofs = List.length cur_lems - ncommon in
- let closedproofs = List.length prev_lems - ncommon in
- let undos = (n,a,b,p,prev_lems) in
- add_qed closedproofs (Util.iterate add_abort openproofs undos)
-
-let pop_command undos t =
- let (state_info,undo_info,section_info) = t.reset_info in
- let undos =
- if !section_info then
- let undos = update_proofs undos undo_info in
- match state_info with
- | _ when is_vernac_tactic_command (snd t.ast) ->
- (* A tactic, active if not below a Qed *)
- add_undo undos
- | ResetAtRegisteredObject mark ->
- add_backtrack undos (BacktrackToMark mark)
- | ResetAtSegmentStart id ->
- add_backtrack undos (BacktrackToModSec id)
- | _ when is_vernac_state_preserving_command (snd t.ast) ->
- undos
- | _ ->
- add_backtrack undos BacktrackToNextActiveMark
- else
- begin
- prerr_endline "In section";
- (* An object inside a closed section *)
- add_backtrack undos BacktrackToNextActiveMark
- end in
- ignore (pop ());
- undos
-
-let apply_aborts a =
- if a <> 0 then prerr_endline ("Applying "^string_of_int a^" aborts");
- try Util.repeat a Pfedit.delete_current_proof ()
- with e -> prerr_endline "WARNING : found a closed environment"; raise e
-
-exception UndoStackExhausted
-
-let apply_tactic_undo n =
- if n<>0 then
- (prerr_endline ("Applying "^string_of_int n^" undos");
- try Pfedit.undo n with _ -> raise UndoStackExhausted)
-
-let apply_reset = function
- | BacktrackToMark mark -> reset_to mark
- | BacktrackToModSec id -> reset_to_mod id
- | NoBacktrack -> ()
- | BacktrackToNextActiveMark -> assert false
-
-let rec apply_undos (n,a,b,p,l as undos) =
- if p = 0 & b <> BacktrackToNextActiveMark then
- begin
- apply_aborts a;
- try
- apply_tactic_undo n;
- apply_reset b
- with UndoStackExhausted ->
- apply_undos (n,0,BacktrackToNextActiveMark,p,l)
- end
- else
- (* re-synchronize Coq to the current state of the stack *)
- if is_empty () then
- Coq.reset_initial ()
- else
- begin
- let t = top () in
- apply_undos (pop_command undos t);
- let reset_info = Coq.compute_reset_info (snd t.ast) in
- interp_last t.ast;
- repush_phrase reset_info t
- end
(* For electric handlers *)
exception Found
@@ -631,19 +375,16 @@ exception Found
(* For find_phrase_starting_at *)
exception Stop of int
-let activate_input i =
- (match !active_view with
- | None -> ()
- | Some n ->
- let a_v = Option.get (Vector.get input_views n).analyzed_view in
- a_v#deactivate ();
- a_v#reset_initial
- );
- let activate_function = (Option.get (Vector.get input_views i).analyzed_view)#activate in
- activate_function ();
- set_active_view i
-
-let warning msg =
+(* XXX *)
+let activate_input i =
+ prerr_endline "entering activate_input";
+ (try on_active_view (fun {analyzed_view=a_v} -> a_v#reset_initial; a_v#deactivate ())
+ with _ -> ());
+ (session_notebook#get_nth_term i).analyzed_view#activate ();
+ set_active_view i;
+ prerr_endline "exiting activate_input"
+
+let warning msg =
GToolbox.message_box ~title:"Warning"
~icon:(let img = GMisc.image () in
img#set_stock `DIALOG_WARNING;
@@ -651,30 +392,142 @@ let warning msg =
img#coerce)
msg
-
-class analyzed_view index =
- let {view = input_view_} as current_all_ = get_input_view index in
- let proof_view_ = Option.get !proof_view in
- let message_view_ = Option.get !message_view in
+let apply_tag (buffer:GText.buffer) orig off_conv from upto sort =
+ let conv_and_apply start stop tag =
+ let start = orig#forward_chars (off_conv from) in
+ let stop = orig#forward_chars (off_conv upto) in
+ buffer#apply_tag ~start ~stop tag
+ in match sort with
+ | Coq_lex.Comment ->
+ conv_and_apply from upto Tags.Script.comment
+ | Coq_lex.Keyword ->
+ conv_and_apply from upto Tags.Script.kwd
+ | Coq_lex.Declaration ->
+ conv_and_apply from upto Tags.Script.decl
+ | Coq_lex.ProofDeclaration ->
+ conv_and_apply from upto Tags.Script.proof_decl
+ | Coq_lex.Qed ->
+ conv_and_apply from upto Tags.Script.qed
+ | Coq_lex.String -> ()
+
+let remove_tags (buffer:GText.buffer) from upto =
+ List.iter (buffer#remove_tag ~start:from ~stop:upto)
+ [ Tags.Script.comment; Tags.Script.kwd; Tags.Script.decl;
+ Tags.Script.proof_decl; Tags.Script.qed ]
+
+let split_slice_lax (buffer:GText.buffer) from upto =
+ remove_tags buffer from upto;
+ buffer#remove_tag ~start:from ~stop:upto Tags.Script.lax_end;
+ let slice = buffer#get_text ~start:from ~stop:upto () in
+ let slice = slice ^ " " in
+ let rec split_substring str =
+ let off_conv = byte_offset_to_char_offset str in
+ let slice_len = String.length str in
+ let sentence_len = Coq_lex.find_end_offset (apply_tag buffer from off_conv) str in
+
+ let stop = from#forward_chars (pred (off_conv sentence_len)) in
+ let start = stop#backward_char in
+ buffer#apply_tag ~start ~stop Tags.Script.lax_end;
+
+ if 1 < slice_len - sentence_len then begin (* remember that we added a trailing space *)
+ ignore (from#nocopy#forward_chars (off_conv sentence_len));
+ split_substring (String.sub str sentence_len (slice_len - sentence_len))
+ end
+ in
+ split_substring slice
+
+let rec grab_safe_sentence_start (iter:GText.iter) soi =
+ let lax_back = iter#backward_char#has_tag Tags.Script.lax_end in
+ let on_space = List.mem iter#char [0x09;0x0A;0x20] in
+ let full_ending = iter#is_start || (lax_back & on_space) in
+ if full_ending then iter
+ else if iter#compare soi <= 0 then raise Not_found
+ else
+ let prev = iter#backward_to_tag_toggle (Some Tags.Script.lax_end) in
+ (if prev#has_tag Tags.Script.lax_end then
+ ignore (prev#nocopy#backward_to_tag_toggle (Some Tags.Script.lax_end)));
+ grab_safe_sentence_start prev soi
+
+let grab_sentence_end_from (start:GText.iter) =
+ let stop = start#forward_to_tag_toggle (Some Tags.Script.lax_end) in
+ stop#forward_char
+
+let get_sentence_bounds (iter:GText.iter) =
+ let start = iter#backward_to_tag_toggle (Some Tags.Script.lax_end) in
+ (if start#has_tag Tags.Script.lax_end then ignore (
+ start#nocopy#backward_to_tag_toggle (Some Tags.Script.lax_end)));
+ let stop = start#forward_to_tag_toggle (Some Tags.Script.lax_end) in
+ let stop = stop#forward_char in
+ start,stop
+
+let end_tag_present end_iter =
+ end_iter#backward_char#has_tag Tags.Script.lax_end
+
+let tag_on_insert =
+ let skip_last = ref (ref true) in (* ref to the mutable flag created on last call *)
+ fun buffer ->
+ try
+ let insert = buffer#get_iter_at_mark `INSERT in
+ let start = grab_safe_sentence_start insert
+ (buffer#get_iter_at_mark (`NAME "start_of_input")) in
+ let stop = grab_sentence_end_from insert in
+ let skip_curr = ref true in (* shall the callback be skipped ? by default yes*)
+ (!skip_last) := true; (* skip the previously created callback *)
+ skip_last := skip_curr;
+ try split_slice_lax buffer start stop
+ with Not_found ->
+ skip_curr := false;
+ ignore (Glib.Timeout.add ~ms:1500
+ ~callback:(fun () -> if not !skip_curr then (
+ try split_slice_lax buffer start buffer#end_iter with _ -> ()); false))
+ with Not_found ->
+ let err_pos = buffer#get_iter_at_mark (`NAME "start_of_input") in
+ buffer#apply_tag Tags.Script.error ~start:err_pos ~stop:err_pos#forward_char
+
+let force_retag buffer =
+ try split_slice_lax buffer buffer#start_iter buffer#end_iter with _ -> ()
+
+let toggle_proof_visibility (buffer:GText.buffer) (cursor:GText.iter) =
+ (* move back twice if not into proof_decl,
+ * once if into proof_decl and back_char into_proof_decl,
+ * don't move if into proof_decl and back_char not into proof_decl *)
+ if not (cursor#has_tag Tags.Script.proof_decl) then
+ ignore (cursor#nocopy#backward_to_tag_toggle (Some Tags.Script.proof_decl));
+ if cursor#backward_char#has_tag Tags.Script.proof_decl then
+ ignore (cursor#nocopy#backward_to_tag_toggle (Some Tags.Script.proof_decl));
+ let decl_start = cursor in
+ let prf_end = decl_start#forward_to_tag_toggle (Some Tags.Script.qed) in
+ let decl_end = grab_sentence_end_from decl_start in
+ let prf_end = grab_sentence_end_from prf_end in
+ let prf_end = prf_end#forward_char in
+ if decl_start#has_tag Tags.Script.folded then (
+ buffer#remove_tag ~start:decl_start ~stop:decl_end Tags.Script.folded;
+ buffer#remove_tag ~start:decl_end ~stop:prf_end Tags.Script.hidden)
+ else (
+ buffer#apply_tag ~start:decl_start ~stop:decl_end Tags.Script.folded;
+ buffer#apply_tag ~start:decl_end ~stop:prf_end Tags.Script.hidden)
+
+class analyzed_view (_script:Undo.undoable_view) (_pv:GText.view) (_mv:GText.view) _cs =
object(self)
- val current_all = current_all_
- val input_view = current_all_.view
- val proof_view = Option.get !proof_view
- val message_view = Option.get !message_view
- val input_buffer = input_view_#buffer
- val proof_buffer = proof_view_#buffer
- val message_buffer = message_view_#buffer
+ val input_view = _script
+ val input_buffer = _script#buffer
+ val proof_view = _pv
+ val proof_buffer = _pv#buffer
+ val message_view = _mv
+ val message_buffer = _mv#buffer
+ val cmd_stack = _cs
val mutable is_active = false
val mutable read_only = false
- val mutable filename = None
+ val mutable filename = None
val mutable stats = None
val mutable last_modification_time = 0.
val mutable last_auto_save_time = 0.
val mutable detached_views = []
val mutable auto_complete_on = !current.auto_complete
+ val hidden_proofs = Hashtbl.create 32
- method private toggle_auto_complete =
+ method private toggle_auto_complete =
auto_complete_on <- not auto_complete_on
method set_auto_complete t = auto_complete_on <- t
method without_auto_complete : 'a 'b. ('a -> 'b) -> 'a -> 'b = fun f x ->
@@ -683,131 +536,130 @@ object(self)
let y = f x in
self#set_auto_complete old;
y
- method add_detached_view (w:GWindow.window) =
+ method add_detached_view (w:GWindow.window) =
detached_views <- w::detached_views
- method remove_detached_view (w:GWindow.window) =
+ method remove_detached_view (w:GWindow.window) =
detached_views <- List.filter (fun e -> w#misc#get_oid<>e#misc#get_oid) detached_views
- method kill_detached_views () =
+ method kill_detached_views () =
List.iter (fun w -> w#destroy ()) detached_views;
detached_views <- []
- method view = input_view
method filename = filename
method stats = stats
- method set_filename f =
+ method set_filename f =
filename <- f;
- match f with
+ match f with
| Some f -> stats <- my_stat f
| None -> ()
- method update_stats =
- match filename with
- | Some f -> stats <- my_stat f
+ method update_stats =
+ match filename with
+ | Some f -> stats <- my_stat f
| _ -> ()
- method revert =
- match filename with
+ method revert =
+ match filename with
| Some f -> begin
- let do_revert () = begin
- !push_info "Reverting buffer";
- try
- if is_active then self#reset_initial;
- let b = Buffer.create 1024 in
- with_file !flash_info f ~f:(input_channel b);
- let s = try_convert (Buffer.contents b) in
- input_buffer#set_text s;
- self#update_stats;
- input_buffer#place_cursor input_buffer#start_iter;
- input_buffer#set_modified false;
- !pop_info ();
- !flash_info "Buffer reverted";
- Highlight.highlight_all input_buffer;
- with _ ->
- !pop_info ();
- !flash_info "Warning: could not revert buffer";
- end
- in
- if input_buffer#modified then
- match (GToolbox.question_box
- ~title:"Modified buffer changed on disk"
- ~buttons:["Revert from File";
- "Overwrite File";
- "Disable Auto Revert"]
- ~default:0
- ~icon:(stock_to_widget `DIALOG_WARNING)
- "Some unsaved buffers changed on disk"
- )
- with 1 -> do_revert ()
- | 2 -> if self#save f then !flash_info "Overwritten" else
- !flash_info "Could not overwrite file"
- | _ ->
- prerr_endline "Auto revert set to false";
- !current.global_auto_revert <- false;
- disconnect_revert_timer ()
- else do_revert ()
- end
+ let do_revert () = begin
+ push_info "Reverting buffer";
+ try
+ if is_active then self#reset_initial;
+ let b = Buffer.create 1024 in
+ with_file flash_info f ~f:(input_channel b);
+ let s = try_convert (Buffer.contents b) in
+ input_buffer#set_text s;
+ self#update_stats;
+ input_buffer#place_cursor input_buffer#start_iter;
+ input_buffer#set_modified false;
+ pop_info ();
+ flash_info "Buffer reverted";
+ force_retag input_buffer;
+ with _ ->
+ pop_info ();
+ flash_info "Warning: could not revert buffer";
+ end
+ in
+ if input_buffer#modified then
+ match (GToolbox.question_box
+ ~title:"Modified buffer changed on disk"
+ ~buttons:["Revert from File";
+ "Overwrite File";
+ "Disable Auto Revert"]
+ ~default:0
+ ~icon:(stock_to_widget `DIALOG_WARNING)
+ "Some unsaved buffers changed on disk"
+ )
+ with 1 -> do_revert ()
+ | 2 -> if self#save f then flash_info "Overwritten" else
+ flash_info "Could not overwrite file"
+ | _ ->
+ prerr_endline "Auto revert set to false";
+ !current.global_auto_revert <- false;
+ disconnect_revert_timer ()
+ else do_revert ()
+ end
| None -> ()
-
- method save f =
+
+ method save f =
if try_export f (input_buffer#get_text ()) then begin
- filename <- Some f;
- input_buffer#set_modified false;
- stats <- my_stat f;
- (match self#auto_save_name with
- | None -> ()
- | Some fn -> try Sys.remove fn with _ -> ());
- true
- end
+ filename <- Some f;
+ input_buffer#set_modified false;
+ stats <- my_stat f;
+ (match self#auto_save_name with
+ | None -> ()
+ | Some fn -> try Sys.remove fn with _ -> ());
+ true
+ end
else false
- method private auto_save_name =
- match filename with
+ method private auto_save_name =
+ match filename with
| None -> None
- | Some f ->
- let dir = Filename.dirname f in
- let base = (fst !current.auto_save_name) ^
- (Filename.basename f) ^
- (snd !current.auto_save_name)
- in Some (Filename.concat dir base)
-
- method private need_auto_save =
+ | Some f ->
+ let dir = Filename.dirname f in
+ let base = (fst !current.auto_save_name) ^
+ (Filename.basename f) ^
+ (snd !current.auto_save_name)
+ in Some (Filename.concat dir base)
+
+ method private need_auto_save =
input_buffer#modified &&
- last_modification_time > last_auto_save_time
-
+ last_modification_time > last_auto_save_time
+
method auto_save =
if self#need_auto_save then begin
- match self#auto_save_name with
- | None -> ()
- | Some fn ->
- try
- last_auto_save_time <- Unix.time();
- prerr_endline ("Autosave time : "^(string_of_float (Unix.time())));
- if try_export fn (input_buffer#get_text ()) then begin
- !flash_info ~delay:1000 "Autosaved"
- end
- else warning
- ("Autosave failed (check if " ^ fn ^ " is writable)")
- with _ ->
- warning ("Autosave: unexpected error while writing "^fn)
- end
-
+ match self#auto_save_name with
+ | None -> ()
+ | Some fn ->
+ try
+ last_auto_save_time <- Unix.time();
+ prerr_endline ("Autosave time : "^(string_of_float (Unix.time())));
+ if try_export fn (input_buffer#get_text ()) then begin
+ flash_info ~delay:1000 "Autosaved"
+ end
+ else warning
+ ("Autosave failed (check if " ^ fn ^ " is writable)")
+ with _ ->
+ warning ("Autosave: unexpected error while writing "^fn)
+ end
+
method save_as f =
- if Sys.file_exists f then
+ if Sys.file_exists f then
match (GToolbox.question_box ~title:"File exists on disk"
- ~buttons:["Overwrite";
- "Cancel";]
- ~default:1
- ~icon:
- (let img = GMisc.image () in
- img#set_stock `DIALOG_WARNING;
- img#set_icon_size `DIALOG;
- img#coerce)
- ("File "^f^"already exists")
- )
+ ~buttons:["Overwrite";
+ "Cancel";]
+ ~default:1
+ ~icon:
+ (let img = GMisc.image () in
+ img#set_stock `DIALOG_WARNING;
+ img#set_icon_size `DIALOG;
+ img#coerce)
+ ("File "^f^"already exists")
+ )
with 1 -> self#save f
- | _ -> false
- else self#save f
+ | _ -> false
+ else self#save f
method set_read_only b = read_only<-b
method read_only = read_only
@@ -823,585 +675,494 @@ object(self)
method clear_message = message_buffer#set_text ""
val mutable last_index = true
val last_array = [|"";""|]
- method get_start_of_input = input_buffer#get_iter_at_mark (`NAME "start_of_input")
+ method get_start_of_input = input_buffer#get_iter_at_mark (`NAME "start_of_input")
method get_insert = get_insert input_buffer
- method recenter_insert =
- (* BUG : to investigate further:
- FIXED : Never call GMain.* in thread !
- PLUS : GTK BUG ??? Cannot be called from a thread...
- ADDITION: using sync instead of async causes deadlock...*)
+ method recenter_insert =
+ (* BUG : to investigate further:
+ FIXED : Never call GMain.* in thread !
+ PLUS : GTK BUG ??? Cannot be called from a thread...
+ ADDITION: using sync instead of async causes deadlock...*)
ignore (GtkThread.async (
- input_view#scroll_to_mark
- ~use_align:false
- ~yalign:0.75
- ~within_margin:0.25)
- `INSERT)
+ input_view#scroll_to_mark
+ ~use_align:false
+ ~yalign:0.75
+ ~within_margin:0.25)
+ `INSERT)
- method indent_current_line =
+ method indent_current_line =
let get_nb_space it =
let it = it#copy in
let nb_sep = ref 0 in
let continue = ref true in
- while !continue do
- if it#char = space then begin
- incr nb_sep;
- if not it#nocopy#forward_char then continue := false;
- end else continue := false
- done;
- !nb_sep
+ while !continue do
+ if it#char = space then begin
+ incr nb_sep;
+ if not it#nocopy#forward_char then continue := false;
+ end else continue := false
+ done;
+ !nb_sep
in
let previous_line = self#get_insert in
if previous_line#nocopy#backward_line then begin
- let previous_line_spaces = get_nb_space previous_line in
- let current_line_start = self#get_insert#set_line_offset 0 in
- let current_line_spaces = get_nb_space current_line_start in
- if input_buffer#delete_interactive
- ~start:current_line_start
- ~stop:(current_line_start#forward_chars current_line_spaces)
- ()
- then
- let current_line_start = self#get_insert#set_line_offset 0 in
- input_buffer#insert
- ~iter:current_line_start
- (String.make previous_line_spaces ' ')
- end
+ let previous_line_spaces = get_nb_space previous_line in
+ let current_line_start = self#get_insert#set_line_offset 0 in
+ let current_line_spaces = get_nb_space current_line_start in
+ if input_buffer#delete_interactive
+ ~start:current_line_start
+ ~stop:(current_line_start#forward_chars current_line_spaces)
+ ()
+ then
+ let current_line_start = self#get_insert#set_line_offset 0 in
+ input_buffer#insert
+ ~iter:current_line_start
+ (String.make previous_line_spaces ' ')
+ end
- method show_pm_goal =
- proof_buffer#insert
- (Printf.sprintf " *** Declarative Mode ***\n");
- try
- let (hyps,concl) = get_current_pm_goal () in
- List.iter
- (fun ((_,_,_,(s,_)) as _hyp) ->
- proof_buffer#insert (s^"\n"))
- hyps;
- proof_buffer#insert
- (String.make 38 '_' ^ "\n");
- let (_,_,_,s) = concl in
- proof_buffer#insert ("thesis := \n "^s^"\n");
- let my_mark = `NAME "end_of_conclusion" in
- proof_buffer#move_mark
- ~where:((proof_buffer#get_iter_at_mark `INSERT))
- my_mark;
- ignore (proof_view#scroll_to_mark my_mark)
- with Not_found ->
+ method show_pm_goal =
+ proof_buffer#insert
+ (Printf.sprintf " *** Declarative Mode ***\n");
+ try
+ let (hyps,concl) = get_current_pm_goal () in
+ List.iter
+ (fun ((_,_,_,(s,_)) as _hyp) ->
+ proof_buffer#insert (s^"\n"))
+ hyps;
+ proof_buffer#insert
+ (String.make 38 '_' ^ "\n");
+ let (_,_,_,s) = concl in
+ proof_buffer#insert ("thesis := \n "^s^"\n");
+ let my_mark = `NAME "end_of_conclusion" in
+ proof_buffer#move_mark
+ ~where:((proof_buffer#get_iter_at_mark `INSERT))
+ my_mark;
+ ignore (proof_view#scroll_to_mark my_mark)
+ with Not_found ->
match Decl_mode.get_end_command (Pfedit.get_pftreestate ()) with
- Some endc ->
- proof_buffer#insert
- ("Subproof completed, now type "^endc^".")
- | None ->
- proof_buffer#insert "Proof completed."
+ Some endc ->
+ proof_buffer#insert
+ ("Subproof completed, now type "^endc^".")
+ | None ->
+ proof_buffer#insert "Proof completed."
+
- method show_goals =
- try
- proof_view#buffer#set_text "";
- match Decl_mode.get_current_mode () with
- Decl_mode.Mode_none -> proof_buffer#insert (Coq.print_no_goal ())
- | Decl_mode.Mode_tactic ->
- begin
- let s = Coq.get_current_goals () in
- match s with
- | [] -> proof_buffer#insert (Coq.print_no_goal ())
- | (hyps,concl)::r ->
- let goal_nb = List.length s in
- proof_buffer#insert
- (Printf.sprintf "%d subgoal%s\n"
- goal_nb
- (if goal_nb<=1 then "" else "s"));
- List.iter
- (fun ((_,_,_,(s,_)) as _hyp) ->
- proof_buffer#insert (s^"\n"))
- hyps;
- proof_buffer#insert
- (String.make 38 '_' ^ "(1/"^
- (string_of_int goal_nb)^
- ")\n") ;
- let _,_,_,sconcl = concl in
- proof_buffer#insert sconcl;
- proof_buffer#insert "\n";
- let my_mark = `NAME "end_of_conclusion" in
- proof_buffer#move_mark
- ~where:((proof_buffer#get_iter_at_mark `INSERT))
- my_mark;
- proof_buffer#insert "\n\n";
- let i = ref 1 in
- List.iter
- (function (_,(_,_,_,concl)) ->
- incr i;
- proof_buffer#insert
- (String.make 38 '_' ^"("^
- (string_of_int !i)^
- "/"^
- (string_of_int goal_nb)^
- ")\n");
- proof_buffer#insert concl;
- proof_buffer#insert "\n\n";
- )
- r;
- ignore (proof_view#scroll_to_mark my_mark)
- end
- | Decl_mode.Mode_proof ->
- self#show_pm_goal
- with e ->
- prerr_endline ("Don't worry be happy despite: "^Printexc.to_string e)
-
-
val mutable full_goal_done = true
- method show_goals_full =
+ method show_goals_full =
if not full_goal_done then
begin
- try
- proof_view#buffer#set_text "";
- match Decl_mode.get_current_mode () with
- Decl_mode.Mode_none ->
- proof_buffer#insert (Coq.print_no_goal ())
- | Decl_mode.Mode_tactic ->
- begin
- match Coq.get_current_goals () with
- [] -> Util.anomaly "show_goals_full"
- | ((hyps,concl)::r) as s ->
- let last_shown_area =
- proof_buffer#create_tag [`BACKGROUND "light green"]
- in
- let goal_nb = List.length s in
- proof_buffer#insert (Printf.sprintf "%d subgoal%s\n"
- goal_nb
- (if goal_nb<=1 then "" else "s"));
- let coq_menu commands =
- let tag = proof_buffer#create_tag []
- in
- ignore
- (tag#connect#event ~callback:
- (fun ~origin ev it ->
- begin match GdkEvent.get_type ev with
- | `BUTTON_PRESS ->
- let ev = (GdkEvent.Button.cast ev) in
- if (GdkEvent.Button.button ev) = 3
- then begin
- let loc_menu = GMenu.menu () in
- let factory =
- new GMenu.factory loc_menu in
- let add_coq_command (cp,ip) =
- ignore
- (factory#add_item cp
- ~callback:
- (fun () -> ignore
- (self#insert_this_phrase_on_success
- true
- true
- false
- ("progress "^ip^"\n")
- (ip^"\n"))
- )
- )
- in
- List.iter add_coq_command commands;
- loc_menu#popup
- ~button:3
- ~time:(GdkEvent.Button.time ev);
- end
- | `MOTION_NOTIFY ->
- proof_buffer#remove_tag
- ~start:proof_buffer#start_iter
- ~stop:proof_buffer#end_iter
- last_shown_area;
- prerr_endline "Before find_tag_limits";
-
- let s,e = find_tag_limits tag
- (new GText.iter it)
- in
- prerr_endline "After find_tag_limits";
- proof_buffer#apply_tag
- ~start:s
- ~stop:e
- last_shown_area;
-
- prerr_endline "Applied tag";
- ()
- | _ -> ()
- end;false
- )
- );
- tag
- in
- List.iter
- (fun ((_,_,_,(s,_)) as hyp) ->
- let tag = coq_menu (hyp_menu hyp) in
- proof_buffer#insert ~tags:[tag] (s^"\n"))
- hyps;
- proof_buffer#insert
- (String.make 38 '_' ^"(1/"^
- (string_of_int goal_nb)^
- ")\n")
- ;
- let tag = coq_menu (concl_menu concl) in
- let _,_,_,sconcl = concl in
- proof_buffer#insert ~tags:[tag] sconcl;
- proof_buffer#insert "\n";
- let my_mark = `NAME "end_of_conclusion" in
- proof_buffer#move_mark
- ~where:((proof_buffer#get_iter_at_mark `INSERT)) my_mark;
- proof_buffer#insert "\n\n";
- let i = ref 1 in
- List.iter
- (function (_,(_,_,_,concl)) ->
- incr i;
- proof_buffer#insert
- (String.make 38 '_' ^"("^
- (string_of_int !i)^
- "/"^
- (string_of_int goal_nb)^
- ")\n");
- proof_buffer#insert concl;
- proof_buffer#insert "\n\n";
- )
- r;
- ignore (proof_view#scroll_to_mark my_mark) ;
- full_goal_done <- true
- end
- | Decl_mode.Mode_proof ->
- self#show_pm_goal
- with e -> prerr_endline (Printexc.to_string e)
+ try
+ proof_buffer#set_text "";
+ match Decl_mode.get_current_mode () with
+ Decl_mode.Mode_none -> ()
+ | Decl_mode.Mode_tactic ->
+ begin
+ match Coq.get_current_goals () with
+ [] -> proof_buffer#insert (Coq.print_no_goal())
+ | ((hyps,concl)::r) as s ->
+ let last_shown_area = Tags.Proof.highlight
+ in
+ let goal_nb = List.length s in
+ proof_buffer#insert (Printf.sprintf "%d subgoal%s\n"
+ goal_nb
+ (if goal_nb<=1 then "" else "s"));
+ let coq_menu commands =
+ let tag = proof_buffer#create_tag []
+ in
+ ignore
+ (tag#connect#event ~callback:
+ (fun ~origin ev it ->
+ match GdkEvent.get_type ev with
+ | `BUTTON_PRESS ->
+ let ev = (GdkEvent.Button.cast ev) in
+ if (GdkEvent.Button.button ev) = 3
+ then (
+ let loc_menu = GMenu.menu () in
+ let factory =
+ new GMenu.factory loc_menu in
+ let add_coq_command (cp,ip) =
+ ignore
+ (factory#add_item cp
+ ~callback:
+ (fun () -> ignore
+ (self#insert_this_phrase_on_success
+ true
+ true
+ false
+ ("progress "^ip^"\n")
+ (ip^"\n"))
+ )
+ )
+ in
+ List.iter add_coq_command commands;
+ loc_menu#popup
+ ~button:3
+ ~time:(GdkEvent.Button.time ev);
+ true)
+ else false
+ | `MOTION_NOTIFY ->
+ proof_buffer#remove_tag
+ ~start:proof_buffer#start_iter
+ ~stop:proof_buffer#end_iter
+ last_shown_area;
+ prerr_endline "Before find_tag_limits";
+
+ let s,e = find_tag_limits tag
+ (new GText.iter it)
+ in
+ prerr_endline "After find_tag_limits";
+ proof_buffer#apply_tag
+ ~start:s
+ ~stop:e
+ last_shown_area;
+
+ prerr_endline "Applied tag";
+ false
+ | _ ->
+ false
+ )
+ );
+ tag
+ in
+ List.iter
+ (fun ((_,_,_,(s,_)) as hyp) ->
+ let tag = coq_menu (hyp_menu hyp) in
+ proof_buffer#insert ~tags:[tag] (s^"\n"))
+ hyps;
+ proof_buffer#insert
+ (String.make 38 '_' ^"(1/"^
+ (string_of_int goal_nb)^
+ ")\n")
+ ;
+ let tag = coq_menu (concl_menu concl) in
+ let _,_,_,sconcl = concl in
+ proof_buffer#insert ~tags:[tag] sconcl;
+ proof_buffer#insert "\n";
+ let my_mark = `NAME "end_of_conclusion" in
+ proof_buffer#move_mark
+ ~where:((proof_buffer#get_iter_at_mark `INSERT)) my_mark;
+ proof_buffer#insert "\n\n";
+ let i = ref 1 in
+ List.iter
+ (function (_,(_,_,_,concl)) ->
+ incr i;
+ proof_buffer#insert
+ (String.make 38 '_' ^"("^
+ (string_of_int !i)^
+ "/"^
+ (string_of_int goal_nb)^
+ ")\n");
+ proof_buffer#insert concl;
+ proof_buffer#insert "\n\n";
+ )
+ r;
+ ignore (proof_view#scroll_to_mark my_mark) ;
+ full_goal_done <- true
+ end
+ | Decl_mode.Mode_proof ->
+ self#show_pm_goal
+ with e -> prerr_endline (Printexc.to_string e)
end
-
+
+ method show_goals = self#show_goals_full
+
+
method send_to_coq verbosely replace phrase show_output show_error localize =
let display_output msg =
self#insert_message (if show_output then msg else "") in
let display_error e =
let (s,loc) = Coq.process_exn e in
- assert (Glib.Utf8.validate s);
- self#insert_message s;
- message_view#misc#draw None;
- if localize then
- (match Option.map Util.unloc loc with
- | None -> ()
- | Some (start,stop) ->
- let convert_pos = byte_offset_to_char_offset phrase in
- let start = convert_pos start in
- let stop = convert_pos stop in
- let i = self#get_start_of_input in
- let starti = i#forward_chars start in
- let stopi = i#forward_chars stop in
- input_buffer#apply_tag_by_name "error"
- ~start:starti
- ~stop:stopi;
- input_buffer#place_cursor starti) in
- try
- full_goal_done <- false;
- prerr_endline "Send_to_coq starting now";
- Decl_mode.clear_daimon_flag ();
- if replace then begin
- let r,info = Coq.interp_and_replace ("info " ^ phrase) in
- let complete = not (Decl_mode.get_daimon_flag ()) in
- let msg = read_stdout () in
- sync display_output msg;
- Some (complete,r)
- end else begin
- let r = Coq.interp verbosely phrase in
- let complete = not (Decl_mode.get_daimon_flag ()) in
- let msg = read_stdout () in
- sync display_output msg;
- Some (complete,r)
- end
- with e ->
- if show_error then sync display_error e;
- None
-
- method find_phrase_starting_at (start:GText.iter) =
- prerr_endline "find_phrase_starting_at starting now";
- let trash_bytes = ref "" in
- let end_iter = start#copy in
- let lexbuf_function s count =
- let i = ref 0 in
- let n_trash = String.length !trash_bytes in
- String.blit !trash_bytes 0 s 0 n_trash;
- i := n_trash;
- try
- while !i <= count - 1 do
- let c = end_iter#char in
- if c = 0 then raise (Stop !i);
- let c' = Glib.Utf8.from_unichar c in
- let n = String.length c' in
- if (n<=0) then exit (-2);
- if n > count - !i then
- begin
- let ri = count - !i in
- String.blit c' 0 s !i ri;
- trash_bytes := String.sub c' ri (n-ri);
- i := count ;
- end else begin
- String.blit c' 0 s !i n;
- i:= !i + n
- end;
- if not end_iter#nocopy#forward_char then
- raise (Stop !i)
- done;
- count
- with Stop x ->
- x
- in
+ assert (Glib.Utf8.validate s);
+ self#insert_message s;
+ message_view#misc#draw None;
+ if localize then
+ (match Option.map Util.unloc loc with
+ | None -> ()
+ | Some (start,stop) ->
+ let convert_pos = byte_offset_to_char_offset phrase in
+ let start = convert_pos start in
+ let stop = convert_pos stop in
+ let i = self#get_start_of_input in
+ let starti = i#forward_chars start in
+ let stopi = i#forward_chars stop in
+ input_buffer#apply_tag Tags.Script.error
+ ~start:starti
+ ~stop:stopi;
+ input_buffer#place_cursor starti) in
try
- trash_bytes := "";
- let _ = Find_phrase.get (Lexing.from_function lexbuf_function)
- in
- end_iter#nocopy#set_offset (start#offset + !Find_phrase.length);
- Some (start,end_iter)
- with
- (*
- | Find_phrase.EOF s ->
- (* Phrase is at the end of the buffer*)
- let si = start#offset in
- let ei = si + !Find_phrase.length in
- end_iter#nocopy#set_offset (ei - 1);
- input_buffer#insert ~iter:end_iter "\n";
- Some (input_buffer#get_iter (`OFFSET si),
- input_buffer#get_iter (`OFFSET ei))
- *)
- | _ -> None
-
- method complete_at_offset (offset:int) =
+ full_goal_done <- false;
+ prerr_endline "Send_to_coq starting now";
+ Decl_mode.clear_daimon_flag ();
+ if replace then begin
+ let r,info = Coq.interp_and_replace ("info " ^ phrase) in
+ let is_complete = not (Decl_mode.get_daimon_flag ()) in
+ let msg = read_stdout () in
+ sync display_output msg;
+ Some (is_complete,r)
+ end else begin
+ let r = Coq.interp verbosely phrase in
+ let is_complete = not (Decl_mode.get_daimon_flag ()) in
+ let msg = read_stdout () in
+ sync display_output msg;
+ Some (is_complete,r)
+ end
+ with e ->
+ if show_error then sync display_error e;
+ None
+
+ method find_phrase_starting_at (start:GText.iter) =
+ try
+ let start = grab_safe_sentence_start start self#get_start_of_input in
+ let stop = grab_sentence_end_from start in
+ if stop#backward_char#has_tag Tags.Script.lax_end then
+ Some (start,stop)
+ else
+ None
+ with Not_found -> None
+
+ method complete_at_offset (offset:int) =
prerr_endline ("Completion at offset : " ^ string_of_int offset);
let it () = input_buffer#get_iter (`OFFSET offset) in
let iit = it () in
let start = find_word_start iit in
- if ends_word iit then
- let w = input_buffer#get_text
- ~start
- ~stop:iit
- ()
- in
- if String.length w <> 0 then begin
- prerr_endline ("Completion of prefix : '" ^ w^"'");
- match complete input_buffer w start#offset with
- | None -> false
- | Some (ss,start,stop) ->
- let completion = input_buffer#get_text ~start ~stop () in
- ignore (input_buffer#delete_selection ());
- ignore (input_buffer#insert_interactive completion);
- input_buffer#move_mark `SEL_BOUND (it())#backward_char;
- true
- end else false
- else false
-
-
- method process_next_phrase verbosely display_goals do_highlight =
+ if ends_word iit then
+ let w = input_buffer#get_text
+ ~start
+ ~stop:iit
+ ()
+ in
+ if String.length w <> 0 then begin
+ prerr_endline ("Completion of prefix : '" ^ w^"'");
+ match complete input_buffer w start#offset with
+ | None -> false
+ | Some (ss,start,stop) ->
+ let completion = input_buffer#get_text ~start ~stop () in
+ ignore (input_buffer#delete_selection ());
+ ignore (input_buffer#insert_interactive completion);
+ input_buffer#move_mark `SEL_BOUND (it())#backward_char;
+ true
+ end else false
+ else false
+
+ method process_next_phrase verbosely display_goals do_highlight =
let get_next_phrase () =
self#clear_message;
prerr_endline "process_next_phrase starting now";
if do_highlight then begin
- !push_info "Coq is computing";
- input_view#set_editable false;
- end;
- match self#find_phrase_starting_at self#get_start_of_input with
- | None ->
- if do_highlight then begin
- input_view#set_editable true;
- !pop_info ();
- end;
+ push_info "Coq is computing";
+ input_view#set_editable false;
+ end;
+ match self#find_phrase_starting_at self#get_start_of_input with
+ | None ->
+ if do_highlight then begin
+ input_view#set_editable true;
+ pop_info ();
+ end;
None
- | Some(start,stop) ->
- prerr_endline "process_next_phrase : to_process highlight";
- if do_highlight then begin
- input_buffer#apply_tag_by_name ~start ~stop "to_process";
- prerr_endline "process_next_phrase : to_process applied";
- end;
- prerr_endline "process_next_phrase : getting phrase";
+ | Some(start,stop) ->
+ prerr_endline "process_next_phrase : to_process highlight";
+ if do_highlight then begin
+ input_buffer#apply_tag Tags.Script.to_process ~start ~stop;
+ prerr_endline "process_next_phrase : to_process applied";
+ end;
+ prerr_endline "process_next_phrase : getting phrase";
Some((start,stop),start#get_slice ~stop) in
let remove_tag (start,stop) =
if do_highlight then begin
- input_buffer#remove_tag_by_name ~start ~stop "to_process" ;
- input_view#set_editable true;
- !pop_info ();
- end in
- let mark_processed reset_info complete (start,stop) ast =
- let b = input_buffer in
- b#move_mark ~where:stop (`NAME "start_of_input");
- b#apply_tag_by_name
- (if complete then "processed" else "unjustified") ~start ~stop;
- if (self#get_insert#compare) stop <= 0 then
- begin
- b#place_cursor stop;
- self#recenter_insert
- end;
- let start_of_phrase_mark = `MARK (b#create_mark start) in
- let end_of_phrase_mark = `MARK (b#create_mark stop) in
- push_phrase
- reset_info
- start_of_phrase_mark
- end_of_phrase_mark ast;
- if display_goals then self#show_goals;
- remove_tag (start,stop) in
- begin
- match sync get_next_phrase () with
- None -> false
- | Some (loc,phrase) ->
+ input_buffer#remove_tag Tags.Script.to_process ~start ~stop;
+ input_view#set_editable true;
+ pop_info ();
+ end in
+ let mark_processed reset_info is_complete (start,stop) =
+ let b = input_buffer in
+ b#move_mark ~where:stop (`NAME "start_of_input");
+ b#apply_tag
+ (if is_complete then Tags.Script.processed else Tags.Script.unjustified) ~start ~stop;
+ if (self#get_insert#compare) stop <= 0 then
+ begin
+ b#place_cursor stop;
+ self#recenter_insert
+ end;
+ let ide_payload = { start = `MARK (b#create_mark start);
+ stop = `MARK (b#create_mark stop); } in
+ push_phrase
+ cmd_stack
+ reset_info
+ ide_payload;
+ if display_goals then self#show_goals;
+ remove_tag (start,stop) in
+ begin
+ match sync get_next_phrase () with
+ None -> false
+ | Some (loc,phrase) ->
(match self#send_to_coq verbosely false phrase true true true with
- | Some (complete,(reset_info,ast)) ->
- sync (mark_processed reset_info complete) loc ast; true
- | None -> sync remove_tag loc; false)
- end
-
- method insert_this_phrase_on_success
- show_output show_msg localize coqphrase insertphrase =
- let mark_processed reset_info complete ast =
+ | Some (is_complete,reset_info) ->
+ sync (mark_processed reset_info is_complete) loc; true
+ | None -> sync remove_tag loc; false)
+ end
+
+ method insert_this_phrase_on_success
+ show_output show_msg localize coqphrase insertphrase =
+ let mark_processed reset_info is_complete =
let stop = self#get_start_of_input in
- if stop#starts_line then
- input_buffer#insert ~iter:stop insertphrase
- else input_buffer#insert ~iter:stop ("\n"^insertphrase);
- let start = self#get_start_of_input in
- input_buffer#move_mark ~where:stop (`NAME "start_of_input");
- input_buffer#apply_tag_by_name
- (if complete then "processed" else "unjustified") ~start ~stop;
- if (self#get_insert#compare) stop <= 0 then
- input_buffer#place_cursor stop;
- let start_of_phrase_mark = `MARK (input_buffer#create_mark start) in
- let end_of_phrase_mark = `MARK (input_buffer#create_mark stop) in
- push_phrase reset_info start_of_phrase_mark end_of_phrase_mark ast;
- self#show_goals;
- (*Auto insert save on success...
- try (match Coq.get_current_goals () with
- | [] ->
- (match self#send_to_coq "Save.\n" true true true with
- | Some ast ->
- begin
- let stop = self#get_start_of_input in
- if stop#starts_line then
- input_buffer#insert ~iter:stop "Save.\n"
- else input_buffer#insert ~iter:stop "\nSave.\n";
- let start = self#get_start_of_input in
- input_buffer#move_mark ~where:stop (`NAME"start_of_input");
- input_buffer#apply_tag_by_name "processed" ~start ~stop;
- if (self#get_insert#compare) stop <= 0 then
- input_buffer#place_cursor stop;
- let start_of_phrase_mark =
- `MARK (input_buffer#create_mark start) in
- let end_of_phrase_mark =
- `MARK (input_buffer#create_mark stop) in
- push_phrase
- reset_info start_of_phrase_mark end_of_phrase_mark ast
- end
- | None -> ())
- | _ -> ())
- with _ -> ()*) in
- match self#send_to_coq false false coqphrase show_output show_msg localize with
- | Some (complete,(reset_info,ast)) ->
- sync (mark_processed reset_info complete) ast; true
- | None ->
- sync
- (fun _ -> self#insert_message ("Unsuccessfully tried: "^coqphrase))
- ();
- false
+ if stop#starts_line then
+ input_buffer#insert ~iter:stop insertphrase
+ else input_buffer#insert ~iter:stop ("\n"^insertphrase);
+ let start = self#get_start_of_input in
+ input_buffer#move_mark ~where:stop (`NAME "start_of_input");
+ input_buffer#apply_tag
+ (if is_complete then Tags.Script.processed else Tags.Script.unjustified) ~start ~stop;
+ if (self#get_insert#compare) stop <= 0 then
+ input_buffer#place_cursor stop;
+ let ide_payload = { start = `MARK (input_buffer#create_mark start);
+ stop = `MARK (input_buffer#create_mark stop); } in
+ push_phrase cmd_stack reset_info ide_payload;
+ self#show_goals;
+ (*Auto insert save on success...
+ try (match Coq.get_current_goals () with
+ | [] ->
+ (match self#send_to_coq "Save.\n" true true true with
+ | Some ast ->
+ begin
+ let stop = self#get_start_of_input in
+ if stop#starts_line then
+ input_buffer#insert ~iter:stop "Save.\n"
+ else input_buffer#insert ~iter:stop "\nSave.\n";
+ let start = self#get_start_of_input in
+ input_buffer#move_mark ~where:stop (`NAME"start_of_input");
+ input_buffer#apply_tag_by_name "processed" ~start ~stop;
+ if (self#get_insert#compare) stop <= 0 then
+ input_buffer#place_cursor stop;
+ let start_of_phrase_mark =
+ `MARK (input_buffer#create_mark start) in
+ let end_of_phrase_mark =
+ `MARK (input_buffer#create_mark stop) in
+ push_phrase
+ reset_info start_of_phrase_mark end_of_phrase_mark ast
+ end
+ | None -> ())
+ | _ -> ())
+ with _ -> ()*) in
+ match self#send_to_coq false false coqphrase show_output show_msg localize with
+ | Some (is_complete,reset_info) ->
+ sync (mark_processed reset_info) is_complete; true
+ | None ->
+ sync
+ (fun _ -> self#insert_message ("Unsuccessfully tried: "^coqphrase))
+ ();
+ false
method process_until_iter_or_error stop =
let stop' = `OFFSET stop#offset in
let start = self#get_start_of_input#copy in
let start' = `OFFSET start#offset in
sync (fun _ ->
- input_buffer#apply_tag_by_name ~start ~stop "to_process";
- input_view#set_editable false) ();
- !push_info "Coq is computing";
+ input_buffer#apply_tag Tags.Script.to_process ~start ~stop;
+ input_view#set_editable false) ();
+ push_info "Coq is computing";
let get_current () =
- if !current.stop_before then
+ if !current.stop_before then
match self#find_phrase_starting_at self#get_start_of_input with
| None -> self#get_start_of_input
| Some (_, stop2) -> stop2
- else begin
- self#get_start_of_input
- end
- in
- (try
- while ((stop#compare (get_current())>=0)
- && (self#process_next_phrase false false false))
- do Util.check_for_interrupt () done
- with Sys.Break ->
- prerr_endline "Interrupted during process_until_iter_or_error");
- sync (fun _ ->
- self#show_goals;
- (* Start and stop might be invalid if an eol was added at eof *)
- let start = input_buffer#get_iter start' in
- let stop = input_buffer#get_iter stop' in
- input_buffer#remove_tag_by_name ~start ~stop "to_process" ;
- input_view#set_editable true) ();
- !pop_info()
-
- method process_until_end_or_error =
+ else begin
+ self#get_start_of_input
+ end
+ in
+ (try
+ while ((stop#compare (get_current())>=0)
+ && (self#process_next_phrase false false false))
+ do Util.check_for_interrupt () done
+ with Sys.Break ->
+ prerr_endline "Interrupted during process_until_iter_or_error");
+ sync (fun _ ->
+ self#show_goals;
+ (* Start and stop might be invalid if an eol was added at eof *)
+ let start = input_buffer#get_iter start' in
+ let stop = input_buffer#get_iter stop' in
+ input_buffer#remove_tag Tags.Script.to_process ~start ~stop;
+ input_view#set_editable true) ();
+ pop_info()
+
+ method process_until_end_or_error =
self#process_until_iter_or_error input_buffer#end_iter
method reset_initial =
sync (fun _ ->
- Stack.iter
- (function inf ->
- let start = input_buffer#get_iter_at_mark inf.start in
- let stop = input_buffer#get_iter_at_mark inf.stop in
- input_buffer#move_mark ~where:start (`NAME "start_of_input");
- input_buffer#remove_tag_by_name "processed" ~start ~stop;
- input_buffer#remove_tag_by_name "unjustified" ~start ~stop;
- input_buffer#delete_mark inf.start;
- input_buffer#delete_mark inf.stop;
- )
- processed_stack;
- Stack.clear processed_stack;
- self#clear_message)();
+ Stack.iter
+ (function (inf,_) ->
+ let start = input_buffer#get_iter_at_mark inf.start in
+ let stop = input_buffer#get_iter_at_mark inf.stop in
+ input_buffer#move_mark ~where:start (`NAME "start_of_input");
+ input_buffer#remove_tag Tags.Script.processed ~start ~stop;
+ input_buffer#remove_tag Tags.Script.unjustified ~start ~stop;
+ input_buffer#delete_mark inf.start;
+ input_buffer#delete_mark inf.stop;
+ )
+ cmd_stack;
+ Stack.clear cmd_stack;
+ self#clear_message)();
Coq.reset_initial ()
(* backtrack Coq to the phrase preceding iterator [i] *)
method backtrack_to_no_lock i =
prerr_endline "Backtracking_to iter starts now.";
(* pop Coq commands until we reach iterator [i] *)
- let rec pop_commands done_smthg undos =
- if is_empty () then
- done_smthg, undos
+ let rec pop_cmds popped =
+ if Stack.is_empty cmd_stack then
+ popped
else
- let t = top () in
- if i#compare (input_buffer#get_iter_at_mark t.stop) < 0 then
+ let (ide,coq) = Stack.pop cmd_stack in
+ if i#compare (input_buffer#get_iter_at_mark ide.stop) < 0 then
begin
- prerr_endline "Popped top command";
- pop_commands true (pop_command undos t)
- end
+ prerr_endline "popped command";
+ pop_cmds (coq::popped)
+ end
else
- done_smthg, undos
+ begin
+ Stack.push (ide,coq) cmd_stack;
+ popped
+ end
in
- let undos = (0,0,NoBacktrack,0,undo_info()) in
- let done_smthg, undos = pop_commands false undos in
+ let seq = List.rev (pop_cmds []) in
prerr_endline "Popped commands";
- if done_smthg then
- begin
- try
- apply_undos undos;
+ if 0 < List.length seq then
+ begin
+ try
+ rewind seq cmd_stack;
sync (fun _ ->
- let start =
- if is_empty () then input_buffer#start_iter
- else input_buffer#get_iter_at_mark (top ()).stop in
- prerr_endline "Removing (long) processed tag...";
- input_buffer#remove_tag_by_name
- ~start
- ~stop:self#get_start_of_input
- "processed";
- input_buffer#remove_tag_by_name
- ~start
- ~stop:self#get_start_of_input
- "unjustified";
- prerr_endline "Moving (long) start_of_input...";
- input_buffer#move_mark ~where:start (`NAME "start_of_input");
- self#show_goals;
- clear_stdout ();
- self#clear_message)
+ let start =
+ if Stack.is_empty cmd_stack then input_buffer#start_iter
+ else input_buffer#get_iter_at_mark (fst (Stack.top cmd_stack)).stop in
+ prerr_endline "Removing (long) processed tag...";
+ input_buffer#remove_tag
+ Tags.Script.processed
+ ~start
+ ~stop:self#get_start_of_input;
+ input_buffer#remove_tag
+ Tags.Script.unjustified
+ ~start
+ ~stop:self#get_start_of_input;
+ prerr_endline "Moving (long) start_of_input...";
+ input_buffer#move_mark ~where:start (`NAME "start_of_input");
+ full_goal_done <- false;
+ self#show_goals;
+ clear_stdout ();
+ self#clear_message)
();
- with _ ->
- !push_info "WARNING: undo failed badly -> Coq might be in an inconsistent state.
-Please restart and report NOW.";
- end
- else prerr_endline "backtrack_to : discarded (...)"
-
- method backtrack_to i =
- if Mutex.try_lock coq_may_stop then
- (!push_info "Undoing...";
+ with _ ->
+ push_info "WARNING: undo failed badly -> Coq might be in an inconsistent state.
+ Please restart and report NOW.";
+ end
+ else prerr_endline "backtrack_to : discarded (...)"
+
+ method backtrack_to i =
+ if Mutex.try_lock coq_may_stop then
+ (push_info "Undoing...";
self#backtrack_to_no_lock i; Mutex.unlock coq_may_stop;
- !pop_info ())
+ pop_info ())
else prerr_endline "backtrack_to : discarded (lock is busy)"
method go_to_insert =
@@ -1411,405 +1172,278 @@ Please restart and report NOW.";
else self#backtrack_to point
method undo_last_step =
- if Mutex.try_lock coq_may_stop then
- (!push_info "Undoing last step...";
+ if Mutex.try_lock coq_may_stop then
+ (push_info "Undoing last step...";
(try
- let last_command = top () in
- let start = input_buffer#get_iter_at_mark last_command.start in
- let update_input () =
- prerr_endline "Removing processed tag...";
- input_buffer#remove_tag_by_name
- ~start
- ~stop:(input_buffer#get_iter_at_mark last_command.stop)
- "processed";
- input_buffer#remove_tag_by_name
- ~start
- ~stop:(input_buffer#get_iter_at_mark last_command.stop)
- "unjustified";
- prerr_endline "Moving start_of_input";
- input_buffer#move_mark
- ~where:start
- (`NAME "start_of_input");
- input_buffer#place_cursor start;
- self#recenter_insert;
- self#show_goals;
- self#clear_message
- in
- let undo = pop_command (0,0,NoBacktrack,0,undo_info()) last_command in
- apply_undos undo;
- sync update_input ()
- with
- | Size 0 -> (* !flash_info "Nothing to Undo"*)()
+ let (ide_ri,_) = Stack.top cmd_stack in
+ let start = input_buffer#get_iter_at_mark ide_ri.start in
+ let update_input () =
+ prerr_endline "Removing processed tag...";
+ input_buffer#remove_tag
+ Tags.Script.processed
+ ~start
+ ~stop:(input_buffer#get_iter_at_mark ide_ri.stop);
+ input_buffer#remove_tag
+ Tags.Script.unjustified
+ ~start
+ ~stop:(input_buffer#get_iter_at_mark ide_ri.stop);
+ prerr_endline "Moving start_of_input";
+ input_buffer#move_mark
+ ~where:start
+ (`NAME "start_of_input");
+ input_buffer#place_cursor start;
+ self#recenter_insert;
+ full_goal_done <- false;
+ self#show_goals;
+ self#clear_message
+ in
+ let _,coq = Stack.pop cmd_stack in
+ rewind [coq] cmd_stack;
+ sync update_input ()
+ with
+ | Stack.Empty -> (* flash_info "Nothing to Undo"*)()
);
- !pop_info ();
+ pop_info ();
Mutex.unlock coq_may_stop)
else prerr_endline "undo_last_step discarded"
-
- method blaster () =
-
- ignore (Thread.create
- (fun () ->
- prerr_endline "Blaster called";
- let c = Blaster_window.present_blaster_window () in
- if Mutex.try_lock c#lock then begin
- c#clear ();
- Decl_mode.check_not_proof_mode "No blaster in Proof mode";
- let current_gls = try get_current_goals () with _ -> [] in
-
- let set_goal i (s,t) =
- let gnb = string_of_int i in
- let s = gnb ^":"^s in
- let t' = gnb ^": progress "^t in
- let t'' = gnb ^": "^t in
- c#set
- ("Goal "^gnb)
- s
- (fun () -> try_interptac t')
- (sync(fun () -> self#insert_command t'' t''))
- in
- let set_current_goal (s,t) =
- c#set
- "Goal 1"
- s
- (fun () -> try_interptac ("progress "^t))
- (sync(fun () -> self#insert_command t t))
- in
- begin match current_gls with
- | [] -> ()
- | (hyp_l,current_gl)::r ->
- List.iter set_current_goal (concl_menu current_gl);
- List.iter
- (fun hyp ->
- List.iter set_current_goal (hyp_menu hyp))
- hyp_l;
- let i = ref 2 in
- List.iter
- (fun (hyp_l,gl) ->
- List.iter (set_goal !i) (concl_menu gl);
- incr i)
- r
- end;
- let _ = c#blaster () in
- Mutex.unlock c#lock
- end else prerr_endline "Blaster discarded")
- ())
-
- method insert_command cp ip =
+
+ method insert_command cp ip =
async(fun _ -> self#clear_message)();
ignore (self#insert_this_phrase_on_success true false false cp ip)
method tactic_wizard l =
async(fun _ -> self#clear_message)();
- ignore
- (List.exists
- (fun p ->
- self#insert_this_phrase_on_success true false false
- ("progress "^p^".\n") (p^".\n")) l)
-
- method active_keypress_handler k =
+ ignore
+ (List.exists
+ (fun p ->
+ self#insert_this_phrase_on_success true false false
+ ("progress "^p^".\n") (p^".\n")) l)
+
+ method active_keypress_handler k =
let state = GdkEvent.Key.state k in
begin
- match state with
- | l when List.mem `MOD1 l ->
- let k = GdkEvent.Key.keyval k in
- if GdkKeysyms._Return=k
- then ignore(
- if (input_buffer#insert_interactive "\n") then
- begin
- let i= self#get_insert#backward_word_start in
- prerr_endline "active_kp_hf: Placing cursor";
- self#process_until_iter_or_error i
- end);
- true
- | l when List.mem `CONTROL l ->
- let k = GdkEvent.Key.keyval k in
- if GdkKeysyms._Break=k
- then break ();
- false
- | l ->
- if GdkEvent.Key.keyval k = GdkKeysyms._Tab then begin
- prerr_endline "active_kp_handler for Tab";
- self#indent_current_line;
- true
- end else false
+ match state with
+ | l when List.mem `MOD1 l ->
+ let k = GdkEvent.Key.keyval k in
+ if GdkKeysyms._Return=k
+ then ignore(
+ if (input_buffer#insert_interactive "\n") then
+ begin
+ let i= self#get_insert#backward_word_start in
+ prerr_endline "active_kp_hf: Placing cursor";
+ self#process_until_iter_or_error i
+ end);
+ true
+ | l when List.mem `CONTROL l ->
+ let k = GdkEvent.Key.keyval k in
+ if GdkKeysyms._Break=k
+ then break ();
+ false
+ | l ->
+ if GdkEvent.Key.keyval k = GdkKeysyms._Tab then begin
+ prerr_endline "active_kp_handler for Tab";
+ self#indent_current_line;
+ true
+ end else false
end
- method disconnected_keypress_handler k =
+
+
+ method disconnected_keypress_handler k =
match GdkEvent.Key.state k with
- | l when List.mem `CONTROL l ->
- let k = GdkEvent.Key.keyval k in
- if GdkKeysyms._c=k
- then break ();
- false
+ | l when List.mem `CONTROL l ->
+ let k = GdkEvent.Key.keyval k in
+ if GdkKeysyms._c=k
+ then break ();
+ false
| l -> false
-
+
val mutable deact_id = None
val mutable act_id = None
- method deactivate () =
+ method deactivate () =
is_active <- false;
- (match act_id with None -> ()
+ (match act_id with None -> ()
| Some id ->
- reset_initial ();
- input_view#misc#disconnect id;
- prerr_endline "DISCONNECTED old active : ";
- print_id id;
- );
- deact_id <- Some
- (input_view#event#connect#key_press self#disconnected_keypress_handler);
+ reset_initial ();
+ input_view#misc#disconnect id;
+ prerr_endline "DISCONNECTED old active : ";
+ print_id id;
+ )(*;
+ deact_id <- Some
+ (input_view#event#connect#key_press self#disconnected_keypress_handler);
prerr_endline "CONNECTED inactive : ";
- print_id (Option.get deact_id)
+ print_id (Option.get deact_id)*)
+ (* XXX *)
method activate () =
- is_active <- true;
- (match deact_id with None -> ()
+ is_active <- true;(*
+ (match deact_id with None -> ()
| Some id -> input_view#misc#disconnect id;
- prerr_endline "DISCONNECTED old inactive : ";
- print_id id
- );
- act_id <- Some
- (input_view#event#connect#key_press self#active_keypress_handler);
+ prerr_endline "DISCONNECTED old inactive : ";
+ print_id id
+ );*)
+ act_id <- Some
+ (input_view#event#connect#key_press self#active_keypress_handler);
prerr_endline "CONNECTED active : ";
print_id (Option.get act_id);
- match
- (Option.get ((Vector.get input_views index).analyzed_view)) #filename
+ match
+ filename
with
| None -> ()
| Some f -> let dir = Filename.dirname f in
- if not (is_in_loadpath dir) then
- begin
- ignore (Coq.interp false
- (Printf.sprintf "Add LoadPath \"%s\". " dir))
- end
-
- method electric_handler =
+ if not (is_in_loadpath dir) then
+ begin
+ ignore (Coq.interp false
+ (Printf.sprintf "Add LoadPath \"%s\". " dir))
+ end
+
+ method electric_handler =
input_buffer#connect#insert_text ~callback:
- (fun it x ->
- begin try
- if last_index then begin
- last_array.(0)<-x;
- if (last_array.(1) ^ last_array.(0) = ".\n") then raise Found
- end else begin
- last_array.(1)<-x;
- if (last_array.(0) ^ last_array.(1) = ".\n") then raise Found
- end
- with Found ->
- begin
- ignore (self#process_next_phrase false true true)
- end;
- end;
- last_index <- not last_index;)
+ (fun it x ->
+ begin try
+ if last_index then begin
+ last_array.(0)<-x;
+ if (last_array.(1) ^ last_array.(0) = ".\n") then raise Found
+ end else begin
+ last_array.(1)<-x;
+ if (last_array.(0) ^ last_array.(1) = ".\n") then raise Found
+ end
+ with Found ->
+ begin
+ ignore (self#process_next_phrase false true true)
+ end;
+ end;
+ last_index <- not last_index;)
method private electric_paren tag =
let oparen_code = Glib.Utf8.to_unichar "(" (ref 0) in
let cparen_code = Glib.Utf8.to_unichar ")" (ref 0) in
ignore (input_buffer#connect#insert_text ~callback:
- (fun it x ->
- input_buffer#remove_tag
- ~start:input_buffer#start_iter
- ~stop:input_buffer#end_iter
- tag;
- if x = "" then () else
- match x.[String.length x - 1] with
- | ')' ->
- let hit = self#get_insert in
- let count = ref 0 in
- if hit#nocopy#backward_find_char
- (fun c ->
- if c = oparen_code && !count = 0 then true
- else if c = cparen_code then
- (incr count;false)
- else if c = oparen_code then
- (decr count;false)
- else false
- )
- then
- begin
- prerr_endline "Found matching parenthesis";
- input_buffer#apply_tag tag ~start:hit ~stop:hit#forward_char
- end
- else ()
- | _ -> ())
- )
+ (fun it x ->
+ input_buffer#remove_tag
+ ~start:input_buffer#start_iter
+ ~stop:input_buffer#end_iter
+ tag;
+ if x = "" then () else
+ match x.[String.length x - 1] with
+ | ')' ->
+ let hit = self#get_insert in
+ let count = ref 0 in
+ if hit#nocopy#backward_find_char
+ (fun c ->
+ if c = oparen_code && !count = 0 then true
+ else if c = cparen_code then
+ (incr count;false)
+ else if c = oparen_code then
+ (decr count;false)
+ else false
+ )
+ then
+ begin
+ prerr_endline "Found matching parenthesis";
+ input_buffer#apply_tag tag ~start:hit ~stop:hit#forward_char
+ end
+ else ()
+ | _ -> ())
+ )
+
+ method help_for_keyword () =
- method help_for_keyword () =
-
browse_keyword (self#insert_message) (get_current_word ())
- initializer
+ initializer
ignore (message_buffer#connect#insert_text
- ~callback:(fun it s -> ignore
- (message_view#scroll_to_mark
- ~use_align:false
- ~within_margin:0.49
- `INSERT)));
+ ~callback:(fun it s -> ignore
+ (message_view#scroll_to_mark
+ ~use_align:false
+ ~within_margin:0.49
+ `INSERT)));
ignore (input_buffer#connect#insert_text
- ~callback:(fun it s ->
- if (it#compare self#get_start_of_input)<0
- then GtkSignal.stop_emit ();
- if String.length s > 1 then
- (prerr_endline "insert_text: Placing cursor";input_buffer#place_cursor it)));
+ ~callback:(fun it s ->
+ if (it#compare self#get_start_of_input)<0
+ then GtkSignal.stop_emit ();
+ if String.length s > 1 then
+ (prerr_endline "insert_text: Placing cursor";input_buffer#place_cursor it)));
ignore (input_buffer#connect#after#apply_tag
- ~callback:(fun tag ~start ~stop ->
- if (start#compare self#get_start_of_input)>=0
- then
- begin
- input_buffer#remove_tag_by_name
- ~start
- ~stop
- "processed";
- input_buffer#remove_tag_by_name
- ~start
- ~stop
- "unjustified"
- end
- )
- );
+ ~callback:(fun tag ~start ~stop ->
+ if (start#compare self#get_start_of_input)>=0
+ then
+ begin
+ input_buffer#remove_tag
+ Tags.Script.processed
+ ~start
+ ~stop;
+ input_buffer#remove_tag
+ Tags.Script.unjustified
+ ~start
+ ~stop
+ end
+ )
+ );
ignore (input_buffer#connect#after#insert_text
- ~callback:(fun it s ->
- if auto_complete_on &&
- String.length s = 1 && s <> " " && s <> "\n"
- then
- let v = Option.get (get_current_view ()).analyzed_view
- in
- let has_completed =
- v#complete_at_offset
- ((v#view#buffer#get_iter `SEL_BOUND)#offset)
- in
- if has_completed then
- input_buffer#move_mark `SEL_BOUND (input_buffer#get_iter `SEL_BOUND)#forward_char;
-
-
- )
- );
- ignore (input_buffer#connect#modified_changed
- ~callback:
- (fun () ->
- if input_buffer#modified then
- set_tab_image index
- ~icon:(match (Option.get (current_all.analyzed_view))#filename with
- | None -> `SAVE_AS
- | Some _ -> `SAVE
- )
- else set_tab_image index ~icon:`YES;
- ));
+ ~callback:(fun it s ->
+ if auto_complete_on &&
+ String.length s = 1 && s <> " " && s <> "\n"
+ then
+ let v = session_notebook#current_term.analyzed_view
+ in
+ let has_completed =
+ v#complete_at_offset
+ ((input_view#buffer#get_iter `SEL_BOUND)#offset)
+ in
+ if has_completed then
+ input_buffer#move_mark `SEL_BOUND (input_buffer#get_iter `SEL_BOUND)#forward_char;
+
+
+ )
+ );
ignore (input_buffer#connect#changed
- ~callback:(fun () ->
- last_modification_time <- Unix.time ();
- let r = input_view#visible_rect in
- let stop =
- input_view#get_iter_at_location
- ~x:(Gdk.Rectangle.x r + Gdk.Rectangle.width r)
- ~y:(Gdk.Rectangle.y r + Gdk.Rectangle.height r)
- in
- input_buffer#remove_tag_by_name
- ~start:self#get_start_of_input
- ~stop
- "error";
- Highlight.highlight_around_current_line
- input_buffer
- )
- );
- ignore (input_buffer#add_selection_clipboard (cb()));
- let paren_highlight_tag = input_buffer#create_tag ~name:"paren" [`BACKGROUND "purple"] in
- self#electric_paren paren_highlight_tag;
- ignore (input_buffer#connect#after#mark_set
- ~callback:(fun it (m:Gtk.text_mark) ->
- !set_location
- (Printf.sprintf
- "Line: %5d Char: %3d" (self#get_insert#line + 1)
- (self#get_insert#line_offset + 1));
- match GtkText.Mark.get_name m with
- | Some "insert" ->
- input_buffer#remove_tag
- ~start:input_buffer#start_iter
- ~stop:input_buffer#end_iter
- paren_highlight_tag;
- | Some s ->
- prerr_endline (s^" moved")
- | None -> () )
- );
+ ~callback:(fun () ->
+ last_modification_time <- Unix.time ();
+ let r = input_view#visible_rect in
+ let stop =
+ input_view#get_iter_at_location
+ ~x:(Gdk.Rectangle.x r + Gdk.Rectangle.width r)
+ ~y:(Gdk.Rectangle.y r + Gdk.Rectangle.height r)
+ in
+ input_buffer#remove_tag
+ Tags.Script.error
+ ~start:self#get_start_of_input
+ ~stop;
+ tag_on_insert input_buffer
+ )
+ );
+ ignore (input_buffer#add_selection_clipboard cb);
+ ignore (proof_buffer#add_selection_clipboard cb);
+ ignore (message_buffer#add_selection_clipboard cb);
+ self#electric_paren Tags.Script.paren;
+ ignore (input_buffer#connect#after#mark_set
+ ~callback:(fun it (m:Gtk.text_mark) ->
+ !set_location
+ (Printf.sprintf
+ "Line: %5d Char: %3d" (self#get_insert#line + 1)
+ (self#get_insert#line_offset + 1));
+ match GtkText.Mark.get_name m with
+ | Some "insert" ->
+ input_buffer#remove_tag
+ ~start:input_buffer#start_iter
+ ~stop:input_buffer#end_iter
+ Tags.Script.paren;
+ | Some s ->
+ prerr_endline (s^" moved")
+ | None -> () )
+ );
ignore (input_buffer#connect#insert_text
- (fun it s ->
- prerr_endline "Should recenter ?";
- if String.contains s '\n' then begin
- prerr_endline "Should recenter : yes";
- self#recenter_insert
- end))
+ (fun it s ->
+ prerr_endline "Should recenter ?";
+ if String.contains s '\n' then begin
+ prerr_endline "Should recenter : yes";
+ self#recenter_insert
+ end));
end
-let create_input_tab filename =
- let b = GText.buffer () in
- let _ = GMisc.label () in
- let v_box = GPack.hbox ~homogeneous:false () in
- let _ = GMisc.image ~packing:v_box#pack () in
- let _ = GMisc.label ~text:filename ~packing:v_box#pack () in
- let appendp x = ignore ((notebook ())#append_page
- ~tab_label:v_box#coerce x) in
- let fr1 = GBin.frame ~shadow_type:`ETCHED_OUT
- ~packing:appendp ()
- in
- let sw1 = GBin.scrolled_window
- ~vpolicy:`AUTOMATIC
- ~hpolicy:`AUTOMATIC
- ~packing:fr1#add ()
- in
- let tv1 = Undo.undoable_view ~buffer:b ~packing:(sw1#add) () in
- prerr_endline ("Language: "^ b#start_iter#language);
- tv1#misc#set_name "ScriptWindow";
- let _ = tv1#set_editable true in
- let _ = tv1#set_wrap_mode `NONE in
- b#place_cursor ~where:(b#start_iter);
- ignore (tv1#event#connect#button_press ~callback:
- (fun ev -> GdkEvent.Button.button ev = 3));
- (* ignore (tv1#event#connect#button_press ~callback:
- (fun ev ->
- if (GdkEvent.Button.button ev=2) then
- (try
- prerr_endline "Paste invoked";
- GtkSignal.emit_unit
- (get_current_view()).view#as_view
- GtkText.View.Signals.paste_clipboard;
- true
- with _ -> false)
- else false
- ));*)
- tv1#misc#grab_focus ();
- ignore (tv1#buffer#create_mark
- ~name:"start_of_input"
- tv1#buffer#start_iter);
- ignore (tv1#buffer#create_tag
- ~name:"kwd"
- [`FOREGROUND "blue"]);
- ignore (tv1#buffer#create_tag
- ~name:"decl"
- [`FOREGROUND "orange red"]);
- ignore (tv1#buffer#create_tag
- ~name:"comment"
- [`FOREGROUND "brown"]);
- ignore (tv1#buffer#create_tag
- ~name:"reserved"
- [`FOREGROUND "dark red"]);
- ignore (tv1#buffer#create_tag
- ~name:"error"
- [`UNDERLINE `DOUBLE ; `FOREGROUND "red"]);
- ignore (tv1#buffer#create_tag
- ~name:"to_process"
- [`BACKGROUND "light blue" ;`EDITABLE false]);
- ignore (tv1#buffer#create_tag
- ~name:"processed"
- [`BACKGROUND "light green" ;`EDITABLE false]);
- ignore (tv1#buffer#create_tag (* Proof mode *)
- ~name:"unjustified"
- [`UNDERLINE `SINGLE ; `FOREGROUND "red";
- `BACKGROUND "gold" ;`EDITABLE false]);
- ignore (tv1#buffer#create_tag
- ~name:"found"
- [`BACKGROUND "blue"; `FOREGROUND "white"]);
- tv1
-
-
let last_make = ref "";;
let last_make_index = ref 0;;
let search_compile_error_regexp =
@@ -1823,20 +1457,228 @@ let search_next_error () =
and b = int_of_string (Str.matched_group 3 !last_make)
and e = int_of_string (Str.matched_group 4 !last_make)
and msg_index = Str.match_beginning ()
- in
- last_make_index := Str.group_end 4;
+ in
+ last_make_index := Str.group_end 4;
(f,l,b,e,
String.sub !last_make msg_index (String.length !last_make - msg_index))
-let main files =
+
+
+(**********************************************************************)
+(* session creation and primitive handling *)
+(**********************************************************************)
+
+let create_session () =
+ let script =
+ Undo.undoable_view
+ ~buffer:(GText.buffer ~tag_table:Tags.Script.table ())
+ ~wrap_mode:`NONE () in
+ let proof =
+ GText.view
+ ~buffer:(GText.buffer ~tag_table:Tags.Proof.table ())
+ ~editable:false ~wrap_mode:`CHAR () in
+ let message =
+ GText.view
+ ~buffer:(GText.buffer ~tag_table:Tags.Message.table ())
+ ~editable:false ~wrap_mode:`WORD () in
+ let basename =
+ GMisc.label ~text:"*scratch*" () in
+ let stack =
+ Stack.create () in
+ let legacy_av =
+ new analyzed_view script proof message stack in
+ let _ =
+ script#buffer#create_mark ~name:"start_of_input" script#buffer#start_iter in
+ let _ =
+ proof#buffer#create_mark ~name:"end_of_conclusion" proof#buffer#start_iter in
+ let _ =
+ GtkBase.Widget.add_events proof#as_widget [`ENTER_NOTIFY;`POINTER_MOTION] in
+ let _ =
+ proof#event#connect#motion_notify ~callback:
+ (fun e ->
+ let win = match proof#get_window `WIDGET with
+ | None -> assert false
+ | Some w -> w in
+ let x,y = Gdk.Window.get_pointer_location win in
+ let b_x,b_y = proof#window_to_buffer_coords ~tag:`WIDGET ~x ~y in
+ let it = proof#get_iter_at_location ~x:b_x ~y:b_y in
+ let tags = it#tags in
+ List.iter
+ (fun t ->
+ ignore (GtkText.Tag.event t#as_tag proof#as_widget e it#as_iter))
+ tags;
+ false) in
+ script#misc#set_name "ScriptWindow";
+ script#buffer#place_cursor ~where:(script#buffer#start_iter);
+ proof#misc#set_can_focus true;
+ message#misc#set_can_focus true;
+ script#misc#modify_font !current.text_font;
+ proof#misc#modify_font !current.text_font;
+ message#misc#modify_font !current.text_font;
+ { tab_label=basename;
+ filename="";
+ script=script;
+ proof_view=proof;
+ message_view=message;
+ analyzed_view=legacy_av;
+ command_stack=stack;
+ encoding=""
+ }
+
+(* XXX - to be used later
+let load_session session filename encs =
+ session.encoding <- List.find (IdeIO.load filename session.script#buffer) encs;
+ session.tab_label#set_text (Glib.Convert.filename_to_utf8 (Filename.basename filename));
+ session.filename <- filename;
+ session.script#buffer#set_modified false
+
+
+let save_session session filename encs =
+ session.encoding <- List.find (IdeIO.save session.script#buffer filename) encs;
+ session.tab_label#set_text (Glib.Convert.filename_to_utf8 (Filename.basename filename));
+ session.filename <- filename;
+ session.script#buffer#set_modified false
+
+
+let init_session session =
+ session.script#buffer#set_modified false;
+ session.script#clear_undo;
+ session.script#buffer#place_cursor session.script#buffer#start_iter
+ *)
+
+
+
+
+(*********************************************************************)
+(* functions called by the user interface *)
+(*********************************************************************)
+(* XXX - to be used later
+let do_open session filename =
+ try
+ load_session session filename ["UTF-8";"ISO-8859-1";"ISO-8859-15"];
+ init_session session;
+ ignore (session_notebook#append_term session)
+ with _ -> ()
+
+
+let do_save session =
+ try
+ if session.script#buffer#modified then
+ save_session session session.filename [session.encoding]
+ with _ -> ()
+
+
+let choose_open =
+ let last_filename = ref "" in fun session ->
+ let open_dialog = GWindow.file_chooser_dialog ~action:`OPEN ~title:"Open file" ~modal:true () in
+ let enc_frame = GBin.frame ~label:"File encoding" ~packing:(open_dialog#vbox#pack ~fill:false) () in
+ let enc_entry = GEdit.entry ~text:(String.concat " " ["UTF-8";"ISO-8859-1";"ISO-8859-15"]) ~packing:enc_frame#add () in
+ let error_dialog = GWindow.message_dialog ~message_type:`ERROR ~modal:true ~buttons:GWindow.Buttons.ok
+ ~message:"Invalid encoding, please indicate the encoding to use." () in
+ let open_response = function
+ | `OPEN -> begin
+ match open_dialog#filename with
+ | Some fn -> begin
+ try
+ load_session session fn (Util.split_string_at ' ' enc_entry#text);
+ session.analyzed_view <- Some (new analyzed_view session);
+ init_session session;
+ session_notebook#goto_page (session_notebook#append_term session);
+ last_filename := fn
+ with
+ | Not_found -> open_dialog#misc#hide (); error_dialog#show ()
+ | _ ->
+ error_dialog#set_markup "Unknown error while loading file, aborting.";
+ open_dialog#destroy (); error_dialog#destroy ()
+ end
+ | None -> ()
+ end
+ | `DELETE_EVENT -> open_dialog#destroy (); error_dialog#destroy ()
+ in
+ let _ = open_dialog#connect#response open_response in
+ let _ = error_dialog#connect#response (fun x -> error_dialog#misc#hide (); open_dialog#show ()) in
+ let filter_any = GFile.filter ~name:"Any" ~patterns:["*"] () in
+ let filter_coq = GFile.filter ~name:"Coq source" ~patterns:["*.v"] () in
+ open_dialog#add_select_button_stock `OPEN `OPEN;
+ open_dialog#add_button_stock `CANCEL `DELETE_EVENT;
+ open_dialog#add_filter filter_any;
+ open_dialog#add_filter filter_coq;
+ ignore(open_dialog#set_filename !last_filename);
+ open_dialog#show ()
+
+
+let choose_save session =
+ let save_dialog = GWindow.file_chooser_dialog ~action:`SAVE ~title:"Save file" ~modal:true () in
+ let enc_frame = GBin.frame ~label:"File encoding" ~packing:(save_dialog#vbox#pack ~fill:false) () in
+ let enc_entry = GEdit.entry ~text:(String.concat " " [session.encoding;"UTF-8";"ISO-8859-1";"ISO-8859-15"]) ~packing:enc_frame#add () in
+ let error_dialog = GWindow.message_dialog ~message_type:`ERROR ~modal:true ~buttons:GWindow.Buttons.ok
+ ~message:"Invalid encoding, please indicate the encoding to use." () in
+ let save_response = function
+ | `SAVE -> begin
+ match save_dialog#filename with
+ | Some fn -> begin
+ try
+ save_session session fn (Util.split_string_at ' ' enc_entry#text)
+ with
+ | Not_found -> save_dialog#misc#hide (); error_dialog#show ()
+ | _ ->
+ error_dialog#set_markup "Unknown error while saving file, aborting.";
+ save_dialog#destroy (); error_dialog#destroy ()
+ end
+ | None -> ()
+ end
+ | `DELETE_EVENT -> save_dialog#destroy (); error_dialog#destroy ()
+ in
+ let _ = save_dialog#connect#response save_response in
+ let _ = error_dialog#connect#response (fun x -> error_dialog#misc#hide (); save_dialog#show ()) in
+ let filter_any = GFile.filter ~name:"Any" ~patterns:["*"] () in
+ let filter_coq = GFile.filter ~name:"Coq source" ~patterns:["*.v"] () in
+ save_dialog#add_select_button_stock `SAVE `SAVE;
+ save_dialog#add_button_stock `CANCEL `DELETE_EVENT;
+ save_dialog#add_filter filter_any;
+ save_dialog#add_filter filter_coq;
+ ignore(save_dialog#set_filename session.filename);
+ save_dialog#show ()
+ *)
+
+let do_print session =
+ let av = session.analyzed_view in
+ if session.filename = ""
+ then flash_info "Cannot print: this buffer has no name"
+ else begin
+ let cmd =
+ "cd " ^ Filename.quote (Filename.dirname session.filename) ^ "; " ^
+ !current.cmd_coqdoc ^ " -ps " ^ Filename.quote (Filename.basename session.filename) ^
+ " | " ^ !current.cmd_print
+ in
+ let print_window = GWindow.window ~title:"Print" ~modal:true ~position:`CENTER ~wm_class:"CoqIDE" ~wm_name: "CoqIDE" () in
+ let vbox_print = GPack.vbox ~spacing:10 ~border_width:10 ~packing:print_window#add () in
+ let _ = GMisc.label ~justify:`LEFT ~text:"Print using the following command:" ~packing:vbox_print#add () in
+ let print_entry = GEdit.entry ~text:cmd ~editable:true ~width_chars:80 ~packing:vbox_print#add () in
+ let hbox_print = GPack.hbox ~spacing:10 ~packing:vbox_print#add () in
+ let print_cancel_button = GButton.button ~stock:`CANCEL ~label:"Cancel" ~packing:hbox_print#add () in
+ let print_button = GButton.button ~stock:`PRINT ~label:"Print" ~packing:hbox_print#add () in
+ let callback_print () =
+ let cmd = print_entry#text in
+ let s,_ = run_command av#insert_message cmd in
+ flash_info (cmd ^ if s = Unix.WEXITED 0 then " succeeded" else " failed");
+ print_window#destroy ()
+ in
+ ignore (print_cancel_button#connect#clicked ~callback:print_window#destroy) ;
+ ignore (print_button#connect#clicked ~callback:callback_print);
+ print_window#misc#show ()
+ end
+
+
+let main files =
(* Statup preferences *)
load_pref ();
(* Main window *)
- let w = GWindow.window
+ let w = GWindow.window
~wm_class:"CoqIde" ~wm_name:"CoqIde"
- ~allow_grow:true ~allow_shrink:true
- ~width:!current.window_width ~height:!current.window_height
+ ~allow_grow:true ~allow_shrink:true
+ ~width:!current.window_width ~height:!current.window_height
~title:"CoqIde" ()
in
(try
@@ -1852,15 +1694,15 @@ let main files =
let menubar = GMenu.menu_bar ~packing:vbox#pack () in
(* Toolbar *)
- let toolbar = GButton.toolbar
- ~orientation:`HORIZONTAL
+ let toolbar = GButton.toolbar
+ ~orientation:`HORIZONTAL
~style:`ICONS
- ~tooltips:true
+ ~tooltips:true
~packing:(* handle#add *)
(vbox#pack ~expand:false ~fill:false)
()
in
- show_toolbar :=
+ show_toolbar :=
(fun b -> if b then toolbar#misc#show () else toolbar#misc#hide ());
let factory = new GMenu.factory ~accel_path:"<CoqIde MenuBar>/" menubar in
@@ -1873,17 +1715,20 @@ let main files =
(* File/Load Menu *)
let load_file handler f =
- let f = absolute_filename f in
+ let f = absolute_filename f in
try
prerr_endline "Loading file starts";
- Vector.find_or_fail
- (function
- | {analyzed_view=Some av} ->
- (match av#filename with
- | None -> false
- | Some fn -> same_file f fn)
- | _ -> false)
- !input_views;
+ if not (Util.list_fold_left_i
+ (fun i found x -> if found then found else
+ let {analyzed_view=av} = x in
+ (match av#filename with
+ | None -> false
+ | Some fn ->
+ if same_file f fn
+ then (session_notebook#goto_page i; true)
+ else false))
+ 0 false session_notebook#pages)
+ then begin
prerr_endline "Loading: must open";
let b = Buffer.create 1024 in
prerr_endline "Loading: get raw content";
@@ -1891,290 +1736,231 @@ let main files =
prerr_endline "Loading: convert content";
let s = do_convert (Buffer.contents b) in
prerr_endline "Loading: create view";
- let view = create_input_tab (Glib.Convert.filename_to_utf8
- (Filename.basename f))
- in
- prerr_endline "Loading: change font";
- view#misc#modify_font !current.text_font;
+ let session = create_session () in
+ session.tab_label#set_text (Glib.Convert.filename_to_utf8 (Filename.basename f));
prerr_endline "Loading: adding view";
- let index = add_input_view {view = view;
- analyzed_view = None;
- }
- in
- let av = (new analyzed_view index) in
- prerr_endline "Loading: register view";
- (get_input_view index).analyzed_view <- Some av;
+ let index = session_notebook#append_term session in
+ let av = session.analyzed_view in
prerr_endline "Loading: set filename";
av#set_filename (Some f);
prerr_endline "Loading: stats";
av#update_stats;
- let input_buffer = view#buffer in
+ let input_buffer = session.script#buffer in
prerr_endline "Loading: fill buffer";
input_buffer#set_text s;
input_buffer#place_cursor input_buffer#start_iter;
prerr_endline ("Loading: switch to view "^ string_of_int index);
- set_current_view index;
- set_tab_image index ~icon:`YES;
+ session_notebook#goto_page index;
prerr_endline "Loading: highlight";
- Highlight.highlight_all input_buffer;
input_buffer#set_modified false;
prerr_endline "Loading: clear undo";
- av#view#clear_undo;
+ session.script#clear_undo;
prerr_endline "Loading: success"
- with
- | Vector.Found i -> set_current_view i
+ end
+ with
| e -> handler ("Load failed: "^(Printexc.to_string e))
in
- let load f = load_file !flash_info f in
- let load_m = file_factory#add_item "_New"
+ let load f = load_file flash_info f in
+ let load_m = file_factory#add_item "_New"
~key:GdkKeysyms._N in
- let load_f () =
- match select_file_for_save ~title:"Create file" () with
+ let load_f () =
+ match select_file_for_save ~title:"Create file" () with
| None -> ()
| Some f -> load f
in
ignore (load_m#connect#activate (load_f));
- let load_m = file_factory#add_item "_Open"
+ let load_m = file_factory#add_item "_Open"
~key:GdkKeysyms._O in
- let load_f () =
- match select_file_for_open ~title:"Load file" () with
+ let load_f () =
+ match select_file_for_open ~title:"Load file" () with
| None -> ()
| Some f -> load f
in
ignore (load_m#connect#activate (load_f));
(* File/Save Menu *)
- let save_m = file_factory#add_item "_Save"
+ let save_m = file_factory#add_item "_Save"
~key:GdkKeysyms._S in
-
-
- let save_f () =
- let current = get_current_view () in
+ let save_f () =
+ let current = session_notebook#current_term in
try
- (match (Option.get current.analyzed_view)#filename with
+ (match current.analyzed_view#filename with
| None ->
begin match select_file_for_save ~title:"Save file" ()
with
| None -> ()
- | Some f ->
- if (Option.get current.analyzed_view)#save_as f then begin
- set_current_tab_label (Filename.basename f);
- !flash_info ("File " ^ f ^ " saved")
+ | Some f ->
+ if current.analyzed_view#save_as f then begin
+ current.tab_label#set_text (Filename.basename f);
+ flash_info ("File " ^ f ^ " saved")
end
else warning ("Save Failed (check if " ^ f ^ " is writable)")
end
- | Some f ->
- if (Option.get current.analyzed_view)#save f then
- !flash_info ("File " ^ f ^ " saved")
+ | Some f ->
+ if current.analyzed_view#save f then
+ flash_info ("File " ^ f ^ " saved")
else warning ("Save Failed (check if " ^ f ^ " is writable)")
-
+
)
- with
+ with
| e -> warning "Save: unexpected error"
- in
+ in
ignore (save_m#connect#activate save_f);
(* File/Save As Menu *)
- let saveas_m = file_factory#add_item "S_ave as"
+ let saveas_m = file_factory#add_item "S_ave as"
in
- let saveas_f () =
- let current = get_current_view () in
- try (match (Option.get current.analyzed_view)#filename with
- | None ->
+ let saveas_f () =
+ let current = session_notebook#current_term in
+ try (match current.analyzed_view#filename with
+ | None ->
begin match select_file_for_save ~title:"Save file as" ()
with
| None -> ()
- | Some f ->
- if (Option.get current.analyzed_view)#save_as f then begin
- set_current_tab_label (Filename.basename f);
- !flash_info "Saved"
+ | Some f ->
+ if current.analyzed_view#save_as f then begin
+ current.tab_label#set_text (Filename.basename f);
+ flash_info "Saved"
end
- else !flash_info "Save Failed"
+ else flash_info "Save Failed"
end
- | Some f ->
- begin match select_file_for_save
- ~dir:(ref (Filename.dirname f))
+ | Some f ->
+ begin match select_file_for_save
+ ~dir:(ref (Filename.dirname f))
~filename:(Filename.basename f)
~title:"Save file as" ()
with
| None -> ()
- | Some f ->
- if (Option.get current.analyzed_view)#save_as f then begin
- set_current_tab_label (Filename.basename f);
- !flash_info "Saved"
- end else !flash_info "Save Failed"
+ | Some f ->
+ if current.analyzed_view#save_as f then begin
+ current.tab_label#set_text (Filename.basename f);
+ flash_info "Saved"
+ end else flash_info "Save Failed"
end);
- with e -> !flash_info "Save Failed"
- in
+ with e -> flash_info "Save Failed"
+ in
ignore (saveas_m#connect#activate saveas_f);
-
+ (* XXX *)
(* File/Save All Menu *)
let saveall_m = file_factory#add_item "Sa_ve all" in
- let saveall_f () =
- Vector.iter
- (function
- | {view = view ; analyzed_view = Some av} ->
- begin match av#filename with
+ let saveall_f () =
+ List.iter
+ (function
+ | {script = view ; analyzed_view = av} ->
+ begin match av#filename with
| None -> ()
| Some f ->
ignore (av#save f)
end
- | _ -> ()
- ) input_views
+ ) session_notebook#pages
in
- let has_something_to_save () =
- Vector.exists
- (function
- | {view=view} -> view#buffer#modified
+ (* XXX *)
+ let has_something_to_save () =
+ List.exists
+ (function
+ | {script=view} -> view#buffer#modified
)
- input_views
+ session_notebook#pages
in
ignore (saveall_m#connect#activate saveall_f);
-
+ (* XXX *)
(* File/Revert Menu *)
let revert_m = file_factory#add_item "_Revert all buffers" in
- let revert_f () =
- Vector.iter
- (function
- {view = view ; analyzed_view = Some av} ->
- (try
- match av#filename,av#stats with
- | Some f,Some stats ->
+ let revert_f () =
+ List.iter
+ (function
+ {analyzed_view = av} ->
+ (try
+ match av#filename,av#stats with
+ | Some f,Some stats ->
let new_stats = Unix.stat f in
- if new_stats.Unix.st_mtime > stats.Unix.st_mtime
+ if new_stats.Unix.st_mtime > stats.Unix.st_mtime
then av#revert
| Some _, None -> av#revert
| _ -> ()
with _ -> av#revert)
- | _ -> ()
- ) input_views
+ ) session_notebook#pages
in
ignore (revert_m#connect#activate revert_f);
-
+
(* File/Close Menu *)
let close_m =
file_factory#add_item "_Close buffer" ~key:GdkKeysyms._W in
- let close_f () =
- let v = Option.get !active_view in
- let act = get_current_view_page () in
- if v = act then !flash_info "Cannot close an active view"
+ let close_f () =
+ let v = !active_view in
+ let act = session_notebook#current_page in
+ if v = act then flash_info "Cannot close an active view"
else remove_current_view_page ()
in
ignore (close_m#connect#activate close_f);
-
+
(* File/Print Menu *)
- let print_f () =
- let v = get_current_view () in
- let av = Option.get v.analyzed_view in
- match av#filename with
- | None ->
- !flash_info "Cannot print: this buffer has no name"
- | Some f ->
- let cmd =
- "cd " ^ Filename.quote (Filename.dirname f) ^ "; " ^
- !current.cmd_coqdoc ^ " -ps " ^ Filename.quote (Filename.basename f) ^
- " | " ^ !current.cmd_print
- in
- let print_window = GWindow.window
- ~title:"Print"
- ~modal:true
- ~position:`CENTER
- ~wm_class:"CodIDE"
- ~wm_name: "CodIDE" () in
- let vbox_print = GPack.vbox
- ~spacing:10
- ~border_width:10
- ~packing:print_window#add () in
- let _ = GMisc.label
- ~justify:`LEFT
- ~text:"Print using the following command:"
- ~packing:vbox_print#add () in
- let print_entry = GEdit.entry
- ~text:cmd
- ~editable:true
- ~width_chars:80
- ~packing:vbox_print#add () in
- let hbox_print = GPack.hbox
- ~spacing:10
- ~packing:vbox_print#add () in
- let print_cancel_button = GButton.button ~stock:`CANCEL ~label:"Cancel" ~packing:hbox_print#add () in
- let print_button = GButton.button ~stock:`PRINT ~label:"Print" ~packing:hbox_print#add () in
- let callback_print () =
- let cmd = print_entry#text in
- let s,_ = run_command av#insert_message cmd in
- !flash_info (cmd ^ if s = Unix.WEXITED 0 then " succeeded" else " failed");
- print_window#destroy ()
- in
- ignore (print_cancel_button#connect#clicked ~callback:print_window#destroy) ;
- ignore (print_button#connect#clicked ~callback:callback_print);
- print_window#misc#show();
- in
let _ = file_factory#add_item "_Print..."
~key:GdkKeysyms._P
- ~callback:print_f in
+ ~callback:(fun () -> do_print session_notebook#current_term) in
(* File/Export to Menu *)
let export_f kind () =
- let v = get_current_view () in
- let av = Option.get v.analyzed_view in
+ let v = session_notebook#current_term in
+ let av = v.analyzed_view in
match av#filename with
- | None ->
- !flash_info "Cannot print: this buffer has no name"
+ | None ->
+ flash_info "Cannot print: this buffer has no name"
| Some f ->
let basef = Filename.basename f in
- let output =
+ let output =
let basef_we = try Filename.chop_extension basef with _ -> basef in
match kind with
| "latex" -> basef_we ^ ".tex"
| "dvi" | "ps" | "pdf" | "html" -> basef_we ^ "." ^ kind
| _ -> assert false
in
- let cmd =
+ let cmd =
"cd " ^ Filename.quote (Filename.dirname f) ^ "; " ^
!current.cmd_coqdoc ^ " --" ^ kind ^ " -o " ^ (Filename.quote output) ^ " " ^ (Filename.quote basef)
in
let s,_ = run_command av#insert_message cmd in
- !flash_info (cmd ^
- if s = Unix.WEXITED 0
- then " succeeded"
+ flash_info (cmd ^
+ if s = Unix.WEXITED 0
+ then " succeeded"
else " failed")
in
let file_export_m = file_factory#add_submenu "E_xport to" in
let file_export_factory = new GMenu.factory ~accel_path:"<CoqIde MenuBar>/Export/" file_export_m ~accel_group in
- let _ =
- file_export_factory#add_item "_Html" ~callback:(export_f "html")
+ let _ =
+ file_export_factory#add_item "_Html" ~callback:(export_f "html")
in
- let _ =
+ let _ =
file_export_factory#add_item "_LaTeX" ~callback:(export_f "latex")
in
- let _ =
- file_export_factory#add_item "_Dvi" ~callback:(export_f "dvi")
+ let _ =
+ file_export_factory#add_item "_Dvi" ~callback:(export_f "dvi")
in
- let _ =
- file_export_factory#add_item "_Pdf" ~callback:(export_f "pdf")
+ let _ =
+ file_export_factory#add_item "_Pdf" ~callback:(export_f "pdf")
in
- let _ =
- file_export_factory#add_item "_Ps" ~callback:(export_f "ps")
+ let _ =
+ file_export_factory#add_item "_Ps" ~callback:(export_f "ps")
in
(* File/Rehighlight Menu *)
let rehighlight_m = file_factory#add_item "Reh_ighlight" ~key:GdkKeysyms._L in
- ignore (rehighlight_m#connect#activate
- (fun () ->
- Highlight.highlight_all
- (get_current_view()).view#buffer;
- (Option.get (get_current_view()).analyzed_view)#recenter_insert));
+ ignore (rehighlight_m#connect#activate
+ (fun () ->
+ force_retag
+ session_notebook#current_term.script#buffer;
+ session_notebook#current_term.analyzed_view#recenter_insert));
(* File/Quit Menu *)
let quit_f () =
save_pref();
- if has_something_to_save () then
+ if has_something_to_save () then
match (GToolbox.question_box ~title:"Quit"
~buttons:["Save Named Buffers and Quit";
"Quit without Saving";
- "Don't Quit"]
+ "Don't Quit"]
~default:0
~icon:
(let img = GMisc.image () in
@@ -2188,7 +1974,7 @@ let main files =
| _ -> ()
else exit 0
in
- let _ = file_factory#add_item "_Quit" ~key:GdkKeysyms._Q
+ let _ = file_factory#add_item "_Quit" ~key:GdkKeysyms._Q
~callback:quit_f
in
ignore (w#event#connect#delete (fun _ -> quit_f (); true));
@@ -2198,50 +1984,60 @@ let main files =
let edit_f = new GMenu.factory ~accel_path:"<CoqIde MenuBar>/Edit/" edit_menu ~accel_group in
ignore(edit_f#add_item "_Undo" ~key:GdkKeysyms._u ~callback:
(do_if_not_computing "undo"
- (fun () ->
- ignore ((Option.get ((get_current_view()).analyzed_view))#
- without_auto_complete
- (fun () -> (get_current_view()).view#undo) ()))));
- ignore(edit_f#add_item "_Clear Undo Stack"
+ (fun () ->
+ ignore (session_notebook#current_term.analyzed_view#
+ without_auto_complete
+ (fun () -> session_notebook#current_term.script#undo) ()))));
+ ignore(edit_f#add_item "_Clear Undo Stack"
(* ~key:GdkKeysyms._exclam *)
~callback:
- (fun () ->
- ignore (get_current_view()).view#clear_undo));
+ (fun () ->
+ ignore session_notebook#current_term.script#clear_undo));
ignore(edit_f#add_separator ());
+ let get_active_view_for_cp () =
+ let has_sel (i0,i1) = i0#compare i1 <> 0 in
+ let current = session_notebook#current_term in
+ if has_sel current.script#buffer#selection_bounds
+ then current.script#as_view
+ else if has_sel current.proof_view#buffer#selection_bounds
+ then current.proof_view#as_view
+ else current.message_view#as_view
+ in
ignore(edit_f#add_item "Cut" ~key:GdkKeysyms._X ~callback:
(fun () -> GtkSignal.emit_unit
- (get_current_view()).view#as_view
- GtkText.View.S.cut_clipboard));
+ (get_active_view_for_cp ())
+ GtkText.View.S.cut_clipboard
+ ));
ignore(edit_f#add_item "Copy" ~key:GdkKeysyms._C ~callback:
(fun () -> GtkSignal.emit_unit
- (get_current_view()).view#as_view
+ (get_active_view_for_cp ())
GtkText.View.S.copy_clipboard));
ignore(edit_f#add_item "Paste" ~key:GdkKeysyms._V ~callback:
- (fun () ->
+ (fun () ->
try GtkSignal.emit_unit
- (get_current_view()).view#as_view
+ session_notebook#current_term.script#as_view
GtkText.View.S.paste_clipboard
with _ -> prerr_endline "EMIT PASTE FAILED"));
ignore (edit_f#add_separator ());
(*
- let toggle_auto_complete_i =
- edit_f#add_check_item "_Auto Completion"
+ let toggle_auto_complete_i =
+ edit_f#add_check_item "_Auto Completion"
~active:!current.auto_complete
~callback:
in
*)
(*
- auto_complete :=
- (fun b -> match (get_current_view()).analyzed_view with
+ auto_complete :=
+ (fun b -> match session_notebook#current_term.analyzed_view with
| Some av -> av#set_auto_complete b
| None -> ());
*)
let last_found = ref None in
let search_backward = ref false in
- let find_w = GWindow.window
+ let find_w = GWindow.window
(* ~wm_class:"CoqIde" ~wm_name:"CoqIde" *)
(* ~allow_grow:true ~allow_shrink:true *)
(* ~width:!current.window_width ~height:!current.window_height *)
@@ -2252,38 +2048,38 @@ let main files =
~columns:3 ~rows:5
~col_spacings:10 ~row_spacings:10 ~border_width:10
~homogeneous:false ~packing:find_w#add () in
-
- let _ =
+
+ let _ =
GMisc.label ~text:"Find:"
~xalign:1.0
- ~packing:(find_box#attach ~left:0 ~top:0 ~fill:`X) ()
+ ~packing:(find_box#attach ~left:0 ~top:0 ~fill:`X) ()
in
let find_entry = GEdit.entry
~editable: true
~packing: (find_box#attach ~left:1 ~top:0 ~expand:`X)
()
in
- let _ =
+ let _ =
GMisc.label ~text:"Replace with:"
~xalign:1.0
- ~packing:(find_box#attach ~left:0 ~top:1 ~fill:`X) ()
+ ~packing:(find_box#attach ~left:0 ~top:1 ~fill:`X) ()
in
let replace_entry = GEdit.entry
~editable: true
~packing: (find_box#attach ~left:1 ~top:1 ~expand:`X)
()
in
- (* let _ =
+ (* let _ =
GButton.check_button
~label:"case sensitive"
~active:true
~packing: (find_box#attach ~left:1 ~top:2)
()
-
+
in
*)
(*
- let find_backwards_check =
+ let find_backwards_check =
GButton.check_button
~label:"search backwards"
~active:false
@@ -2322,25 +2118,25 @@ let main files =
()
in
let last_find () =
- let v = (get_current_view()).view in
+ let v = session_notebook#current_term.script in
let b = v#buffer in
let start,stop =
- match !last_found with
+ match !last_found with
| None -> let i = b#get_iter_at_mark `INSERT in (i,i)
| Some(start,stop) ->
let start = b#get_iter_at_mark start
and stop = b#get_iter_at_mark stop
in
- b#remove_tag_by_name ~start ~stop "found";
+ b#remove_tag Tags.Script.found ~start ~stop;
last_found:=None;
start,stop
in
(v,b,start,stop)
in
let do_replace () =
- let v = (get_current_view()).view in
+ let v = session_notebook#current_term.script in
let b = v#buffer in
- match !last_found with
+ match !last_found with
| None -> ()
| Some(start,stop) ->
let start = b#get_iter_at_mark start
@@ -2358,7 +2154,7 @@ let main files =
with
| None -> ()
| Some(start,stop) ->
- b#apply_tag_by_name "found" ~start ~stop;
+ b#apply_tag Tags.Script.found ~start ~stop;
let start = `MARK (b#create_mark start)
and stop = `MARK (b#create_mark stop)
in
@@ -2368,7 +2164,7 @@ let main files =
in
let do_find () =
let (v,b,starti,_) = last_find () in
- find_from v b starti find_entry#text
+ find_from v b starti find_entry#text
in
let do_replace_find () =
do_replace();
@@ -2380,8 +2176,8 @@ let main files =
find_w#misc#hide();
v#coerce#misc#grab_focus()
in
- to_do_on_page_switch :=
- (fun i -> if find_w#misc#visible then close_find())::
+ to_do_on_page_switch :=
+ (fun i -> if find_w#misc#visible then close_find())::
!to_do_on_page_switch;
let find_again_forward () =
search_backward := false;
@@ -2403,12 +2199,12 @@ let main files =
find_w#misc#hide();
v#coerce#misc#grab_focus();
true
- end
+ end
else if k = GdkKeysyms._Return then
begin
close_find();
true
- end
+ end
else if List.mem `CONTROL s && k = GdkKeysyms._f then
begin
find_again_forward ();
@@ -2421,7 +2217,7 @@ let main files =
end
else false (* to let default callback execute *)
in
- let find_f ~backward () =
+ let find_f ~backward () =
search_backward := backward;
find_w#show ();
find_w#present ();
@@ -2455,30 +2251,30 @@ let main files =
let complete_i = edit_f#add_item "_Complete"
~key:GdkKeysyms._comma
~callback:
- (do_if_not_computing
- (fun b ->
- let v = Option.get (get_current_view ()).analyzed_view
-
- in v#complete_at_offset
+ (do_if_not_computing
+ (fun b ->
+ let v = session_notebook#current_term.analyzed_view
+
+ in v#complete_at_offset
((v#view#buffer#get_iter `SEL_BOUND)#offset)
))
in
complete_i#misc#set_state `INSENSITIVE;
*)
-
+
ignore(edit_f#add_item "Complete Word" ~key:GdkKeysyms._slash ~callback:
- (fun () ->
+ (fun () ->
ignore (
- let av = Option.get ((get_current_view()).analyzed_view) in
+ let av = session_notebook#current_term.analyzed_view in
av#complete_at_offset (av#get_insert)#offset
)));
ignore(edit_f#add_separator ());
(* external editor *)
- let _ =
+ let _ =
edit_f#add_item "External editor" ~callback:
- (fun () ->
- let av = Option.get ((get_current_view()).analyzed_view) in
+ (fun () ->
+ let av = session_notebook#current_term.analyzed_view in
match av#filename with
| None -> warning "Call to external editor available only on named files"
| Some f ->
@@ -2491,34 +2287,33 @@ let main files =
(* Preferences *)
let reset_revert_timer () =
disconnect_revert_timer ();
- if !current.global_auto_revert then
+ if !current.global_auto_revert then
revert_timer := Some
- (GMain.Timeout.add ~ms:!current.global_auto_revert_delay
+ (GMain.Timeout.add ~ms:!current.global_auto_revert_delay
~callback:
- (fun () ->
+ (fun () ->
do_if_not_computing "revert" (sync revert_f) ();
true))
in reset_revert_timer (); (* to enable statup preferences timer *)
-
- let auto_save_f () =
- Vector.iter
- (function
- {view = view ; analyzed_view = Some av} ->
- (try
+ (* XXX *)
+ let auto_save_f () =
+ List.iter
+ (function
+ {script = view ; analyzed_view = av} ->
+ (try
av#auto_save
with _ -> ())
- | _ -> ()
- )
- input_views
+ )
+ session_notebook#pages
in
let reset_auto_save_timer () =
disconnect_auto_save_timer ();
- if !current.auto_save then
+ if !current.auto_save then
auto_save_timer := Some
- (GMain.Timeout.add ~ms:!current.auto_save_delay
+ (GMain.Timeout.add ~ms:!current.auto_save_delay
~callback:
- (fun () ->
+ (fun () ->
do_if_not_computing "autosave" (sync auto_save_f) ();
true))
in reset_auto_save_timer (); (* to enable statup preferences timer *)
@@ -2536,34 +2331,40 @@ let main files =
*)
(* Navigation Menu *)
let navigation_menu = factory#add_submenu "_Navigation" in
- let navigation_factory =
- new GMenu.factory navigation_menu
+ let navigation_factory =
+ new GMenu.factory navigation_menu
~accel_path:"<CoqIde MenuBar>/Navigation/"
- ~accel_group
- ~accel_modi:!current.modifier_for_navigation
+ ~accel_group
+ ~accel_modi:!current.modifier_for_navigation
in
- let do_or_activate f () =
- let current = get_current_view () in
- let analyzed_view = Option.get current.analyzed_view in
- if analyzed_view#is_active then
+ let _do_or_activate f () =
+ let current = session_notebook#current_term in
+ let analyzed_view = current.analyzed_view in
+ if analyzed_view#is_active then begin
+ prerr_endline ("view "^current.tab_label#text^"already active");
ignore (f analyzed_view)
- else
+ end else
begin
- !flash_info "New proof started";
- activate_input (notebook ())#current_page;
+ flash_info "New proof started";
+ prerr_endline ("activating view "^current.tab_label#text);
+ activate_input session_notebook#current_page;
ignore (f analyzed_view)
end
in
- let do_or_activate f =
+ let do_or_activate f =
do_if_not_computing "do_or_activate"
- (do_or_activate
- (fun av -> f av ; !pop_info();!push_info (Coq.current_status())))
+ (_do_or_activate
+ (fun av -> f av;
+ pop_info ();
+ push_info (Coq.current_status())
+ )
+ )
in
- let add_to_menu_toolbar text ~tooltip ?key ~callback icon =
+ let add_to_menu_toolbar text ~tooltip ?key ~callback icon =
begin
- match key with None -> ()
+ match key with None -> ()
| Some key -> ignore (navigation_factory#add_item text ~key ~callback)
end;
ignore (toolbar#insert_button
@@ -2573,107 +2374,106 @@ let main files =
~callback
())
in
- add_to_menu_toolbar
- "_Save"
- ~tooltip:"Save current buffer"
+ add_to_menu_toolbar
+ "_Save"
+ ~tooltip:"Save current buffer"
~callback:save_f
`SAVE;
- add_to_menu_toolbar
- "_Close"
- ~tooltip:"Close current buffer"
+ add_to_menu_toolbar
+ "_Close"
+ ~tooltip:"Close current buffer"
~callback:close_f
`CLOSE;
- add_to_menu_toolbar
- "_Forward"
- ~tooltip:"Forward one command"
- ~key:GdkKeysyms._Down
- ~callback:(do_or_activate (fun a -> a#process_next_phrase true true true))
+ add_to_menu_toolbar
+ "_Forward"
+ ~tooltip:"Forward one command"
+ ~key:GdkKeysyms._Down
+ ~callback:(do_or_activate (fun a -> a#process_next_phrase true true true ))
+
`GO_DOWN;
add_to_menu_toolbar "_Backward"
- ~tooltip:"Backward one command"
+ ~tooltip:"Backward one command"
~key:GdkKeysyms._Up
~callback:(do_or_activate (fun a -> a#undo_last_step))
`GO_UP;
- add_to_menu_toolbar
- "_Go to"
- ~tooltip:"Go to cursor"
+ add_to_menu_toolbar
+ "_Go to"
+ ~tooltip:"Go to cursor"
~key:GdkKeysyms._Right
~callback:(do_or_activate (fun a-> a#go_to_insert))
`JUMP_TO;
- add_to_menu_toolbar
- "_Start"
- ~tooltip:"Go to start"
+ add_to_menu_toolbar
+ "_Start"
+ ~tooltip:"Go to start"
~key:GdkKeysyms._Home
~callback:(do_or_activate (fun a -> a#reset_initial))
`GOTO_TOP;
- add_to_menu_toolbar
- "_End"
- ~tooltip:"Go to end"
+ add_to_menu_toolbar
+ "_End"
+ ~tooltip:"Go to end"
~key:GdkKeysyms._End
~callback:(do_or_activate (fun a -> a#process_until_end_or_error))
`GOTO_BOTTOM;
add_to_menu_toolbar "_Interrupt"
- ~tooltip:"Interrupt computations"
- ~key:GdkKeysyms._Break
+ ~tooltip:"Interrupt computations"
+ ~key:GdkKeysyms._Break
~callback:break
`STOP;
+ add_to_menu_toolbar "_Hide"
+ ~tooltip:"Hide proof"
+ ~key:GdkKeysyms._h
+ ~callback:(fun x ->
+ let sess = session_notebook#current_term in
+ toggle_proof_visibility sess.script#buffer
+ sess.analyzed_view#get_insert)
+ `MISSING_IMAGE;
(* Tactics Menu *)
let tactics_menu = factory#add_submenu "_Try Tactics" in
- let tactics_factory =
- new GMenu.factory tactics_menu
+ let tactics_factory =
+ new GMenu.factory tactics_menu
~accel_path:"<CoqIde MenuBar>/Tactics/"
- ~accel_group
+ ~accel_group
~accel_modi:!current.modifier_for_tactics
in
- let do_if_active_raw f () =
- let current = get_current_view () in
- let analyzed_view = Option.get current.analyzed_view in
+ let do_if_active_raw f () =
+ let current = session_notebook#current_term in
+ let analyzed_view = current.analyzed_view in
if analyzed_view#is_active then ignore (f analyzed_view)
in
let do_if_active f =
do_if_not_computing "do_if_active" (do_if_active_raw f) in
- (*
- let blaster_i =
- tactics_factory#add_item "_Blaster"
- ~key:GdkKeysyms._b
- ~callback: (do_if_active_raw (fun a -> a#blaster ()))
- (* Custom locking mechanism! *)
- in
- blaster_i#misc#set_state `INSENSITIVE;
- *)
-
- ignore (tactics_factory#add_item "_auto"
+ ignore (tactics_factory#add_item "_auto"
~key:GdkKeysyms._a
~callback:(do_if_active (fun a -> a#insert_command "progress auto.\n" "auto.\n"))
);
ignore (tactics_factory#add_item "_auto with *"
~key:GdkKeysyms._asterisk
- ~callback:(do_if_active (fun a -> a#insert_command
+ ~callback:(do_if_active (fun a -> a#insert_command
"progress auto with *.\n"
"auto with *.\n")));
ignore (tactics_factory#add_item "_eauto"
~key:GdkKeysyms._e
- ~callback:(do_if_active (fun a -> a#insert_command
+ ~callback:(do_if_active (fun a -> a#insert_command
"progress eauto.\n"
"eauto.\n"))
);
ignore (tactics_factory#add_item "_eauto with *"
~key:GdkKeysyms._ampersand
- ~callback:(do_if_active (fun a -> a#insert_command
- "progress eauto with *.\n"
+ ~callback:(do_if_active (fun a -> a#insert_command
+ "progress eauto with *.\n"
"eauto with *.\n"))
);
ignore (tactics_factory#add_item "_intuition"
~key:GdkKeysyms._i
- ~callback:(do_if_active (fun a -> a#insert_command
- "progress intuition.\n"
+ ~callback:(do_if_active (fun a -> a#insert_command
+ "progress intuition.\n"
"intuition.\n"))
);
ignore (tactics_factory#add_item "_omega"
~key:GdkKeysyms._o
- ~callback:(do_if_active (fun a -> a#insert_command
+ ~callback:(do_if_active (fun a -> a#insert_command
"omega.\n" "omega.\n"))
);
ignore (tactics_factory#add_item "_simpl"
@@ -2703,15 +2503,15 @@ let main files =
ignore (tactics_factory#add_item "<Proof _Wizard>"
~key:GdkKeysyms._dollar
- ~callback:(do_if_active (fun a -> a#tactic_wizard
+ ~callback:(do_if_active (fun a -> a#tactic_wizard
!current.automatic_tactics
))
);
-
+
ignore (tactics_factory#add_separator ());
- let add_simple_template (factory: GMenu.menu GMenu.factory)
+ let add_simple_template (factory: GMenu.menu GMenu.factory)
(menu_text, text) =
- let text =
+ let text =
let l = String.length text - 1 in
if String.get text l = '.'
then text ^"\n"
@@ -2719,42 +2519,42 @@ let main files =
in
ignore (factory#add_item menu_text
~callback:
- (fun () -> let {view = view } = get_current_view () in
+ (fun () -> let {script = view } = session_notebook#current_term in
ignore (view#buffer#insert_interactive text)))
in
- List.iter
- (fun l ->
- match l with
+ List.iter
+ (fun l ->
+ match l with
| [] -> ()
- | [s] -> add_simple_template tactics_factory ("_"^s, s)
- | s::_ ->
+ | [s] -> add_simple_template tactics_factory ("_"^s, s)
+ | s::_ ->
let a = "_@..." in
a.[1] <- s.[0];
- let f = tactics_factory#add_submenu a in
+ let f = tactics_factory#add_submenu a in
let ff = new GMenu.factory f ~accel_group in
- List.iter
- (fun x ->
+ List.iter
+ (fun x ->
add_simple_template
- ff
+ ff
((String.sub x 0 1)^
"_"^
(String.sub x 1 (String.length x - 1)),
x))
l
- )
+ )
Coq_commands.tactics;
-
+
(* Templates Menu *)
let templates_menu = factory#add_submenu "Te_mplates" in
- let templates_factory = new GMenu.factory templates_menu
+ let templates_factory = new GMenu.factory templates_menu
~accel_path:"<CoqIde MenuBar>/Templates/"
- ~accel_group
+ ~accel_group
~accel_modi:!current.modifier_for_templates
in
let add_complex_template (menu_text, text, offset, len, key) =
(* Templates/Lemma *)
let callback () =
- let {view = view } = get_current_view () in
+ let {script = view } = session_notebook#current_term in
if view#buffer#insert_interactive text then begin
let iter = view#buffer#get_iter_at_mark `INSERT in
ignore (iter#nocopy#backward_chars offset);
@@ -2764,19 +2564,19 @@ let main files =
end in
ignore (templates_factory#add_item menu_text ~callback ?key)
in
- add_complex_template
- ("_Lemma __", "Lemma new_lemma : .\nProof.\n\nSave.\n",
+ add_complex_template
+ ("_Lemma __", "Lemma new_lemma : .\nProof.\n\nSave.\n",
19, 9, Some GdkKeysyms._L);
- add_complex_template
- ("_Theorem __", "Theorem new_theorem : .\nProof.\n\nSave.\n",
+ add_complex_template
+ ("_Theorem __", "Theorem new_theorem : .\nProof.\n\nSave.\n",
19, 11, Some GdkKeysyms._T);
- add_complex_template
+ add_complex_template
("_Definition __", "Definition ident := .\n",
6, 5, Some GdkKeysyms._D);
- add_complex_template
+ add_complex_template
("_Inductive __", "Inductive ident : :=\n | : .\n",
14, 5, Some GdkKeysyms._I);
- add_complex_template
+ add_complex_template
("_Fixpoint __", "Fixpoint ident (_ : _) {struct _} : _ :=\n.\n",
29, 5, Some GdkKeysyms._F);
add_complex_template("_Scheme __",
@@ -2784,14 +2584,14 @@ let main files =
with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
(* Template for match *)
- let callback () =
+ let callback () =
let w = get_current_word () in
- try
+ try
let cases = Coq.make_cases w
in
let print c = function
| [x] -> Format.fprintf c " | %s => _@\n" x
- | x::l -> Format.fprintf c " | (%s%a) => _@\n" x
+ | x::l -> Format.fprintf c " | (%s%a) => _@\n" x
(print_list (fun c s -> Format.fprintf c " %s" s)) l
| [] -> assert false
in
@@ -2801,28 +2601,28 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
(print_list print) cases;
let s = Buffer.contents b in
prerr_endline s;
- let {view = view } = get_current_view () in
+ let {script = view } = session_notebook#current_term in
ignore (view#buffer#delete_selection ());
- let m = view#buffer#create_mark
+ let m = view#buffer#create_mark
(view#buffer#get_iter `INSERT)
in
- if view#buffer#insert_interactive s then
+ if view#buffer#insert_interactive s then
let i = view#buffer#get_iter (`MARK m) in
let _ = i#nocopy#forward_chars 9 in
view#buffer#place_cursor i;
view#buffer#move_mark ~where:(i#backward_chars 3)
- `SEL_BOUND
- with Not_found -> !flash_info "Not an inductive type"
+ `SEL_BOUND
+ with Not_found -> flash_info "Not an inductive type"
in
ignore (templates_factory#add_item "match ..."
~key:GdkKeysyms._C
~callback
);
-
+
(*
- let add_simple_template (factory: GMenu.menu GMenu.factory)
+ let add_simple_template (factory: GMenu.menu GMenu.factory)
(menu_text, text) =
- let text =
+ let text =
let l = String.length text - 1 in
if String.get text l = '.'
then text ^"\n"
@@ -2830,7 +2630,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
in
ignore (factory#add_item menu_text
~callback:
- (fun () -> let {view = view } = get_current_view () in
+ (fun () -> let {view = view } = session_notebook#current_term in
ignore (view#buffer#insert_interactive text)))
in
*)
@@ -2849,92 +2649,100 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
];
ignore (templates_factory#add_separator ());
*)
- List.iter
- (fun l ->
- match l with
+ List.iter
+ (fun l ->
+ match l with
| [] -> ()
- | [s] -> add_simple_template templates_factory ("_"^s, s)
- | s::_ ->
+ | [s] -> add_simple_template templates_factory ("_"^s, s)
+ | s::_ ->
let a = "_@..." in
a.[1] <- s.[0];
- let f = templates_factory#add_submenu a in
+ let f = templates_factory#add_submenu a in
let ff = new GMenu.factory f ~accel_group in
- List.iter
- (fun x ->
- add_simple_template
- ff
+ List.iter
+ (fun x ->
+ add_simple_template
+ ff
((String.sub x 0 1)^
"_"^
(String.sub x 1 (String.length x - 1)),
x))
l
- )
+ )
Coq_commands.commands;
-
+
(* Queries Menu *)
let queries_menu = factory#add_submenu "_Queries" in
let queries_factory = new GMenu.factory queries_menu ~accel_group
~accel_path:"<CoqIde MenuBar>/Queries"
~accel_modi:[]
in
-
+
(* Command/Show commands *)
- let _ =
+ let _ =
queries_factory#add_item "_SearchAbout " ~key:GdkKeysyms._F2
~callback:(fun () -> let term = get_current_word () in
(Command_windows.command_window ())#new_command
~command:"SearchAbout"
- ~term
+ ~term
())
in
- let _ =
+ let _ =
queries_factory#add_item "_Check " ~key:GdkKeysyms._F3
~callback:(fun () -> let term = get_current_word () in
(Command_windows.command_window ())#new_command
~command:"Check"
- ~term
+ ~term
())
in
- let _ =
+ let _ =
queries_factory#add_item "_Print " ~key:GdkKeysyms._F4
~callback:(fun () -> let term = get_current_word () in
(Command_windows.command_window ())#new_command
~command:"Print"
- ~term
+ ~term
+ ())
+ in
+ let _ =
+ queries_factory#add_item "_About " ~key:GdkKeysyms._F5
+ ~callback:(fun () -> let term = get_current_word () in
+ (Command_windows.command_window ())#new_command
+ ~command:"About"
+ ~term
())
in
- let _ =
- queries_factory#add_item "_Locate"
+ let _ =
+ queries_factory#add_item "_Locate"
~callback:(fun () -> let term = get_current_word () in
(Command_windows.command_window ())#new_command
~command:"Locate"
- ~term
+ ~term
())
in
- let _ =
- queries_factory#add_item "_Whelp Locate"
+ let _ =
+ queries_factory#add_item "_Whelp Locate"
~callback:(fun () -> let term = get_current_word () in
(Command_windows.command_window ())#new_command
~command:"Whelp Locate"
- ~term
+ ~term
())
in
(* Display menu *)
-
+
let display_menu = factory#add_submenu "_Display" in
let view_factory = new GMenu.factory display_menu
~accel_path:"<CoqIde MenuBar>/Display/"
- ~accel_group
+ ~accel_group
~accel_modi:!current.modifier_for_display
in
- let _ = ignore (view_factory#add_check_item
- "Display _implicit arguments"
+ let _ = ignore (view_factory#add_check_item
+ "Display _implicit arguments"
~key:GdkKeysyms._i
~callback:(fun _ -> printing_state.printing_implicit <- not printing_state.printing_implicit; do_or_activate (fun a -> a#show_goals) ())) in
- let _ = ignore (view_factory#add_check_item
+ let _ = ignore (view_factory#add_check_item
"Display _coercions"
~key:GdkKeysyms._c
~callback:(fun _ -> printing_state.printing_coercions <- not printing_state.printing_coercions; do_or_activate (fun a -> a#show_goals) ())) in
@@ -2944,104 +2752,77 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
~key:GdkKeysyms._m
~callback:(fun _ -> printing_state.printing_raw_matching <- not printing_state.printing_raw_matching; do_or_activate (fun a -> a#show_goals) ())) in
- let _ = ignore (view_factory#add_check_item
+ let _ = ignore (view_factory#add_check_item
"Deactivate _notations display"
~key:GdkKeysyms._n
~callback:(fun _ -> printing_state.printing_no_notation <- not printing_state.printing_no_notation; do_or_activate (fun a -> a#show_goals) ())) in
- let _ = ignore (view_factory#add_check_item
+ let _ = ignore (view_factory#add_check_item
"Display _all basic low-level contents"
~key:GdkKeysyms._a
- ~callback:(fun _ -> printing_state.printing_all <- not printing_state.printing_all; do_or_activate (fun a -> a#show_goals) ())) in
+ ~callback:(fun _ -> printing_state.printing_all <- not printing_state.printing_all; do_or_activate (fun a -> a#show_goals) ())) in
- let _ = ignore (view_factory#add_check_item
+ let _ = ignore (view_factory#add_check_item
"Display _existential variable instances"
~key:GdkKeysyms._e
~callback:(fun _ -> printing_state.printing_evar_instances <- not printing_state.printing_evar_instances; do_or_activate (fun a -> a#show_goals) ())) in
- let _ = ignore (view_factory#add_check_item
+ let _ = ignore (view_factory#add_check_item
"Display _universe levels"
~key:GdkKeysyms._u
~callback:(fun _ -> printing_state.printing_universes <- not printing_state.printing_universes; do_or_activate (fun a -> a#show_goals) ())) in
- let _ = ignore (view_factory#add_check_item
+ let _ = ignore (view_factory#add_check_item
"Display all _low-level contents"
~key:GdkKeysyms._l
- ~callback:(fun _ -> printing_state.printing_full_all <- not printing_state.printing_full_all; do_or_activate (fun a -> a#show_goals) ())) in
+ ~callback:(fun _ -> printing_state.printing_full_all <- not printing_state.printing_full_all; do_or_activate (fun a -> a#show_goals) ())) in
+
+
- (* Unicode *)
-(*
- let unicode_menu = factory#add_submenu "_Unicode" in
- let unicode_factory = new GMenu.factory unicode_menu
- ~accel_path:"<CoqIde MenuBar>/Unicode/"
- ~accel_group
- ~accel_modi:[]
- in
- let logic_symbols_menu = unicode_factory#add_submenu "Math operators" in
- let logic_factory = new GMenu.factory logic_symbols_menu
- ~accel_path:"<CoqIde MenuBar>/Unicode/Math operators"
- ~accel_group
- ~accel_modi:[]
- in
- let new_unicode_item s = ignore (
- logic_factory#add_item s
- ~callback:(fun () ->
- let v = get_current_view () in
- ignore (v.view#buffer#insert_interactive s)))
- in
-
- for i = 0x2200 to 0x22FF do
- List.iter new_unicode_item [Glib.Utf8.from_unichar i];
-
- done;
-
-*)
-
-
(* Externals *)
let externals_menu = factory#add_submenu "_Compile" in
- let externals_factory = new GMenu.factory externals_menu
+ let externals_factory = new GMenu.factory externals_menu
~accel_path:"<CoqIde MenuBar>/Compile/"
- ~accel_group
+ ~accel_group
~accel_modi:[]
in
-
+
(* Command/Compile Menu *)
let compile_f () =
- let v = get_current_view () in
- let av = Option.get v.analyzed_view in
+ let v = session_notebook#current_term in
+ let av = v.analyzed_view in
save_f ();
match av#filename with
- | None ->
- !flash_info "Active buffer has no name"
+ | None ->
+ flash_info "Active buffer has no name"
| Some f ->
- let cmd = !current.cmd_coqc ^ " -I "
+ let cmd = !current.cmd_coqc ^ " -I "
^ (Filename.quote (Filename.dirname f))
^ " " ^ (Filename.quote f) in
let s,res = run_command av#insert_message cmd in
if s = Unix.WEXITED 0 then
- !flash_info (f ^ " successfully compiled")
+ flash_info (f ^ " successfully compiled")
else begin
- !flash_info (f ^ " failed to compile");
- activate_input (notebook ())#current_page;
+ flash_info (f ^ " failed to compile");
+ activate_input session_notebook#current_page;
av#process_until_end_or_error;
av#insert_message "Compilation output:\n";
av#insert_message res
end
in
- let _ =
- externals_factory#add_item "_Compile Buffer" ~callback:compile_f
+ let _ =
+ externals_factory#add_item "_Compile Buffer" ~callback:compile_f
in
(* Command/Make Menu *)
let make_f () =
- let v = get_current_view () in
- let av = Option.get v.analyzed_view in
+ let v = session_notebook#current_term in
+ let av = v.analyzed_view in
match av#filename with
- | None ->
- !flash_info "Cannot make: this buffer has no name"
+ | None ->
+ flash_info "Cannot make: this buffer has no name"
| Some f ->
- let cmd =
+ let cmd =
"cd " ^ Filename.quote (Filename.dirname f) ^ "; " ^ !current.cmd_make in
(*
@@ -3051,22 +2832,22 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
let s,res = run_command av#insert_message cmd in
last_make := res;
last_make_index := 0;
- !flash_info (!current.cmd_make ^ if s = Unix.WEXITED 0 then " succeeded" else " failed")
+ flash_info (!current.cmd_make ^ if s = Unix.WEXITED 0 then " succeeded" else " failed")
in
- let _ = externals_factory#add_item "_Make"
+ let _ = externals_factory#add_item "_Make"
~key:GdkKeysyms._F6
- ~callback:make_f
+ ~callback:make_f
in
-
+
(* Compile/Next Error *)
- let next_error () =
+ let next_error () =
try
let file,line,start,stop,error_msg = search_next_error () in
- load file;
- let v = get_current_view () in
- let av = Option.get v.analyzed_view in
- let input_buffer = v.view#buffer in
+ load file;
+ let v = session_notebook#current_term in
+ let av = v.analyzed_view in
+ let input_buffer = v.script#buffer in
(*
let init = input_buffer#start_iter in
let i = init#forward_lines (line-1) in
@@ -3082,215 +2863,143 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
*)
let starti = input_buffer#get_iter_at_byte ~line:(line-1) start in
let stopi = input_buffer#get_iter_at_byte ~line:(line-1) stop in
- input_buffer#apply_tag_by_name "error"
+ input_buffer#apply_tag Tags.Script.error
~start:starti
~stop:stopi;
input_buffer#place_cursor starti;
av#set_message error_msg;
- v.view#misc#grab_focus ()
+ v.script#misc#grab_focus ()
with Not_found ->
last_make_index := 0;
- let v = get_current_view () in
- let av = Option.get v.analyzed_view in
+ let v = session_notebook#current_term in
+ let av = v.analyzed_view in
av#set_message "No more errors.\n"
in
- let _ =
- externals_factory#add_item "_Next error"
+ let _ =
+ externals_factory#add_item "_Next error"
~key:GdkKeysyms._F7
~callback:next_error in
-
+
(* Command/CoqMakefile Menu*)
let coq_makefile_f () =
- let v = get_current_view () in
- let av = Option.get v.analyzed_view in
+ let v = session_notebook#current_term in
+ let av = v.analyzed_view in
match av#filename with
- | None ->
- !flash_info "Cannot make makefile: this buffer has no name"
+ | None ->
+ flash_info "Cannot make makefile: this buffer has no name"
| Some f ->
- let cmd =
+ let cmd =
"cd " ^ Filename.quote (Filename.dirname f) ^ "; " ^ !current.cmd_coqmakefile in
let s,res = run_command av#insert_message cmd in
- !flash_info
+ flash_info
(!current.cmd_coqmakefile ^ if s = Unix.WEXITED 0 then " succeeded" else " failed")
in
- let _ = externals_factory#add_item "_Make makefile" ~callback:coq_makefile_f
+ let _ = externals_factory#add_item "_Make makefile" ~callback:coq_makefile_f
in
(* Windows Menu *)
let configuration_menu = factory#add_submenu "_Windows" in
- let configuration_factory = new GMenu.factory configuration_menu
+ let configuration_factory = new GMenu.factory configuration_menu
~accel_path:"<CoqIde MenuBar>/Windows"
~accel_modi:[]
~accel_group
in
let _ =
- configuration_factory#add_item
+ configuration_factory#add_item
"Show/Hide _Query Pane"
~key:GdkKeysyms._Escape
- ~callback:(fun () -> if (Command_windows.command_window ())#frame#misc#visible then
+ ~callback:(fun () -> if (Command_windows.command_window ())#frame#misc#visible then
(Command_windows.command_window ())#frame#misc#hide ()
else
(Command_windows.command_window ())#frame#misc#show ())
- in
- let _ =
- configuration_factory#add_check_item
- "Show/Hide _Toolbar"
- ~callback:(fun _ ->
- !current.show_toolbar <- not !current.show_toolbar;
- !show_toolbar !current.show_toolbar)
- in
- let _ = configuration_factory#add_item
- "Detach _Script Window"
- ~callback:
- (do_if_not_computing "detach script window" (sync
- (fun () ->
- let nb = notebook () in
- if nb#misc#toplevel#get_oid=w#coerce#get_oid then
- begin
- let nw = GWindow.window
- ~width:(!current.window_width*2/3)
- ~height:(!current.window_height*2/3)
- ~position:`CENTER
- ~wm_name:"CoqIde"
- ~wm_class:"CoqIde"
- ~title:"Script"
- ~show:true () in
- let parent = Option.get nb#misc#parent in
- ignore (nw#connect#destroy
- ~callback:
- (fun () -> nb#misc#reparent parent));
- nw#add_accel_group accel_group;
- nb#misc#reparent nw#coerce
- end
- )))
in
-(* let _ = configuration_factory#add_item
- "Detach _Command Pane"
- ~callback:
- (do_if_not_computing "detach command pane" (sync
- (fun () ->
- let command_object = Command_windows.command_window() in
- let queries_frame = command_object#frame in
- if queries_frame#misc#toplevel#get_oid=w#coerce#get_oid then
- begin
- let nw = GWindow.window
- ~width:(!current.window_width*2/3)
- ~height:(!current.window_height*2/3)
- ~wm_name:"CoqIde"
- ~wm_class:"CoqIde"
- ~position:`CENTER
- ~title:"Queries"
- ~show:true () in
- let parent = Option.get queries_frame#misc#parent in
- ignore (nw#connect#destroy
- ~callback:
- (fun () -> queries_frame#misc#reparent parent));
- queries_frame#misc#show();
- queries_frame#misc#reparent nw#coerce
- end
- )))
+ let _ =
+ configuration_factory#add_check_item
+ "Show/Hide _Toolbar"
+ ~callback:(fun _ ->
+ !current.show_toolbar <- not !current.show_toolbar;
+ !show_toolbar !current.show_toolbar)
in
-*)
- let _ =
- configuration_factory#add_item
+ let _ =
+ configuration_factory#add_item
"Detach _View"
~callback:
(do_if_not_computing "detach view"
- (fun () ->
- match get_current_view () with
- | {view=v;analyzed_view=Some av} ->
- let w = GWindow.window ~show:true
+ (fun () ->
+ match session_notebook#current_term with
+ | {script=v;analyzed_view=av} ->
+ let w = GWindow.window ~show:true
~width:(!current.window_width*2/3)
~height:(!current.window_height*2/3)
~position:`CENTER
~title:(match av#filename with
| None -> "*Unnamed*"
- | Some f -> f)
- ()
+ | Some f -> f)
+ ()
in
- let sb = GBin.scrolled_window
- ~packing:w#add ()
+ let sb = GBin.scrolled_window
+ ~packing:w#add ()
in
- let nv = GText.view
- ~buffer:v#buffer
- ~packing:sb#add
+ let nv = GText.view
+ ~buffer:v#buffer
+ ~packing:sb#add
()
in
- nv#misc#modify_font
- !current.text_font;
- ignore (w#connect#destroy
+ nv#misc#modify_font
+ !current.text_font;
+ ignore (w#connect#destroy
~callback:
(fun () -> av#remove_detached_view w));
av#add_detached_view w
- | _ -> ()
-
+
))
in
(* Help Menu *)
let help_menu = factory#add_submenu "_Help" in
- let help_factory = new GMenu.factory help_menu
+ let help_factory = new GMenu.factory help_menu
~accel_path:"<CoqIde MenuBar>/Help/"
~accel_modi:[]
~accel_group in
- let _ = help_factory#add_item "Browse Coq _Manual"
+ let _ = help_factory#add_item "Browse Coq _Manual"
~callback:
- (fun () ->
- let av = Option.get ((get_current_view ()).analyzed_view) in
- browse av#insert_message (!current.doc_url)) in
- let _ = help_factory#add_item "Browse Coq _Library"
+ (fun () ->
+ let av = session_notebook#current_term.analyzed_view in
+ browse av#insert_message (doc_url ())) in
+ let _ = help_factory#add_item "Browse Coq _Library"
~callback:
- (fun () ->
- let av = Option.get ((get_current_view ()).analyzed_view) in
+ (fun () ->
+ let av = session_notebook#current_term.analyzed_view in
browse av#insert_message !current.library_url) in
- let _ =
+ let _ =
help_factory#add_item "Help for _keyword" ~key:GdkKeysyms._F1
- ~callback:(fun () ->
- let av = Option.get ((get_current_view ()).analyzed_view) in
+ ~callback:(fun () ->
+ let av = session_notebook#current_term.analyzed_view in
av#help_for_keyword ())
in
let _ = help_factory#add_separator () in
- (*
- let faq_m = help_factory#add_item "_FAQ" in
- *)
let about_m = help_factory#add_item "_About" in
(* End of menu *)
(* The vertical Separator between Scripts and Goals *)
let queries_pane = GPack.paned `VERTICAL ~packing:(vbox#pack ~expand:true ) () in
- let hb = GPack.paned `HORIZONTAL ~border_width:5 ~packing:(queries_pane#pack1 ~shrink:false ~resize:true) () in
- let fr_notebook = GBin.frame ~shadow_type:`IN ~packing:hb#add1 () in
- _notebook := Some (GPack.notebook ~border_width:2 ~show_border:false ~scrollable:true
- ~packing:fr_notebook#add
- ());
+ queries_pane#pack1 ~shrink:false ~resize:true session_notebook#coerce;
update_notebook_pos ();
- let nb = notebook () in
- let hb2 = GPack.paned `VERTICAL ~packing:hb#add2 () in
- let fr_a = GBin.frame ~shadow_type:`IN ~packing:hb2#add () in
- let fr_b = GBin.frame ~shadow_type:`IN ~packing:hb2#add () in
- let sw2 = GBin.scrolled_window
- ~vpolicy:`AUTOMATIC
- ~hpolicy:`AUTOMATIC
- ~packing:(fr_a#add) () in
- let sw3 = GBin.scrolled_window
- ~vpolicy:`AUTOMATIC
- ~hpolicy:`AUTOMATIC
- ~packing:(fr_b#add) () in
+ let nb = session_notebook in
let command_object = Command_windows.command_window() in
let queries_frame = command_object#frame in
queries_pane#pack2 ~shrink:false ~resize:false (queries_frame#coerce);
let lower_hbox = GPack.hbox ~homogeneous:false ~packing:vbox#pack () in
- let status_bar = GMisc.statusbar ~packing:(lower_hbox#pack ~expand:true) ()
- in
+ lower_hbox#pack ~expand:true status#coerce;
let search_lbl = GMisc.label ~text:"Search:"
~show:false
- ~packing:(lower_hbox#pack ~expand:false) ()
+ ~packing:(lower_hbox#pack ~expand:false) ()
in
let search_history = ref [] in
let search_input = GEdit.combo ~popdown_strings:!search_history
~enable_arrow_keys:true
~show:false
- ~packing:(lower_hbox#pack ~expand:false) ()
+ ~packing:(lower_hbox#pack ~expand:false) ()
in
search_input#disable_activate ();
let ready_to_wrap_search = ref false in
@@ -3301,108 +3010,99 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
let search_forward = ref true in
let matched_word = ref None in
- let memo_search () =
+ let memo_search () =
matched_word := Some search_input#entry#text
-
- (* if not (List.mem search_input#entry#text !search_history) then
- (search_history :=
- search_input#entry#text::!search_history;
- search_input#set_popdown_strings !search_history);
- start_of_search := None;
- ready_to_wrap_search := false
- *)
-
in
- let end_search () =
+ let end_search () =
prerr_endline "End Search";
memo_search ();
- let v = (get_current_view ()).view in
+ let v = session_notebook#current_term.script in
v#buffer#move_mark `SEL_BOUND (v#buffer#get_iter_at_mark `INSERT);
v#coerce#misc#grab_focus ();
search_input#entry#set_text "";
search_lbl#misc#hide ();
search_input#misc#hide ()
in
- let end_search_focus_out () =
+ let end_search_focus_out () =
prerr_endline "End Search(focus out)";
memo_search ();
- let v = (get_current_view ()).view in
+ let v = session_notebook#current_term.script in
v#buffer#move_mark `SEL_BOUND (v#buffer#get_iter_at_mark `INSERT);
search_input#entry#set_text "";
search_lbl#misc#hide ();
search_input#misc#hide ()
in
ignore (search_input#entry#connect#activate ~callback:end_search);
- ignore (search_input#entry#event#connect#key_press
+ ignore (search_input#entry#event#connect#key_press
~callback:(fun k -> let kv = GdkEvent.Key.keyval k in
- if
+ if
kv = GdkKeysyms._Right
- || kv = GdkKeysyms._Up
+ || kv = GdkKeysyms._Up
|| kv = GdkKeysyms._Left
- || (kv = GdkKeysyms._g
+ || (kv = GdkKeysyms._g
&& (List.mem `CONTROL (GdkEvent.Key.state k)))
- then end_search ();
+ then end_search ();
false));
ignore (search_input#entry#event#connect#focus_out
~callback:(fun _ -> end_search_focus_out (); false));
- to_do_on_page_switch :=
- (fun i ->
+ to_do_on_page_switch :=
+ (fun i ->
start_of_search := None;
ready_to_wrap_search:=false)::!to_do_on_page_switch;
(* TODO : make it work !!! *)
- let rec search_f () =
+ let rec search_f () =
search_lbl#misc#show ();
search_input#misc#show ();
prerr_endline "search_f called";
if !start_of_search = None then begin
(* A full new search is starting *)
- start_of_search :=
- Some ((get_current_view ()).view#buffer#create_mark
- ((get_current_view ()).view#buffer#get_iter_at_mark `INSERT));
+ start_of_search :=
+ Some (session_notebook#current_term.script#buffer#create_mark
+ (session_notebook#current_term.script#buffer#get_iter_at_mark `INSERT));
start_of_found := !start_of_search;
end_of_found := !start_of_search;
matched_word := Some "";
end;
- let txt = search_input#entry#text in
- let v = (get_current_view ()).view in
- let iit = v#buffer#get_iter_at_mark `SEL_BOUND
+ let txt = search_input#entry#text in
+ let v = session_notebook#current_term.script in
+ let iit = v#buffer#get_iter_at_mark `SEL_BOUND
and insert_iter = v#buffer#get_iter_at_mark `INSERT
in
prerr_endline ("SELBOUND="^(string_of_int iit#offset));
prerr_endline ("INSERT="^(string_of_int insert_iter#offset));
-
+
(match
- if !search_forward then iit#forward_search txt
+ if !search_forward then iit#forward_search txt
else let npi = iit#forward_chars (Glib.Utf8.length txt) in
- match
+ match
(npi#offset = (v#buffer#get_iter_at_mark `INSERT)#offset),
- (let t = iit#get_text ~stop:npi in
- !flash_info (t^"\n"^txt);
+ (let t = iit#get_text ~stop:npi in
+ flash_info (t^"\n"^txt);
t = txt)
- with
- | true,true ->
- (!flash_info "T,T";iit#backward_search txt)
- | false,true -> !flash_info "F,T";Some (iit,npi)
+ with
+ | true,true ->
+ (flash_info "T,T";iit#backward_search txt)
+ | false,true -> flash_info "F,T";Some (iit,npi)
| _,false ->
(iit#backward_search txt)
- with
- | None ->
+ with
+ | None ->
if !ready_to_wrap_search then begin
ready_to_wrap_search := false;
- !flash_info "Search wrapped";
- v#buffer#place_cursor
+ flash_info "Search wrapped";
+ v#buffer#place_cursor
(if !search_forward then v#buffer#start_iter else
v#buffer#end_iter);
search_f ()
end else begin
- if !search_forward then !flash_info "Search at end"
- else !flash_info "Search at start";
+ if !search_forward then flash_info "Search at end"
+ else flash_info "Search at start";
ready_to_wrap_search := true
end
- | Some (start,stop) ->
+ | Some (start,stop) ->
prerr_endline "search: before moving marks";
prerr_endline ("SELBOUND="^(string_of_int (v#buffer#get_iter_at_mark `SEL_BOUND)#offset));
prerr_endline ("INSERT="^(string_of_int (v#buffer#get_iter_at_mark `INSERT)#offset));
@@ -3415,105 +3115,49 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
v#scroll_to_mark `SEL_BOUND
)
in
- ignore (search_input#entry#event#connect#key_release
+ ignore (search_input#entry#event#connect#key_release
~callback:
(fun ev ->
if GdkEvent.Key.keyval ev = GdkKeysyms._Escape then begin
- let v = (get_current_view ()).view in
- (match !start_of_search with
- | None ->
+ let v = session_notebook#current_term.script in
+ (match !start_of_search with
+ | None ->
prerr_endline "search_key_rel: Placing sel_bound";
- v#buffer#move_mark
- `SEL_BOUND
+ v#buffer#move_mark
+ `SEL_BOUND
(v#buffer#get_iter_at_mark `INSERT)
- | Some mk -> let it = v#buffer#get_iter_at_mark
+ | Some mk -> let it = v#buffer#get_iter_at_mark
(`MARK mk) in
prerr_endline "search_key_rel: Placing cursor";
v#buffer#place_cursor it;
start_of_search := None
);
- search_input#entry#set_text "";
+ search_input#entry#set_text "";
v#coerce#misc#grab_focus ();
- end;
+ end;
false
));
ignore (search_input#entry#connect#changed search_f);
-
- (*
- ignore (search_if#connect#activate
- ~callback:(fun b ->
- search_forward:= true;
- search_input#entry#coerce#misc#grab_focus ();
- search_f ();
- )
- );
- ignore (search_ib#connect#activate
- ~callback:(fun b ->
- search_forward:= false;
-
- (* Must restore the SEL_BOUND mark after
- grab_focus ! *)
- let v = (get_current_view ()).view in
- let old_sel = v#buffer#get_iter_at_mark `SEL_BOUND
- in
- search_input#entry#coerce#misc#grab_focus ();
- v#buffer#move_mark `SEL_BOUND old_sel;
- search_f ();
- ));
- *)
- let status_context = status_bar#new_context "Messages" in
- let flash_context = status_bar#new_context "Flash" in
- ignore (status_context#push "Ready");
- status := Some status_bar;
- push_info := (fun s -> ignore (status_context#push s));
- pop_info := (fun () -> status_context#pop ());
- flash_info := (fun ?(delay=5000) s -> flash_context#flash ~delay s);
-
- (* Location display *)
+ push_info "Ready";
+ (* Location display *)
let l = GMisc.label
- ~text:"Line: 1 Char: 1"
- ~packing:lower_hbox#pack () in
+ ~text:"Line: 1 Char: 1"
+ ~packing:lower_hbox#pack () in
l#coerce#misc#set_name "location";
set_location := l#set_text;
-
(* Progress Bar *)
- pulse :=
- (let pb = GRange.progress_bar ~pulse_step:0.2 ~packing:lower_hbox#pack ()
- in pb#set_text "CoqIde started";pb)#pulse;
- let tv2 = GText.view ~packing:(sw2#add) () in
- tv2#misc#set_name "GoalWindow";
- let _ = tv2#set_editable false in
- let _ = tv2#buffer in
- let tv3 = GText.view ~packing:(sw3#add) () in
- tv2#misc#set_name "MessageWindow";
- let _ = tv2#set_wrap_mode `CHAR in
- let _ = tv3#set_wrap_mode `WORD in
- let _ = tv3#set_editable false in
- let _ = GtkBase.Widget.add_events tv2#as_widget
- [`ENTER_NOTIFY;`POINTER_MOTION] in
- let _ =
- tv2#event#connect#motion_notify
- ~callback:
- (fun e ->
- let win = match tv2#get_window `WIDGET with
- | None -> assert false
- | Some w -> w in
- let x,y = Gdk.Window.get_pointer_location win in
- let b_x,b_y = tv2#window_to_buffer_coords ~tag:`WIDGET ~x ~y in
- let it = tv2#get_iter_at_location ~x:b_x ~y:b_y in
- let tags = it#tags in
- List.iter
- (fun t ->
- ignore(GtkText.Tag.event t#as_tag tv2#as_widget e it#as_iter))
- tags;
- false) in
- change_font :=
- (fun fd ->
- tv2#misc#modify_font fd;
- tv3#misc#modify_font fd;
- Vector.iter
- (fun {view=view} -> view#misc#modify_font fd)
- input_views;
+ lower_hbox#pack pbar#coerce;
+ pbar#set_text "CoqIde started";
+ (* XXX *)
+ change_font :=
+ (fun fd ->
+ List.iter
+ (fun {script=view; proof_view=prf_v; message_view=msg_v} ->
+ view#misc#modify_font fd;
+ prf_v#misc#modify_font fd;
+ msg_v#misc#modify_font fd
+ )
+ session_notebook#pages;
);
let about_full_string =
"\nCoq is developed by the Coq Development Team\
@@ -3539,7 +3183,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
b#insert ~iter:b#start_iter "\n\n";
if Glib.Utf8.validate ("You are running " ^ coq_version) then b#insert ~iter:b#start_iter ("You are running " ^ coq_version);
if Glib.Utf8.validate initial_string then b#insert ~iter:b#start_iter initial_string;
- (try
+ (try
let image = lib_ide_file "coq.png" in
let startup_image = GdkPixbuf.from_file image in
b#insert ~iter:b#start_iter "\n\n";
@@ -3549,7 +3193,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
in
let about (b:GText.buffer) =
- (try
+ (try
let image = lib_ide_file "coq.png" in
let startup_image = GdkPixbuf.from_file image in
b#insert ~iter:b#start_iter "\n\n";
@@ -3563,77 +3207,30 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
then b#insert coq_version
in
- initial_about tv2#buffer;
w#add_accel_group accel_group;
(* Remove default pango menu for textviews *)
- ignore (tv2#event#connect#button_press ~callback:
- (fun ev -> GdkEvent.Button.button ev = 3));
- ignore (tv3#event#connect#button_press ~callback:
- (fun ev -> GdkEvent.Button.button ev = 3));
- tv2#misc#set_can_focus true;
- tv3#misc#set_can_focus true;
- ignore (tv2#buffer#create_mark
- ~name:"end_of_conclusion"
- tv2#buffer#start_iter);
- ignore (tv3#buffer#create_tag
- ~name:"error"
- [`FOREGROUND "red"]);
w#show ();
- message_view := Some tv3;
- proof_view := Some tv2;
- tv2#misc#modify_font !current.text_font;
- tv3#misc#modify_font !current.text_font;
- ignore (about_m#connect#activate
- ~callback:(fun () -> tv2#buffer#set_text ""; about tv2#buffer));
+ ignore (about_m#connect#activate
+ ~callback:(fun () -> let prf_v = session_notebook#current_term.proof_view in
+ prf_v#buffer#set_text ""; about prf_v#buffer));
(*
- ignore (faq_m#connect#activate
- ~callback:(fun () ->
- load (lib_ide_file "FAQ")));
-
+
*)
- resize_window := (fun () ->
- w#resize
+ resize_window := (fun () ->
+ w#resize
~width:!current.window_width
~height:!current.window_height);
-
- ignore (w#misc#connect#size_allocate
- (let old_w = ref 0
- and old_h = ref 0 in
- fun {Gtk.width=w;Gtk.height=h} ->
- if !old_w <> w or !old_h <> h then
- begin
- old_h := h;
- old_w := w;
- hb#set_position (w/2);
- hb2#set_position (h/2);
- !current.window_height <- h;
- !current.window_width <- w;
- end
- ));
- ignore(nb#connect#switch_page
+ ignore(nb#connect#switch_page
~callback:
- (fun i ->
+ (fun i ->
prerr_endline ("switch_page: starts " ^ string_of_int i);
List.iter (function f -> f i) !to_do_on_page_switch;
prerr_endline "switch_page: success")
);
- ignore(tv2#event#connect#enter_notify
- (fun _ ->
- if !current.contextual_menus_on_goal then
- begin
- let w = (Option.get (get_active_view ()).analyzed_view) in
- !push_info "Computing advanced goal's menus";
- prerr_endline "Entering Goal Window. Computing Menus....";
- w#show_goals_full;
- prerr_endline "....Done with Goal menu";
- !pop_info();
- end;
- false;
- ));
- if List.length files >=1 then
+ if List.length files >=1 then
begin
- List.iter (fun f ->
- if Sys.file_exists f then load f else
+ List.iter (fun f ->
+ if Sys.file_exists f then load f else
let f = if Filename.check_suffix f ".v" then f else f^".v" in
load_file (fun s -> print_endline s; exit 1) f)
files;
@@ -3641,69 +3238,66 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
end
else
begin
- let view = create_input_tab "*Unnamed Buffer*" in
- let index = add_input_view {view = view;
- analyzed_view = None;
- }
- in
- (get_input_view index).analyzed_view <- Some (new analyzed_view index);
+ let session = create_session () in
+ let index = session_notebook#append_term session in
activate_input index;
- set_tab_image index ~icon:`YES;
- view#misc#modify_font !current.text_font
end;
+ initial_about session_notebook#current_term.proof_view#buffer;
+ !show_toolbar !current.show_toolbar;
+ session_notebook#current_term.script#misc#grab_focus ()
;;
-(* This function check every half of second if GeoProof has send
+(* This function check every half of second if GeoProof has send
something on his private clipboard *)
-let rec check_for_geoproof_input () =
+let rec check_for_geoproof_input () =
let cb_Dr = GData.clipboard (Gdk.Atom.intern "_GeoProof") in
while true do
Thread.delay 0.1;
let s = cb_Dr#text in
- (match s with
- Some s ->
+ (match s with
+ Some s ->
if s <> "Ack" then
- (get_current_view()).view#buffer#insert (s^"\n");
+ session_notebook#current_term.script#buffer#insert (s^"\n");
cb_Dr#set_text "Ack"
| None -> ()
);
(* cb_Dr#clear does not work so i use : *)
- (* cb_Dr#set_text "Ack" *)
+ (* cb_Dr#set_text "Ack" *)
done
-
-
-let start () =
+
+
+let start () =
let files = Coq.init () in
ignore_break ();
GtkMain.Rc.add_default_file (lib_ide_file ".coqide-gtk2rc");
- (try
+ (try
GtkMain.Rc.add_default_file (Filename.concat System.home ".coqide-gtk2rc");
with Not_found -> ());
ignore (GtkMain.Main.init ());
- GtkData.AccelGroup.set_default_mod_mask
+ GtkData.AccelGroup.set_default_mod_mask
(Some [`CONTROL;`SHIFT;`MOD1;`MOD3;`MOD4]);
- cb_ := Some (GData.clipboard Gdk.Atom.primary);
ignore (
Glib.Message.set_log_handler ~domain:"Gtk" ~levels:[`ERROR;`FLAG_FATAL;
`WARNING;`CRITICAL]
- (fun ~level msg ->
+ (fun ~level msg ->
if level land Glib.Message.log_level `WARNING <> 0
then Pp.warning msg
else failwith ("Coqide internal error: " ^ msg)));
Command_windows.main ();
- Blaster_window.main 9;
init_stdout ();
main files;
- if !Coq_config.with_geoproof then ignore (Thread.create check_for_geoproof_input ());
- while true do
- try
- GtkThread.main ()
+ if !Coq_config.with_geoproof then ignore (Thread.create check_for_geoproof_input ());
+ while true do
+ try
+ GtkThread.main ()
with
| Sys.Break -> prerr_endline "Interrupted." ; flush stderr
- | e ->
+ | e ->
Pervasives.prerr_endline ("CoqIde unexpected error:" ^ (Printexc.to_string e));
flush stderr;
crash_save 127
done
+
+
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-16 04:02:26 +0000