aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--ide/coq.ml2
-rw-r--r--ide/coqide.ml211
-rw-r--r--ide/find_phrase.mll24
-rw-r--r--ide/highlight.mll50
-rw-r--r--ide/ideutils.ml9
5 files changed, 203 insertions, 93 deletions
diff --git a/ide/coq.ml b/ide/coq.ml
index 8e74b6d09..3a6b729ce 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -75,7 +75,7 @@ let print_toplevel_error exc =
let (loc,exc) =
match exc with
| Stdpp.Exc_located (loc, ie) -> (Some loc),ie
- | Error_in_file (s, (fname, loc), ie) -> assert false
+ | Error_in_file (s, (fname, loc), ie) -> None, ie
| _ -> dloc,exc
in
match exc with
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 136f4dc91..35eb79360 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -115,6 +115,9 @@ object('self)
val proof_buffer : GText.buffer
val proof_view : GText.view
val mutable is_active : bool
+ val mutable read_only : bool
+ method read_only : bool
+ method set_read_only : bool -> unit
method is_active : bool
method activate : unit -> unit
method active_keypress_handler : GdkEvent.Key.t -> bool
@@ -133,7 +136,7 @@ object('self)
method insert_message : string -> unit
method insert_this_phrase_on_success :
bool -> bool -> bool -> string -> string -> bool
- method process_next_phrase : bool -> bool
+ method process_next_phrase : bool -> bool -> bool
method process_until_insert_or_error : unit
method process_until_iter_or_error : GText.iter -> unit
method process_until_end_or_error : unit
@@ -232,6 +235,22 @@ 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
+let coq_computing = ref false
+let id () = ()
+let do_if_not_computing f x =
+ if not !coq_computing then
+ begin
+ try
+ coq_computing := true;
+ f x;
+ coq_computing := false;
+ with e ->
+ coq_computing := false;
+ raise e
+ end
+ else
+ id x
+
(* push a new Coq phrase *)
let update_on_end_of_proof () =
@@ -339,6 +358,9 @@ object(self)
val proof_buffer = proof_view_#buffer
val message_buffer = message_view_#buffer
val mutable is_active = false
+ val mutable read_only = false
+ method set_read_only b = read_only<-b
+ method read_only = read_only
method is_active = is_active
method insert_message s =
message_buffer#insert s;
@@ -351,7 +373,6 @@ 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_insert = get_insert input_buffer
@@ -450,24 +471,17 @@ object(self)
)
r;
ignore (proof_view#scroll_to_mark my_mark)
-
+
method send_to_coq phrase show_output show_error localize =
- try
- !push_info "Coq is computing";
- (out_some !status)#misc#draw None;
- input_view#set_editable false;
+ try
+ prerr_endline "Send_to_coq starting now";
can_break ();
let r = Some (Coq.interp phrase) in
cant_break ();
- input_view#set_editable true;
- !pop_info ();
- (out_some !status)#misc#draw None;
let msg = read_stdout () in
self#insert_message (if show_output then msg else "");
r
with e ->
- input_view#set_editable true;
- !pop_info ();
(if show_error then
let (s,loc) = Coq.process_exn e in
assert (Glib.Utf8.validate s);
@@ -489,6 +503,7 @@ object(self)
));
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 =
@@ -502,6 +517,7 @@ object(self)
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
@@ -516,24 +532,41 @@ object(self)
raise (Stop !i)
done;
count
- with Stop x -> x
+ with Stop x ->
+ x
in
try
- Find_phrase.length := 0;
trash_bytes := "";
- let phrase = Find_phrase.next_phrase (Lexing.from_function lexbuf_function) in
+ let phrase = Find_phrase.get (Lexing.from_function lexbuf_function)
+ in
end_iter#nocopy#set_offset (start#offset + !Find_phrase.length);
Some (start,end_iter)
with _ -> None
- method process_next_phrase display_goals =
+ method process_next_phrase display_goals do_highlight =
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 -> false
+ with None ->
+ if do_highlight then begin
+ input_view#set_editable true;
+ !pop_info ();
+ end; false
| Some(start,stop) ->
+ prerr_endline "process_next_phrase : to_process highlight";
let b = input_buffer in
+ if do_highlight then begin
+ input_buffer#apply_tag_by_name ~start ~stop "to_process";
+ process_pending ()
+ end;
+ prerr_endline "process_next_phrase : getting phrase";
let phrase = start#get_slice ~stop in
- match self#send_to_coq phrase true true true with
+ let r =
+ match self#send_to_coq phrase true true true with
| Some ast ->
begin
b#move_mark ~where:stop (`NAME "start_of_input");
@@ -549,9 +582,16 @@ object(self)
if display_goals then
(try self#show_goals with e ->
prerr_endline (Printexc.to_string e);());
- true;
+ true
end
| None -> false
+ in
+ if do_highlight then begin
+ b#remove_tag_by_name ~start ~stop "to_process" ;
+ input_view#set_editable true;
+ !pop_info ();
+ end;
+ r
method insert_this_phrase_on_success show_output show_msg localize coqphrase insertphrase =
match self#send_to_coq coqphrase show_output show_msg localize with
@@ -602,18 +642,25 @@ object(self)
~start
~stop
"to_process";
- while ((stop#compare self#get_start_of_input>=0) && self#process_next_phrase false)
+ input_view#set_editable false;
+ !flash_info "Coq is computing";
+ process_pending ();
+ while ((stop#compare self#get_start_of_input>=0)
+ && self#process_next_phrase false false)
do () done;
(try self#show_goals with _ -> ());
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
+ method process_until_end_or_error =
+ self#process_until_iter_or_error input_buffer#end_iter
method process_until_insert_or_error =
let stop = self#get_insert in
self#process_until_iter_or_error stop
- method reset_initial =
+ method reset_initial =
Stack.iter
(function inf ->
let start = input_buffer#get_iter_at_mark inf.start in
@@ -630,7 +677,7 @@ object(self)
(* backtrack Coq to the phrase preceding iterator [i] *)
- method backtrack_to i =
+ method backtrack_to i =
(* re-synchronize Coq to the current state of the stack *)
let rec synchro () =
if is_empty () then
@@ -679,7 +726,8 @@ object(self)
self#clear_message
end
- method backtrack_to_insert = self#backtrack_to self#get_insert
+ method backtrack_to_insert =
+ self#backtrack_to self#get_insert
method undo_last_step =
try
@@ -729,34 +777,35 @@ object(self)
self#insert_this_phrase_on_success true false false cp ip) l)
method active_keypress_handler k =
- match GdkEvent.Key.state k 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
- input_buffer#place_cursor i;
- self#process_until_insert_or_error
- end);
- true
- | l when List.mem `CONTROL l ->
- let k = GdkEvent.Key.keyval k in
- if GdkKeysyms._c=k
- then break ();
- false
- | l -> false
+ if !coq_computing then true else
+ match GdkEvent.Key.state k 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
+ input_buffer#place_cursor i;
+ self#process_until_insert_or_error
+ end);
+ true
+ | l when List.mem `CONTROL l ->
+ let k = GdkEvent.Key.keyval k in
+ if GdkKeysyms._c=k
+ then break ();
+ false
+ | l -> false
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 -> false
-
+ 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 -> false
+
val mutable deact_id = None
val mutable act_id = None
@@ -804,7 +853,7 @@ object(self)
end
with Found ->
begin
- ignore (self#process_next_phrase true)
+ ignore (self#process_next_phrase true true)
end;
end;
last_index <- not last_index;)
@@ -821,6 +870,11 @@ object(self)
(message_view#scroll_to_mark
~within_margin:0.49
`INSERT)));
+ ignore (input_buffer#connect#insert_text
+ ~callback:(fun it s ->
+ if String.length s > 1 then
+ input_buffer#place_cursor it));
+
ignore (input_buffer#connect#modified_changed
~callback:(fun () ->
if input_buffer#modified then
@@ -833,11 +887,24 @@ object(self)
));
ignore (input_buffer#connect#changed
~callback:(fun () ->
+ 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:input_buffer#end_iter
+ ~stop
"error";
- Highlight.highlight_current_line input_buffer));
+ input_buffer#remove_tag_by_name
+ ~start:self#get_start_of_input
+ ~stop
+ "processed";
+ Highlight.highlight_around_current_line
+ input_buffer
+ )
+ );
ignore (input_buffer#add_selection_clipboard (cb()))
end
@@ -858,7 +925,7 @@ let create_input_tab filename =
let tv1 = GText.view ~buffer:b ~packing:(sw1#add) () in
tv1#misc#set_name "ScriptWindow";
let _ = tv1#set_editable true in
- let _ = tv1#set_wrap_mode `CHAR 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));
@@ -933,14 +1000,15 @@ let main () =
input_buffer#set_modified false
with e -> !flash_info "Load failed"
in
- ignore (load_m#connect#activate load_f);
+ ignore (load_m#connect#activate (do_if_not_computing load_f));
(* File/Save Menu *)
let save_m = file_factory#add_item "_Save" ~key:GdkKeysyms._S in
let save_f () =
let current = get_current_view () in
- try (match current.filename with
- | None ->
+ try
+ (match current.filename with
+ | None ->
begin match GToolbox.select_file ~title:"Save file" ()
with
| None -> ()
@@ -995,6 +1063,7 @@ let main () =
(* File/Save All Menu *)
let saveall_m = file_factory#add_item "Sa_ve All" in
let saveall_f () =
+
Vector.iter
(fun {view = view ; filename = filename} ->
match filename with
@@ -1113,22 +1182,29 @@ let main () =
(get_current_view()).view#as_view
GtkText.View.Signals.copy_clipboard));
ignore(edit_f#add_item "Cut" ~key:GdkKeysyms._X ~callback:
+ (do_if_not_computing
(fun () -> GtkSignal.emit_unit
(get_current_view()).view#as_view
- GtkText.View.Signals.cut_clipboard));
+ GtkText.View.Signals.cut_clipboard)));
ignore(edit_f#add_item "Paste" ~key:GdkKeysyms._V ~callback:
- (fun () -> GtkSignal.emit_unit
- (get_current_view()).view#as_view GtkText.View.Signals.paste_clipboard));
+ (fun () ->
+ try GtkSignal.emit_unit
+ (get_current_view()).view#as_view
+ GtkText.View.Signals.paste_clipboard
+ with _ -> prerr_endline "EMIT PASTE FAILED"));
ignore (edit_f#add_separator ());
let read_only_i = edit_f#add_check_item "Read only" ~active:false
~callback:(fun b ->
- (get_current_view()).view#set_editable
- (not b))
+ let v = get_current_view () in
+ v.view#set_editable (not b);
+ (out_some v.analyzed_view)#set_read_only b
+ )
in
to_do_on_page_switch :=
(fun i ->
- let v = (get_input_view i).view in
- read_only_i#set_active (not v#editable)
+ prerr_endline ("Switching to tab "^(string_of_int i));
+ let v = out_some (get_input_view i).analyzed_view in
+ read_only_i#set_active v#read_only
)::!to_do_on_page_switch;
(* Navigation Menu *)
@@ -1142,9 +1218,11 @@ let main () =
else
activate_input (notebook ())#current_page
in
+ let do_or_activate f = do_if_not_computing (do_or_activate f) in
ignore (navigation_factory#add_item "Forward"
~key:GdkKeysyms._Down
- ~callback:(do_or_activate (fun a -> a#process_next_phrase true)));
+ ~callback:(do_or_activate (fun a ->
+ a#process_next_phrase true true)));
ignore (navigation_factory#add_item "Backward"
~key:GdkKeysyms._Up
~callback:(do_or_activate (fun a -> a#undo_last_step)));
@@ -1173,6 +1251,7 @@ let main () =
let analyzed_view = out_some 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 f) in
ignore (tactics_factory#add_item "Auto"
~key:GdkKeysyms._a
~callback:(do_if_active (fun a -> a#insert_command "Progress Auto.\n" "Auto.\n"))
@@ -1443,7 +1522,7 @@ let main () =
w#show ();
message_view := Some tv3;
proof_view := Some tv2;
- let view = create_input_tab "New File" in
+ let view = create_input_tab "*Unamed Buffer*" in
let index = add_input_view {view = view;
analyzed_view = None;
filename = None}
diff --git a/ide/find_phrase.mll b/ide/find_phrase.mll
index 3c73d8f67..8a428710a 100644
--- a/ide/find_phrase.mll
+++ b/ide/find_phrase.mll
@@ -1,18 +1,23 @@
{
exception Lex_error of string
let length = ref 0
+ let buff = Buffer.create 513
}
rule next_phrase = parse
| "(*" { incr length; incr length;
skip_comment lexbuf;
next_phrase lexbuf}
- | '.'[' ''\n''\t''\r'] {incr length; incr length; Lexing.lexeme lexbuf}
+ | '.'[' ''\n''\t''\r'] {
+ length := !length + 2;
+ Buffer.add_string buff (Lexing.lexeme lexbuf);
+ Buffer.contents buff}
| _
{
- let c = Lexing.lexeme lexbuf in
- if Ideutils.is_char_start c.[0] then incr length;
- c^(next_phrase lexbuf)
+ let c = Lexing.lexeme_char lexbuf 0 in
+ if Ideutils.is_char_start c then incr length;
+ Buffer.add_char buff c ;
+ next_phrase lexbuf
}
| eof { raise (Lex_error "no phrase") }
and skip_comment = parse
@@ -20,7 +25,16 @@ and skip_comment = parse
| "(*" {incr length; incr length;
skip_comment lexbuf;
skip_comment lexbuf}
- | _ { if Ideutils.is_char_start (Lexing.lexeme lexbuf).[0] then incr length; skip_comment lexbuf}
+ | _ { if Ideutils.is_char_start (Lexing.lexeme_char lexbuf 0) then
+ incr length;
+ skip_comment lexbuf}
| eof { raise (Lex_error "No closing *)") }
+{
+ let get lb =
+ Buffer.reset buff;
+ length := 0;
+ next_phrase lb
+
+}
diff --git a/ide/highlight.mll b/ide/highlight.mll
index e58654714..5e624fdf2 100644
--- a/ide/highlight.mll
+++ b/ide/highlight.mll
@@ -78,28 +78,42 @@ and comment = parse
open Ideutils
let highlight_slice (input_buffer:GText.buffer) (start:GText.iter) stop =
- let offset = start#offset in
- let s = start#get_slice ~stop in
- let convert_pos = byte_offset_to_char_offset s in
- let lb = Lexing.from_string s in
- try
- while true do
- process_pending ();
- let b,e,o=next_order lb in
- let b,e = convert_pos b,convert_pos e in
- let start = input_buffer#get_iter_at_char (offset + b) in
- let stop = input_buffer#get_iter_at_char (offset + e) in
+ try begin
+ let offset = start#offset in
+ let s = start#get_slice ~stop in
+ let convert_pos = byte_offset_to_char_offset s in
+ let lb = Lexing.from_string s in
+ try
+ while true do
+ process_pending ();
+ let b,e,o=next_order lb in
+ let b,e = convert_pos b,convert_pos e in
+ let start = input_buffer#get_iter_at_char (offset + b) in
+ let stop = input_buffer#get_iter_at_char (offset + e) in
input_buffer#apply_tag_by_name ~start ~stop o
- done
- with End_of_file -> ()
- | _ -> ()
-
+ done
+ with End_of_file -> ()
+ end
+ with _ -> ()
let highlight_current_line input_buffer =
- let i = get_insert input_buffer in
- highlight_slice input_buffer (i#set_line_offset 0) i
+ try
+ let i = get_insert input_buffer in
+ highlight_slice input_buffer (i#set_line_offset 0) i
+ with _ -> ()
+
+ let highlight_around_current_line input_buffer =
+ try
+ let i = get_insert input_buffer in
+ highlight_slice input_buffer
+ (i#backward_lines 3)
+ (ignore (i#nocopy#forward_lines 3);i)
+ with _ -> ()
+
let highlight_all input_buffer =
- highlight_slice input_buffer input_buffer#start_iter input_buffer#end_iter
+ try
+ highlight_slice input_buffer input_buffer#start_iter input_buffer#end_iter
+ with _ -> ()
}
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index f0a0b4181..3edd65aac 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -1,6 +1,8 @@
open Preferences
+exception Forbidden
+
let lib_ide = Filename.concat Coq_config.coqlib "ide"
let get_insert input_buffer = input_buffer#get_iter_at_mark `INSERT
@@ -17,15 +19,15 @@ let byte_offset_to_char_offset s byte_offset =
byte_offset - !count_delta
-let process_pending () =
+let process_pending () =
while Glib.Main.pending () do
- ignore (Glib.Main.iteration false)
+ ignore (Glib.Main.iteration false)
done
let debug = ref true
let prerr_endline s =
- if !debug then prerr_endline s else ()
+ if !debug then (prerr_endline s;flush stderr) else ()
let print_id id =
prerr_endline ("GOT sig id :"^(string_of_int (Obj.magic id)))
@@ -77,3 +79,4 @@ let browse_keyword text =
try
let u = url_for_keyword text in browse (current.doc_url ^ u)
with _ -> ()
+
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 13:52:00 +0000