summaryrefslogtreecommitdiff
path: root/ide/coqOps.ml
diff options
context:
space:
mode:
Diffstat (limited to 'ide/coqOps.ml')
-rw-r--r--ide/coqOps.ml196
1 files changed, 137 insertions, 59 deletions
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 89f4e513..1563c7ff 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -12,15 +12,19 @@ open Ideutils
open Interface
open Feedback
-type flag = [ `INCOMPLETE | `UNSAFE | `PROCESSING | `ERROR of string ]
-type mem_flag = [ `INCOMPLETE | `UNSAFE | `PROCESSING | `ERROR ]
+let b2c = byte_offset_to_char_offset
+
+type flag = [ `INCOMPLETE | `UNSAFE | `PROCESSING | `ERROR of Loc.t * string | `WARNING of Loc.t * string ]
+type mem_flag = [ `INCOMPLETE | `UNSAFE | `PROCESSING | `ERROR | `WARNING ]
let mem_flag_of_flag : flag -> mem_flag = function
| `ERROR _ -> `ERROR
+ | `WARNING _ -> `WARNING
| (`INCOMPLETE | `UNSAFE | `PROCESSING) as mem_flag -> mem_flag
let str_of_flag = function
| `UNSAFE -> "U"
| `PROCESSING -> "P"
| `ERROR _ -> "E"
+ | `WARNING _ -> "W"
| `INCOMPLETE -> "I"
class type signals =
@@ -44,12 +48,9 @@ module SentenceId : sig
val mk_sentence :
start:GText.mark -> stop:GText.mark -> flag list -> sentence
- val set_flags : sentence -> flag list -> unit
val add_flag : sentence -> flag -> unit
val has_flag : sentence -> mem_flag -> bool
val remove_flag : sentence -> mem_flag -> unit
- val same_sentence : sentence -> sentence -> bool
- val hidden_edit_id : unit -> int
val find_all_tooltips : sentence -> int -> string list
val add_tooltip : sentence -> int -> int -> string -> unit
val set_index : sentence -> int -> unit
@@ -87,18 +88,15 @@ end = struct
index = -1;
changed_sig = new GUtil.signal ();
}
- let hidden_edit_id () = decr id; !id
let changed s =
s.changed_sig#call (s.index, List.map mem_flag_of_flag s.flags)
- let set_flags s f = s.flags <- f; changed s
let add_flag s f = s.flags <- CList.add_set (=) f s.flags; changed s
let has_flag s mf =
List.exists (fun f -> mem_flag_of_flag f = mf) s.flags
let remove_flag s mf =
s.flags <- List.filter (fun f -> mem_flag_of_flag f <> mf) s.flags; changed s
- let same_sentence s1 s2 = s1.edit_id = s2.edit_id
let find_all_tooltips s off =
CList.map_filter (fun (start,stop,t) ->
if start <= off && off <= stop then Some t else None)
@@ -130,8 +128,6 @@ end = struct
end
open SentenceId
-let prefs = Preferences.current
-
let log msg : unit task =
Coq.lift (fun () -> Minilib.log msg)
@@ -142,7 +138,7 @@ object
method tactic_wizard : string list -> unit task
method process_next_phrase : unit task
method process_until_end_or_error : unit task
- method handle_reset_initial : Coq.reset_kind -> unit task
+ method handle_reset_initial : unit task
method raw_coq_query : string -> unit task
method show_goals : unit task
method backtrack_last_phrase : unit task
@@ -160,15 +156,71 @@ object
end
let flags_to_color f =
- let of_col c = `NAME (Tags.string_of_color c) in
if List.mem `PROCESSING f then `NAME "blue"
else if List.mem `ERROR f then `NAME "red"
else if List.mem `UNSAFE f then `NAME "orange"
else if List.mem `INCOMPLETE f then `NAME "gray"
- else of_col (Tags.get_processed_color ())
+ else `NAME Preferences.processed_color#get
+
+let validate s =
+ let open Xml_datatype in
+ let rec validate = function
+ | PCData s -> Glib.Utf8.validate s
+ | Element (_, _, children) -> List.for_all validate children
+ in
+ validate (Richpp.repr s)
module Doc = Document
+let segment_model (doc : sentence Doc.document) : Wg_Segment.model =
+object (self)
+
+ val mutable cbs = []
+
+ val mutable document_length = 0
+
+ method length = document_length
+
+ method changed ~callback = cbs <- callback :: cbs
+
+ method fold : 'a. ('a -> Wg_Segment.color -> 'a) -> 'a -> 'a = fun f accu ->
+ let fold accu _ _ s =
+ let flags = List.map mem_flag_of_flag s.flags in
+ f accu (flags_to_color flags)
+ in
+ Doc.fold_all doc accu fold
+
+ method private on_changed (i, f) =
+ let data = (i, flags_to_color f) in
+ List.iter (fun f -> f (`SET data)) cbs
+
+ method private on_push s ctx =
+ let after = match ctx with
+ | None -> []
+ | Some (l, _) -> l
+ in
+ List.iter (fun s -> set_index s (s.index + 1)) after;
+ set_index s (document_length - List.length after);
+ ignore ((SentenceId.connect s)#changed self#on_changed);
+ document_length <- document_length + 1;
+ List.iter (fun f -> f `INSERT) cbs
+
+ method private on_pop s ctx =
+ let () = match ctx with
+ | None -> ()
+ | Some (l, _) -> List.iter (fun s -> set_index s (s.index - 1)) l
+ in
+ set_index s (-1);
+ document_length <- document_length - 1;
+ List.iter (fun f -> f `REMOVE) cbs
+
+ initializer
+ let _ = (Doc.connect doc)#pushed self#on_push in
+ let _ = (Doc.connect doc)#popped self#on_pop in
+ ()
+
+end
+
class coqops
(_script:Wg_ScriptView.script_view)
(_pv:Wg_ProofView.proof_view)
@@ -201,20 +253,8 @@ object(self)
script#misc#set_has_tooltip true;
ignore(script#misc#connect#query_tooltip ~callback:self#tooltip_callback);
feedback_timer.Ideutils.run ~ms:300 ~callback:self#process_feedback;
- let on_changed (i, f) = segment#add i (flags_to_color f) in
- let on_push s =
- set_index s document_length;
- ignore ((SentenceId.connect s)#changed on_changed);
- document_length <- succ document_length;
- segment#set_length document_length;
- let flags = List.map mem_flag_of_flag s.flags in
- segment#add s.index (flags_to_color flags);
- in
- let on_pop s =
- set_index s (-1);
- document_length <- pred document_length;
- segment#set_length document_length;
- in
+ let md = segment_model document in
+ segment#set_model md;
let on_click id =
let find _ _ s = Int.equal s.index id in
let sentence = Doc.find document find in
@@ -230,8 +270,6 @@ object(self)
script#buffer#place_cursor iter;
ignore (script#scroll_to_iter ~use_align:true ~yalign:0. iter)
in
- let _ = (Doc.connect document)#pushed on_push in
- let _ = (Doc.connect document)#popped on_pop in
let _ = segment#connect#clicked on_click in
()
@@ -301,8 +339,11 @@ object(self)
method private show_goals_aux ?(move_insert=false) () =
Coq.PrintOpt.set_printing_width proof#width;
if move_insert then begin
- buffer#place_cursor ~where:self#get_start_of_input;
- script#recenter_insert;
+ let dest = self#get_start_of_input in
+ if (buffer#get_iter_at_mark `INSERT)#compare dest <= 0 then begin
+ buffer#place_cursor ~where:dest;
+ script#recenter_insert
+ end
end;
Coq.bind (Coq.goals ~logger:messages#push ()) (function
| Fail x -> self#handle_failure_aux ~move_insert x
@@ -322,7 +363,7 @@ object(self)
method raw_coq_query phrase =
let action = log "raw_coq_query starting now" in
let display_error s =
- if not (Glib.Utf8.validate s) then
+ if not (validate s) then
flash_info "This error is so nasty that I can't even display it."
else messages#add s;
in
@@ -331,7 +372,7 @@ object(self)
let next = function
| Fail (_, _, err) -> display_error err; Coq.return ()
| Good msg ->
- messages#add msg; Coq.return ()
+ messages#add_string msg; Coq.return ()
in
Coq.bind (Coq.seq action query) next
@@ -362,8 +403,8 @@ object(self)
let start_sentence, stop_sentence, phrase = self#get_sentence sentence in
let pre_chars, post_chars =
if Loc.is_ghost loc then 0, String.length phrase else Loc.unloc loc in
- let pre = Ideutils.glib_utf8_pos_to_offset phrase ~off:pre_chars in
- let post = Ideutils.glib_utf8_pos_to_offset phrase ~off:post_chars in
+ let pre = b2c phrase pre_chars in
+ let post = b2c phrase post_chars in
let start = start_sentence#forward_chars pre in
let stop = start_sentence#forward_chars post in
let markup = Glib.Markup.escape_text text in
@@ -406,7 +447,6 @@ object(self)
| Processed, Some (id,sentence) ->
log "Processed" id;
remove_flag sentence `PROCESSING;
- remove_flag sentence `ERROR;
self#mark_as_needed sentence
| ProcessingIn _, Some (id,sentence) ->
log "ProcessingIn" id;
@@ -424,14 +464,25 @@ object(self)
log "GlobRef" id;
self#attach_tooltip sentence loc
(Printf.sprintf "%s %s %s" filepath ident ty)
- | ErrorMsg(loc, msg), Some (id,sentence) ->
+ | Message(Error, loc, msg), Some (id,sentence) ->
+ let loc = Option.default Loc.ghost loc in
+ let msg = Richpp.raw_print msg in
log "ErrorMsg" id;
remove_flag sentence `PROCESSING;
- add_flag sentence (`ERROR msg);
+ add_flag sentence (`ERROR (loc, msg));
self#mark_as_needed sentence;
self#attach_tooltip sentence loc msg;
if not (Loc.is_ghost loc) then
self#position_error_tag_at_sentence sentence (Some (Loc.unloc loc))
+ | Message(Warning, loc, msg), Some (id,sentence) ->
+ let loc = Option.default Loc.ghost loc in
+ let msg = Richpp.raw_print msg in
+ log "WarningMsg" id;
+ add_flag sentence (`WARNING (loc, msg));
+ self#attach_tooltip sentence loc msg;
+ self#position_warning_tag_at_sentence sentence loc
+ | Message((Info|Notice|Debug as lvl), _, msg), _ ->
+ messages#push lvl msg
| InProgress n, _ ->
if n < 0 then processed <- processed + abs n
else to_process <- to_process + n
@@ -466,13 +517,25 @@ object(self)
| None -> ()
| Some (start, stop) ->
buffer#apply_tag Tags.Script.error
- ~start:(iter#forward_chars (byte_offset_to_char_offset phrase start))
- ~stop:(iter#forward_chars (byte_offset_to_char_offset phrase stop))
+ ~start:(iter#forward_chars (b2c phrase start))
+ ~stop:(iter#forward_chars (b2c phrase stop))
method private position_error_tag_at_sentence sentence loc =
let start, _, phrase = self#get_sentence sentence in
self#position_error_tag_at_iter start phrase loc
+ method private position_warning_tag_at_iter iter_start iter_stop phrase loc =
+ if Loc.is_ghost loc then
+ buffer#apply_tag Tags.Script.warning ~start:iter_start ~stop:iter_stop
+ else
+ buffer#apply_tag Tags.Script.warning
+ ~start:(iter_start#forward_chars (b2c phrase loc.Loc.bp))
+ ~stop:(iter_stop#forward_chars (b2c phrase loc.Loc.ep))
+
+ method private position_warning_tag_at_sentence sentence loc =
+ let start, stop, phrase = self#get_sentence sentence in
+ self#position_warning_tag_at_iter start stop phrase loc
+
method private process_interp_error queue sentence loc msg tip id =
Coq.bind (Coq.return ()) (function () ->
let start, stop, phrase = self#get_sentence sentence in
@@ -483,7 +546,7 @@ object(self)
self#position_error_tag_at_iter start phrase loc;
buffer#place_cursor ~where:stop;
messages#clear;
- messages#push Pp.Error msg;
+ messages#push Feedback.Error msg;
self#show_goals
end else
self#show_goals_aux ~move_insert:true ()
@@ -499,13 +562,19 @@ object(self)
condition returns true; it is fed with the number of phrases read and the
iters enclosing the current sentence. *)
method private fill_command_queue until queue =
+ let topstack =
+ if Doc.focused document then fst (Doc.context document) else [] in
let rec loop n iter =
match Sentence.find buffer iter with
| None -> ()
| Some (start, stop) ->
if until n start stop then begin
()
- end else if stop#backward_char#has_tag Tags.Script.processed then begin
+ end else if
+ List.exists (fun (_, s) ->
+ start#equal (buffer#get_iter_at_mark s.start) &&
+ stop#equal (buffer#get_iter_at_mark s.stop)) topstack
+ then begin
Queue.push (`Skip (start, stop)) queue;
loop n stop
end else begin
@@ -559,7 +628,8 @@ object(self)
if Queue.is_empty queue then conclude topstack else
match Queue.pop queue, topstack with
| `Skip(start,stop), [] ->
- logger Pp.Error "You must close the proof with Qed or Admitted";
+
+ logger Feedback.Error (Richpp.richpp_of_string "You must close the proof with Qed or Admitted");
self#discard_command_queue queue;
conclude []
| `Skip(start,stop), (_,s) :: topstack ->
@@ -575,7 +645,7 @@ object(self)
let handle_answer = function
| Good (id, (Util.Inl (* NewTip *) (), msg)) ->
Doc.assign_tip_id document id;
- logger Pp.Notice msg;
+ logger Feedback.Notice (Richpp.richpp_of_string msg);
self#commit_queue_transaction sentence;
loop id []
| Good (id, (Util.Inr (* Unfocus *) tip, msg)) ->
@@ -583,7 +653,7 @@ object(self)
let topstack, _ = Doc.context document in
self#exit_focus;
self#cleanup (Doc.cut_at document tip);
- logger Pp.Notice msg;
+ logger Feedback.Notice (Richpp.richpp_of_string msg);
self#mark_as_needed sentence;
if Queue.is_empty queue then loop tip []
else loop tip (List.rev topstack)
@@ -602,7 +672,7 @@ object(self)
let next = function
| Good _ ->
messages#clear;
- messages#push Pp.Info "All proof terms checked by the kernel";
+ messages#push Feedback.Info (Richpp.richpp_of_string "All proof terms checked by the kernel");
Coq.return ()
| Fail x -> self#handle_failure x in
Coq.bind (Coq.status ~logger:messages#push true) next
@@ -618,7 +688,15 @@ object(self)
method get_errors =
let extract_error s =
match List.find (function `ERROR _ -> true | _ -> false) s.flags with
- | `ERROR msg -> (buffer#get_iter_at_mark s.start)#line + 1, msg
+ | `ERROR (loc, msg) ->
+ let iter =
+ if Loc.is_ghost loc then
+ buffer#get_iter_at_mark s.start
+ else
+ let (iter, _, phrase) = self#get_sentence s in
+ let (start, _) = Loc.unloc loc in
+ iter#forward_chars (b2c phrase start) in
+ iter#line + 1, msg
| _ -> assert false in
List.rev
(Doc.fold_all document [] (fun acc _ _ s ->
@@ -630,7 +708,7 @@ object(self)
method private process_until_iter iter =
let until _ start stop =
- if prefs.Preferences.stop_before then stop#compare iter > 0
+ if Preferences.stop_before#get then stop#compare iter > 0
else start#compare iter >= 0
in
self#process_until until false
@@ -696,8 +774,8 @@ object(self)
self#cleanup (Doc.cut_at document to_id);
conclusion ()
| Fail (safe_id, loc, msg) ->
- if loc <> None then messages#push Pp.Error "Fixme LOC";
- messages#push Pp.Error msg;
+(* if loc <> None then messages#push Feedback.Error (Richpp.richpp_of_string "Fixme LOC"); *)
+ messages#push Feedback.Error msg;
if Stateid.equal safe_id Stateid.dummy then self#show_goals
else undo safe_id
(Doc.focused document && Doc.is_in_focus document safe_id))
@@ -714,8 +792,7 @@ object(self)
method private handle_failure_aux
?(move_insert=false) (safe_id, (loc : (int * int) option), msg)
=
- messages#clear;
- messages#push Pp.Error msg;
+ messages#push Feedback.Error msg;
ignore(self#process_feedback ());
if Stateid.equal safe_id Stateid.dummy then Coq.lift (fun () -> ())
else
@@ -772,7 +849,7 @@ object(self)
self#show_goals
in
let display_error (loc, s) =
- if not (Glib.Utf8.validate s) then
+ if not (validate s) then
flash_info "This error is so nasty that I can't even display it."
else messages#add s
in
@@ -782,10 +859,10 @@ object(self)
let next = function
| Fail (_, l, str) -> (* FIXME: check *)
display_error (l, str);
- messages#add ("Unsuccessfully tried: "^phrase);
+ messages#add (Richpp.richpp_of_string ("Unsuccessfully tried: "^phrase));
more
| Good msg ->
- messages#add msg;
+ messages#add_string msg;
stop Tags.Script.processed
in
Coq.bind (Coq.seq action query) next
@@ -797,10 +874,8 @@ object(self)
in
loop l
- method handle_reset_initial why =
+ method handle_reset_initial =
let action () =
- if why = Coq.Unexpected then warning "Coqtop died badly. Resetting."
- else
(* clear the stack *)
if Doc.focused document then Doc.unfocus document;
while not (Doc.is_empty document) do
@@ -829,7 +904,10 @@ object(self)
method initialize =
let get_initial_state =
let next = function
- | Fail _ -> messages#set ("Couln't initialize Coq"); Coq.return ()
+ | Fail (_, _, message) ->
+ let message = "Couldn't initialize coqtop\n\n" ^ (Richpp.raw_print message) in
+ let popup = GWindow.message_dialog ~buttons:GWindow.Buttons.ok ~message_type:`ERROR ~message () in
+ ignore (popup#run ()); exit 1
| Good id -> initial_state <- id; Coq.return () in
Coq.bind (Coq.init (get_filename ())) next in
Coq.seq get_initial_state Coq.PrintOpt.enforce
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-06 06:12:16 +0000