summaryrefslogtreecommitdiff
path: root/ide/coqide.ml
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-11-21 21:38:49 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-11-21 21:38:49 +0000
commit208a0f7bfa5249f9795e6e225f309cbe715c0fad (patch)
tree591e9e512063e34099782e2518573f15ffeac003 /ide/coqide.ml
parentde0085539583f59dc7c4bf4e272e18711d565466 (diff)
Imported Upstream version 8.1~gammaupstream/8.1.gamma
Diffstat (limited to 'ide/coqide.ml')
-rw-r--r--ide/coqide.ml656
1 files changed, 373 insertions, 283 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml
index cfde925d..fb650cbf 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: coqide.ml 8932 2006-06-09 09:29:03Z notin $ *)
+(* $Id: coqide.ml 9307 2006-10-28 18:48:48Z herbelin $ *)
open Preferences
open Vernacexpr
@@ -175,8 +175,9 @@ object('self)
method reset_initial : unit
method send_to_coq :
bool -> bool -> string ->
- bool -> bool -> bool -> (Util.loc * Vernacexpr.vernac_expr) option
+ bool -> bool -> bool -> (bool*(Util.loc * Vernacexpr.vernac_expr)) option
method set_message : string -> unit
+ method show_pm_goal : unit
method show_goals : unit
method show_goals_full : unit
method undo_last_step : unit
@@ -327,10 +328,10 @@ let remove_current_view_page () =
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 is_word_char c =
- Glib.Unichar.isalnum c || c = underscore || c = prime || c = arobase
-
let starts_word it =
prerr_endline ("Starts word ? '"^(Glib.Utf8.from_unichar it#char)^"'");
(not it#copy#nocopy#backward_char ||
@@ -340,14 +341,14 @@ let starts_word it =
let ends_word it =
(not it#copy#nocopy#forward_char ||
let c = it#forward_char#char in
- not (Glib.Unichar.isalnum c || c = underscore || c = prime || c = arobase)
+ not (is_word_char c)
)
let inside_word it =
let c = it#char in
not (starts_word it) &&
not (ends_word it) &&
- (Glib.Unichar.isalnum c || c = underscore || c = prime || c = arobase)
+ is_word_char c
let is_on_word_limit it = inside_word it || ends_word it
@@ -789,50 +790,88 @@ object(self)
(String.make previous_line_spaces ' ')
end
+ method show_pm_goal =
+ proof_buffer#insert
+ (Printf.sprintf " *** Declarative Mode ***\n");
+ try
+ let (hyps,metas) = get_current_pm_goal () in
+ List.iter
+ (fun ((_,_,_,(s,_)) as _hyp) ->
+ proof_buffer#insert (s^"\n"))
+ hyps;
+ proof_buffer#insert
+ (String.make 38 '_' ^ "\n");
+ List.iter
+ (fun (_,_,m) ->
+ proof_buffer#insert (m^"\n"))
+ metas;
+ 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."
method show_goals =
try
proof_view#buffer#set_text "";
- 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)
- with e -> prerr_endline ("Don't worry be happy despite: "^Printexc.to_string e)
-
-
+ 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 =
@@ -840,148 +879,160 @@ object(self)
begin
try
proof_view#buffer#set_text "";
- let s = Coq.get_current_goals () in
- let last_shown_area = proof_buffer#create_tag [`BACKGROUND "light green"]
- 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"));
- 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
+ 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;
- with e -> prerr_endline (Printexc.to_string e)
+ 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)
end
-
+
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 Util.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";
- if replace then begin
- let r,info = Coq.interp_and_replace ("info " ^ phrase) in
- let msg = read_stdout () in
- sync display_output msg;
- Some r
- end else begin
- let r = Coq.interp verbosely phrase in
- let msg = read_stdout () in
- sync display_output msg;
- Some r
- end
- with e ->
- if show_error then sync display_error e;
- None
+ assert (Glib.Utf8.validate s);
+ self#insert_message s;
+ message_view#misc#draw None;
+ if localize then
+ (match Util.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";
@@ -1018,7 +1069,7 @@ object(self)
in
try
trash_bytes := "";
- let phrase = Find_phrase.get (Lexing.from_function lexbuf_function)
+ let _ = Find_phrase.get (Lexing.from_function lexbuf_function)
in
end_iter#nocopy#set_offset (start#offset + !Find_phrase.length);
Some (start,end_iter)
@@ -1089,10 +1140,11 @@ object(self)
input_view#set_editable true;
!pop_info ();
end in
- let mark_processed (start,stop) ast =
- let b = input_buffer in
+ let mark_processed complete (start,stop) ast =
+ let b = input_buffer in
b#move_mark ~where:stop (`NAME "start_of_input");
- b#apply_tag_by_name "processed" ~start ~stop;
+ 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;
@@ -1100,67 +1152,69 @@ object(self)
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
- start_of_phrase_mark
- end_of_phrase_mark ast;
- if display_goals then self#show_goals;
- remove_tag (start,stop) in
+ push_phrase
+ 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) ->
- (match self#send_to_coq verbosely false phrase true true true with
- | Some ast -> sync (mark_processed loc) ast; true
- | None -> sync remove_tag loc; false)
+ (match self#send_to_coq verbosely false phrase true true true with
+ | Some (complete,ast) ->
+ sync (mark_processed 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 ast =
+ let mark_processed complete ast =
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 "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 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
+ 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 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 start_of_phrase_mark end_of_phrase_mark ast
- end
+ 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 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 ast -> sync mark_processed ast; true
- | None ->
- sync
- (fun _ -> self#insert_message ("Unsuccessfully tried: "^coqphrase))
- ();
- false
+ | _ -> ())
+ with _ -> ()*) in
+ match self#send_to_coq false false coqphrase show_output show_msg localize with
+ | Some (complete,ast) -> sync (mark_processed complete) ast; true
+ | None ->
+ sync
+ (fun _ -> self#insert_message ("Unsuccessfully tried: "^coqphrase))
+ ();
+ false
method process_until_iter_or_error stop =
let stop' = `OFFSET stop#offset in
@@ -1170,20 +1224,29 @@ object(self)
input_buffer#apply_tag_by_name ~start ~stop "to_process";
input_view#set_editable false) ();
!push_info "Coq is computing";
- (try
- while ((stop#compare self#get_start_of_input>=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()
+ let get_current () =
+ 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 =
self#process_until_iter_or_error input_buffer#end_iter
@@ -1196,6 +1259,7 @@ object(self)
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;
)
@@ -1260,6 +1324,10 @@ object(self)
~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;
@@ -1269,9 +1337,9 @@ object(self)
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 (...)"
-
+ 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;
@@ -1296,6 +1364,10 @@ Please restart and report NOW.";
~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
@@ -1356,6 +1428,7 @@ Please restart and report NOW.";
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) =
@@ -1555,10 +1628,16 @@ Please restart and report NOW.";
~callback:(fun tag ~start ~stop ->
if (start#compare self#get_start_of_input)>=0
then
- input_buffer#remove_tag_by_name
- ~start
- ~stop
- "processed"
+ begin
+ input_buffer#remove_tag_by_name
+ ~start
+ ~stop
+ "processed";
+ input_buffer#remove_tag_by_name
+ ~start
+ ~stop
+ "unjustified"
+ end
)
);
ignore (input_buffer#connect#after#insert_text
@@ -1636,10 +1715,10 @@ end
let create_input_tab filename =
let b = GText.buffer () in
- let tablabel = GMisc.label () in
+ let _ = GMisc.label () in
let v_box = GPack.hbox ~homogeneous:false () in
- let image = GMisc.image ~packing:v_box#pack () in
- let label = GMisc.label ~text:filename ~packing:v_box#pack () in
+ let _ = GMisc.image ~packing:v_box#pack () in
+ let _ = GMisc.label ~text:filename ~packing:v_box#pack () in
let fr1 = GBin.frame ~shadow_type:`ETCHED_OUT
~packing:((notebook ())#append_page
~tab_label:v_box#coerce) ()
@@ -1694,6 +1773,10 @@ let create_input_tab filename =
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"]);
@@ -1933,7 +2016,8 @@ let main files =
ignore (revert_m#connect#activate revert_f);
(* File/Close Menu *)
- let close_m = file_factory#add_item "_Close Buffer" in
+ let close_m =
+ file_factory#add_item "_Close Buffer" ~key:GdkKeysyms._W in
let close_f () =
let v = out_some !active_view in
let act = get_current_view_page () in
@@ -1958,7 +2042,9 @@ let main files =
let s,_ = run_command av#insert_message cmd in
!flash_info (cmd ^ if s = Unix.WEXITED 0 then " succeeded" else " failed")
in
- let print_m = file_factory#add_item "_Print" ~callback:print_f in
+ let _ = file_factory#add_item "_Print"
+ ~key:GdkKeysyms._P
+ ~callback:print_f in
(* File/Export to Menu *)
let export_f kind () =
@@ -1989,16 +2075,16 @@ let main files =
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 export_html_m =
+ let _ =
file_export_factory#add_item "_Html" ~callback:(export_f "html")
in
- let export_latex_m =
+ let _ =
file_export_factory#add_item "_LaTeX" ~callback:(export_f "latex")
in
- let export_dvi_m =
+ let _ =
file_export_factory#add_item "_Dvi" ~callback:(export_f "dvi")
in
- let export_ps_m =
+ let _ =
file_export_factory#add_item "_Ps" ~callback:(export_f "ps")
in
@@ -2031,7 +2117,7 @@ let main files =
| _ -> ()
else exit 0
in
- let quit_m = 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));
@@ -2096,7 +2182,7 @@ let main files =
~col_spacings:10 ~row_spacings:10 ~border_width:10
~homogeneous:false ~packing:find_w#add () in
- let find_lbl =
+ let _ =
GMisc.label ~text:"Find:"
~xalign:1.0
~packing:(find_box#attach ~left:0 ~top:0 ~fill:`X) ()
@@ -2106,7 +2192,7 @@ let main files =
~packing: (find_box#attach ~left:1 ~top:0 ~expand:`X)
()
in
- let replace_lbl =
+ let _ =
GMisc.label ~text:"Replace with:"
~xalign:1.0
~packing:(find_box#attach ~left:0 ~top:1 ~fill:`X) ()
@@ -2116,7 +2202,7 @@ let main files =
~packing: (find_box#attach ~left:1 ~top:1 ~expand:`X)
()
in
- let case_sensitive_check =
+ let _ =
GButton.check_button
~label:"case sensitive"
~active:true
@@ -2268,11 +2354,11 @@ let main files =
find_w#present ();
find_entry#misc#grab_focus ()
in
- let find_i = edit_f#add_item "_Find in buffer"
+ let _ = edit_f#add_item "_Find in buffer"
~key:GdkKeysyms._F
~callback:(find_f ~backward:false)
in
- let find_back_i = edit_f#add_item "Find _backwards"
+ let _ = edit_f#add_item "Find _backwards"
~key:GdkKeysyms._B
~callback:(find_f ~backward:true)
in
@@ -2365,7 +2451,7 @@ let main files =
in reset_auto_save_timer (); (* to enable statup preferences timer *)
- let edit_prefs_m =
+ let _ =
edit_f#add_item "_Preferences"
~callback:(fun () -> configure ();reset_revert_timer ())
in
@@ -2417,10 +2503,14 @@ let main files =
add_to_menu_toolbar
"_Save"
~tooltip:"Save current buffer"
- (* ~key:GdkKeysyms._Down *)
~callback:save_f
`SAVE;
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
@@ -2779,7 +2869,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
av#insert_message res
end
in
- let compile_m =
+ let _ =
externals_factory#add_item "_Compile Buffer" ~callback:compile_f
in
@@ -2796,7 +2886,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
last_make_index := 0;
!flash_info (!current.cmd_make ^ if s = Unix.WEXITED 0 then " succeeded" else " failed")
in
- let make_m = externals_factory#add_item "_Make"
+ let _ = externals_factory#add_item "_Make"
~key:GdkKeysyms._F6
~callback:make_f
in
@@ -2837,7 +2927,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
let av = out_some v.analyzed_view in
av#set_message "No more errors.\n"
in
- let next_error_m =
+ let _ =
externals_factory#add_item "_Next error"
~key:GdkKeysyms._F7
~callback:next_error in
@@ -2857,7 +2947,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
let configuration_menu = factory#add_submenu "_Windows" in
let configuration_factory = new GMenu.factory configuration_menu ~accel_path:"<CoqIde MenuBar>/Windows" ~accel_group
in
- let queries_show_m =
+ let _ =
configuration_factory#add_item
"Show _Query Window"
(*
@@ -2865,14 +2955,14 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
*)
~callback:(Command_windows.command_window ())#window#present
in
- let toolbar_show_m =
+ let _ =
configuration_factory#add_item
"Show/Hide _Toolbar"
~callback:(fun () ->
!current.show_toolbar <- not !current.show_toolbar;
!show_toolbar !current.show_toolbar)
in
- let detach_menu = configuration_factory#add_item
+ let _ = configuration_factory#add_item
"Detach _Script Window"
~callback:
(do_if_not_computing "detach script window" (sync
@@ -2890,7 +2980,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
end
)))
in
- let detach_current_view =
+ let _ =
configuration_factory#add_item
"Detach _View"
~callback:
@@ -3177,7 +3267,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
let tv2 = GText.view ~packing:(sw2#add) () in
tv2#misc#set_name "GoalWindow";
let _ = tv2#set_editable false in
- let tb2 = tv2#buffer 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