aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide
diff options
context:
space:
mode:
Diffstat (limited to 'ide')
-rw-r--r--ide/coq.ml33
-rw-r--r--ide/coq.mli10
-rw-r--r--ide/coqOps.ml133
-rw-r--r--ide/coqOps.mli1
-rw-r--r--ide/session.ml4
-rw-r--r--ide/wg_Command.ml5
6 files changed, 133 insertions, 53 deletions
diff --git a/ide/coq.ml b/ide/coq.ml
index 121981110..baff54d62 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -275,6 +275,8 @@ type coqtop = {
sup_args : string list;
(* called whenever coqtop dies *)
mutable reset_handler : reset_kind -> unit task;
+ (* called whenever coqtop sends a feedback message *)
+ mutable feedback_handler : Interface.feedback -> unit;
(* actual coqtop process and its status *)
mutable handle : handle;
mutable status : status;
@@ -360,6 +362,11 @@ let handle_intermediate_message logger xml =
let content = message.Interface.message_content in
logger level content
+let handle_feedback feedback_processor xml =
+ let () = Minilib.log "Handling some feedback" in
+ let feedback = Serialize.to_feedback xml in
+ feedback_processor feedback
+
let handle_final_answer handle ccb xml =
let () = Minilib.log "Handling coqtop answer" in
let () = handle.waiting_for <- None in
@@ -370,7 +377,7 @@ type input_state = {
mutable lexerror : int option;
}
-let unsafe_handle_input handle state conds =
+let unsafe_handle_input handle feedback_processor state conds =
let chan = Glib.Io.channel_of_descr handle.cout in
let () = check_errors conds in
let s = io_read_all chan in
@@ -392,6 +399,12 @@ let unsafe_handle_input handle state conds =
let () = state.lexerror <- None in
let () = handle_intermediate_message logger xml in
loop ()
+ else if Serialize.is_feedback xml then
+ let remaining = String.sub s l_end (String.length s - l_end) in
+ let () = state.fragment <- remaining in
+ let () = state.lexerror <- None in
+ let () = handle_feedback feedback_processor xml in
+ loop ()
else
(* We should have finished decoding s *)
let () = if not (is_blank s l_end) then raise AnswerWithoutRequest in
@@ -413,7 +426,7 @@ let unsafe_handle_input handle state conds =
let () = state.lexerror <- Some l_end in
()
-let install_input_watch handle respawner =
+let install_input_watch handle respawner feedback_processor =
let io_chan = Glib.Io.channel_of_descr handle.cout in
let all_conds = [`ERR; `HUP; `IN; `NVAL; `PRI] in (* all except `OUT *)
let state = {
@@ -429,7 +442,7 @@ let install_input_watch handle respawner =
if not handle.alive then false (* coqtop already terminated *)
else
try
- let () = unsafe_handle_input handle state conds in
+ let () = unsafe_handle_input handle feedback_processor state conds in
true
with e ->
let () = Minilib.log ("Coqtop reader failed, resetting: "^print_exception e) in
@@ -472,7 +485,9 @@ let rec respawn_coqtop ?(why=Unexpected) coqtop =
If not, there isn't much we can do ... *)
assert (coqtop.handle.alive = true);
coqtop.status <- New;
- install_input_watch coqtop.handle (fun () -> respawn_coqtop coqtop);
+ install_input_watch coqtop.handle
+ (fun () -> respawn_coqtop coqtop)
+ (fun msg -> coqtop.feedback_handler msg);
ignore (coqtop.reset_handler why coqtop.handle (mkready coqtop))
let spawn_coqtop sup_args =
@@ -481,14 +496,18 @@ let spawn_coqtop sup_args =
handle = spawn_handle sup_args;
sup_args = sup_args;
reset_handler = (fun _ _ k -> k ());
+ feedback_handler = (fun _ -> ());
status = New;
}
in
- install_input_watch ct.handle (fun () -> respawn_coqtop ct);
+ install_input_watch ct.handle
+ (fun () -> respawn_coqtop ct) (fun msg -> ct.feedback_handler msg);
ct
let set_reset_handler coqtop hook = coqtop.reset_handler <- hook
+let set_feedback_handler coqtop hook = coqtop.feedback_handler <- hook
+
let is_computing coqtop = (coqtop.status = Busy)
(* For closing a coqtop, we don't try to send it a Quit call anymore,
@@ -540,8 +559,8 @@ let eval_call ?(logger=default_logger) call handle k =
Minilib.log "End eval_call";
Void
-let interp ?(logger=default_logger) ?(raw=false) ?(verbose=true) s h k =
- eval_call ~logger (Serialize.interp (raw,verbose,s)) h
+let interp ?(logger=default_logger) ?(raw=false) ?(verbose=true) i s h k =
+ eval_call ~logger (Serialize.interp (i,raw,verbose,s)) h
(function
| Interface.Good (Util.Inl v) -> k (Interface.Good v)
| Interface.Good (Util.Inr v) -> k (Interface.Unsafe v)
diff --git a/ide/coq.mli b/ide/coq.mli
index 0210d0b41..84ef466d7 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -63,6 +63,9 @@ val spawn_coqtop : string list -> coqtop
val set_reset_handler : coqtop -> (reset_kind -> unit task) -> unit
(** Register a handler called when a coqtop dies (badly or on purpose) *)
+val set_feedback_handler : coqtop -> (Interface.feedback -> unit) -> unit
+(** Register a handler called when coqtop sends a feedback message *)
+
val init_coqtop : coqtop -> unit task -> unit
(** Finish initializing a freshly spawned coqtop, by running a first task on it.
The task should run its inner continuation at the end. *)
@@ -113,8 +116,11 @@ val try_grab : coqtop -> unit task -> (unit -> unit) -> unit
type 'a query = 'a Interface.value task
(** A type abbreviation for coqtop specific answers *)
-val interp : ?logger:Ideutils.logger -> ?raw:bool -> ?verbose:bool ->
- string -> string query
+val interp :
+ ?logger:Ideutils.logger ->
+ ?raw:bool ->
+ ?verbose:bool ->
+ int -> string -> string query
val rewind : int -> int query
val status : Interface.status query
val goals : Interface.goals option query
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 3e76b94b2..2647f923c 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -11,11 +11,40 @@ open Ideutils
type flag = [ `COMMENT | `UNSAFE ]
-type ide_info = {
- start : GText.mark;
- stop : GText.mark;
- flags : flag list;
-}
+module SentenceId : sig
+
+ type sentence = private {
+ start : GText.mark;
+ stop : GText.mark;
+ mutable flags : flag list;
+ id : int;
+ }
+
+ val mk_sentence :
+ start:GText.mark -> stop:GText.mark -> flag list -> sentence
+ val set_flags : sentence -> flag list -> unit
+
+end = struct
+
+ type sentence = {
+ start : GText.mark;
+ stop : GText.mark;
+ mutable flags : flag list;
+ id : int;
+ }
+
+ let id = ref 0
+ let mk_sentence ~start ~stop flags = decr id; {
+ start = start;
+ stop = stop;
+ flags = flags;
+ id = !id;
+ }
+
+ let set_flags s f = s.flags <- f
+
+end
+open SentenceId
let prefs = Preferences.current
@@ -39,6 +68,7 @@ class coqops
(_script:Wg_ScriptView.script_view)
(_pv:Wg_ProofView.proof_view)
(_mv:Wg_MessageView.message_view)
+ (_ct:Coq.coqtop)
get_filename =
object(self)
val script = _script
@@ -48,6 +78,9 @@ object(self)
val cmd_stack = Stack.create ()
+ initializer
+ Coq.set_feedback_handler _ct self#process_feedback
+
method private get_start_of_input =
buffer#get_iter_at_mark (`NAME "start_of_input")
@@ -81,7 +114,8 @@ object(self)
flash_info "This error is so nasty that I can't even display it."
else messages#add s;
in
- let query = Coq.interp ~logger:messages#push ~raw:true ~verbose:false phrase in
+ let query =
+ Coq.interp ~logger:messages#push ~raw:true ~verbose:false 0 phrase in
let next = function
| Interface.Fail (_, err) -> display_error err; Coq.return ()
| Interface.Good msg | Interface.Unsafe msg ->
@@ -103,12 +137,12 @@ object(self)
let is_comment =
stop#backward_char#has_tag Tags.Script.comment_sentence
in
- let payload = {
- start = `MARK (buffer#create_mark start);
- stop = `MARK (buffer#create_mark stop);
- flags = if is_comment then [`COMMENT] else [];
- } in
- Queue.push payload queue;
+ let sentence =
+ mk_sentence
+ ~start:(`MARK (buffer#create_mark start))
+ ~stop:(`MARK (buffer#create_mark stop))
+ (if is_comment then [`COMMENT] else []) in
+ Queue.push sentence queue;
if not stop#is_end then loop (succ len) stop
in
try loop 0 self#get_start_of_input with Exit -> ()
@@ -123,22 +157,37 @@ object(self)
buffer#delete_mark sentence.stop;
done
- method private commit_queue_transaction queue sentence newflags =
+ method private mark_as_needed sentence =
+ let start = buffer#get_iter_at_mark sentence.start in
+ let stop = buffer#get_iter_at_mark sentence.stop in
+ let tag =
+ if List.mem `UNSAFE sentence.flags then Tags.Script.unjustified
+ else Tags.Script.processed in
+ buffer#apply_tag tag ~start ~stop
+
+ method private process_feedback msg =
+ let id = msg.Interface.edit_id in
+ if id = 0 || Stack.is_empty cmd_stack then () else
+ let sentence =
+ let last_sentence = Stack.top cmd_stack in
+ if last_sentence.id = id then Some last_sentence else None in
+ match msg.Interface.content, sentence with
+ | Interface.AddedAxiom, Some sentence ->
+ set_flags sentence (CList.add_set `UNSAFE sentence.flags);
+ self#mark_as_needed sentence
+ | Interface.Processed, Some sentence -> self#mark_as_needed sentence
+ | _, None -> Minilib.log "Coqide/Coq is really asynchronous now!"
+ (* In this case we shoud look for (exec_)id into cmd_stack *)
+
+ method private commit_queue_transaction sentence =
(* A queued command has been successfully done, we push it to [cmd_stack].
We reget the iters here because Gtk is unable to warranty that they
were not modified meanwhile. Not really necessary but who knows... *)
+ self#mark_as_needed sentence;
let start = buffer#get_iter_at_mark sentence.start in
let stop = buffer#get_iter_at_mark sentence.stop in
- let sentence = { sentence with flags = newflags @ sentence.flags } in
- let tag =
- if List.mem `UNSAFE newflags then Tags.Script.unjustified
- else Tags.Script.processed
- in
buffer#move_mark ~where:stop (`NAME "start_of_input");
- buffer#apply_tag tag ~start ~stop;
- buffer#remove_tag Tags.Script.to_process ~start ~stop;
- ignore (Queue.pop queue);
- Stack.push sentence cmd_stack
+ buffer#remove_tag Tags.Script.to_process ~start ~stop
method private process_error queue phrase loc msg =
Coq.bind (Coq.return ()) (function () ->
@@ -153,6 +202,10 @@ object(self)
buffer#apply_tag Tags.Script.error ~start ~stop;
buffer#place_cursor ~where:start
in
+ let sentence = Stack.pop cmd_stack in
+ let start = buffer#get_iter_at_mark sentence.start in
+ let stop = buffer#get_iter_at_mark sentence.stop in
+ buffer#remove_tag Tags.Script.to_process ~start ~stop;
self#discard_command_queue queue;
pop_info ();
position_error loc;
@@ -183,9 +236,10 @@ object(self)
let () = script#recenter_insert in
self#show_goals
else
- let sentence = Queue.peek queue in
+ let sentence = Queue.pop queue in
+ Stack.push sentence cmd_stack;
if List.mem `COMMENT sentence.flags then
- (self#commit_queue_transaction queue sentence []; loop ())
+ (self#commit_queue_transaction sentence; loop ())
else
(* If the line is not a comment, we interpret it. *)
let phrase =
@@ -193,17 +247,18 @@ object(self)
let stop = buffer#get_iter_at_mark sentence.stop in
start#get_slice ~stop
in
- let commit_and_continue msg flags =
+ let commit_and_continue msg =
push_msg Interface.Notice msg;
- self#commit_queue_transaction queue sentence flags;
+ self#commit_queue_transaction sentence;
loop ()
in
- let query = Coq.interp ~logger:push_msg ~verbose phrase in
+ let query = Coq.interp ~logger:push_msg ~verbose sentence.id phrase in
let next = function
- | Interface.Good msg -> commit_and_continue msg []
- | Interface.Unsafe msg -> commit_and_continue msg [`UNSAFE]
- | Interface.Fail (loc, msg) ->
- self#process_error queue phrase loc msg
+ | Interface.Good msg -> commit_and_continue msg
+ | Interface.Unsafe msg ->
+ set_flags sentence (CList.add_set `UNSAFE sentence.flags);
+ commit_and_continue msg
+ | Interface.Fail (loc, msg) -> self#process_error queue phrase loc msg
in
Coq.bind query next
in
@@ -329,12 +384,12 @@ object(self)
buffer#apply_tag tag ~start ~stop;
if self#get_insert#compare stop <= 0 then
buffer#place_cursor ~where:stop;
- let ide_payload = {
- start = `MARK (buffer#create_mark start);
- stop = `MARK (buffer#create_mark stop);
- flags = [];
- } in
- Stack.push ide_payload cmd_stack;
+ let sentence =
+ mk_sentence
+ ~start:(`MARK (buffer#create_mark start))
+ ~stop:(`MARK (buffer#create_mark stop))
+ [] in
+ Stack.push sentence cmd_stack;
messages#clear;
self#show_goals
in
@@ -345,7 +400,7 @@ object(self)
in
let try_phrase phrase stop more =
let action = log "Sending to coq now" in
- let query = Coq.interp ~verbose:false phrase in
+ let query = Coq.interp ~verbose:false 0 phrase in
let next = function
| Interface.Fail (l, str) ->
display_error (l, str);
@@ -400,7 +455,7 @@ object(self)
| Interface.Good true | Interface.Unsafe true -> Coq.return ()
| Interface.Good false | Interface.Unsafe false ->
let cmd = Printf.sprintf "Add LoadPath \"%s\". " dir in
- let cmd = Coq.interp cmd in
+ let cmd = Coq.interp 0 cmd in
let next = function
| Interface.Fail (l, str) ->
messages#set ("Couln't add loadpath:\n"^str);
diff --git a/ide/coqOps.mli b/ide/coqOps.mli
index 7e47ca23f..48a07f48b 100644
--- a/ide/coqOps.mli
+++ b/ide/coqOps.mli
@@ -25,5 +25,6 @@ class coqops :
Wg_ScriptView.script_view ->
Wg_ProofView.proof_view ->
Wg_MessageView.message_view ->
+ coqtop ->
(unit -> string option) ->
ops
diff --git a/ide/session.ml b/ide/session.ml
index 8eeb3c6f9..4e95fefca 100644
--- a/ide/session.ml
+++ b/ide/session.ml
@@ -155,8 +155,8 @@ let create file coqtop_args =
let finder = new Wg_Find.finder (script :> GText.view) in
let fops = new FileOps.fileops (buffer :> GText.buffer) file reset in
let _ = fops#update_stats in
- let cops = new CoqOps.coqops script proof messages (fun () -> fops#filename)
- in
+ let cops =
+ new CoqOps.coqops script proof messages coqtop (fun () -> fops#filename) in
let _ = Coq.set_reset_handler coqtop cops#handle_reset_initial in
let _ = Coq.init_coqtop coqtop cops#initialize in
{
diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml
index e0a742779..dd8896cba 100644
--- a/ide/wg_Command.ml
+++ b/ide/wg_Command.ml
@@ -111,10 +111,9 @@ object(self)
if String.get com (String.length com - 1) = '.'
then com ^ " " else com ^ " " ^ entry#text ^" . "
in
- let log level message = result#buffer#insert (message^"\n")
- in
+ let log level message = result#buffer#insert (message^"\n") in
let process =
- Coq.bind (Coq.interp ~logger:log ~raw:true phrase) (function
+ Coq.bind (Coq.interp ~logger:log ~raw:true 0 phrase) (function
| Interface.Fail (l,str) ->
result#buffer#insert ("Error while interpreting "^phrase^":\n"^str);
Coq.return ()
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-26 20:45:09 +0000