summaryrefslogtreecommitdiff
path: root/ide/coqOps.ml
diff options
context:
space:
mode:
Diffstat (limited to 'ide/coqOps.ml')
-rw-r--r--ide/coqOps.ml272
1 files changed, 123 insertions, 149 deletions
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 1563c7ff..6c3438a4 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -1,9 +1,11 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open Util
@@ -14,7 +16,7 @@ open Feedback
let b2c = byte_offset_to_char_offset
-type flag = [ `INCOMPLETE | `UNSAFE | `PROCESSING | `ERROR of Loc.t * string | `WARNING of Loc.t * string ]
+type flag = [ `INCOMPLETE | `UNSAFE | `PROCESSING | `ERROR of string Loc.located | `WARNING of string Loc.located ]
type mem_flag = [ `INCOMPLETE | `UNSAFE | `PROCESSING | `ERROR | `WARNING ]
let mem_flag_of_flag : flag -> mem_flag = function
| `ERROR _ -> `ERROR
@@ -58,7 +60,7 @@ module SentenceId : sig
val connect : sentence -> signals
val dbg_to_string :
- GText.buffer -> bool -> Stateid.t option -> sentence -> Pp.std_ppcmds
+ GText.buffer -> bool -> Stateid.t option -> sentence -> Pp.t
end = struct
@@ -117,7 +119,7 @@ end = struct
(b#get_iter_at_mark s.start)#offset
(b#get_iter_at_mark s.stop)#offset
(ellipsize
- ((b#get_iter_at_mark s.start)#get_slice (b#get_iter_at_mark s.stop)))
+ ((b#get_iter_at_mark s.start)#get_slice ~stop:(b#get_iter_at_mark s.stop)))
(String.concat "," (List.map str_of_flag s.flags))
(ellipsize
(String.concat ","
@@ -139,7 +141,8 @@ object
method process_next_phrase : unit task
method process_until_end_or_error : unit task
method handle_reset_initial : unit task
- method raw_coq_query : string -> unit task
+ method raw_coq_query :
+ route_id:int -> next:(query_rty value -> unit task) -> string -> unit task
method show_goals : unit task
method backtrack_last_phrase : unit task
method initialize : unit task
@@ -162,14 +165,6 @@ let flags_to_color f =
else if List.mem `INCOMPLETE f then `NAME "gray"
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 =
@@ -201,7 +196,7 @@ object (self)
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);
+ ignore ((SentenceId.connect s)#changed ~callback:self#on_changed);
document_length <- document_length + 1;
List.iter (fun f -> f `INSERT) cbs
@@ -215,8 +210,8 @@ object (self)
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
+ let _ = (Doc.connect doc)#pushed ~callback:self#on_push in
+ let _ = (Doc.connect doc)#popped ~callback:self#on_pop in
()
end
@@ -224,7 +219,7 @@ end
class coqops
(_script:Wg_ScriptView.script_view)
(_pv:Wg_ProofView.proof_view)
- (_mv:Wg_MessageView.message_view)
+ (_mv:Wg_RoutedMessageViews.message_views_router)
(_sg:Wg_Segment.segment)
(_ct:Coq.coqtop)
get_filename =
@@ -267,15 +262,15 @@ object(self)
else iter
in
let iter = sentence_start iter in
- script#buffer#place_cursor iter;
+ script#buffer#place_cursor ~where:iter;
ignore (script#scroll_to_iter ~use_align:true ~yalign:0. iter)
in
- let _ = segment#connect#clicked on_click in
+ let _ = segment#connect#clicked ~callback:on_click in
()
method private tooltip_callback ~x ~y ~kbd tooltip =
- let x, y = script#window_to_buffer_coords `WIDGET x y in
- let iter = script#get_iter_at_location x y in
+ let x, y = script#window_to_buffer_coords ~tag:`WIDGET ~x ~y in
+ let iter = script#get_iter_at_location ~x ~y in
if iter#has_tag Tags.Script.tooltip then begin
let s =
let rec aux iter =
@@ -305,7 +300,7 @@ object(self)
method private print_stack =
Minilib.log "document:";
- Minilib.log (Pp.string_of_ppcmds (Doc.print document (dbg_to_string buffer)))
+ Minilib.log_pp (Doc.print document (dbg_to_string buffer))
method private enter_focus start stop =
let at id id' _ = Stateid.equal id' id in
@@ -337,7 +332,6 @@ object(self)
buffer#get_iter_at_mark `INSERT
method private show_goals_aux ?(move_insert=false) () =
- Coq.PrintOpt.set_printing_width proof#width;
if move_insert then begin
let dest = self#get_start_of_input in
if (buffer#get_iter_at_mark `INSERT)#compare dest <= 0 then begin
@@ -345,7 +339,7 @@ object(self)
script#recenter_insert
end
end;
- Coq.bind (Coq.goals ~logger:messages#push ()) (function
+ Coq.bind (Coq.goals ()) (function
| Fail x -> self#handle_failure_aux ~move_insert x
| Good goals ->
Coq.bind (Coq.evars ()) (function
@@ -353,32 +347,28 @@ object(self)
| Good evs ->
proof#set_goals goals;
proof#set_evars evs;
- proof#refresh ();
+ proof#refresh ~force:true;
Coq.return ()
)
)
method show_goals = self#show_goals_aux ()
(* This method is intended to perform stateless commands *)
- method raw_coq_query phrase =
- let action = log "raw_coq_query starting now" in
- let display_error s =
- if not (validate s) then
- flash_info "This error is so nasty that I can't even display it."
- else messages#add s;
- in
- let query =
- Coq.query ~logger:messages#push (phrase,Stateid.dummy) in
- let next = function
- | Fail (_, _, err) -> display_error err; Coq.return ()
- | Good msg ->
- messages#add_string msg; Coq.return ()
+ method raw_coq_query ~route_id ~next phrase : unit Coq.task =
+ let sid = try Document.tip document
+ with Document.Empty -> Stateid.initial
in
+ let action = log "raw_coq_query starting now" in
+ let query = Coq.query (route_id,(phrase,sid)) in
Coq.bind (Coq.seq action query) next
+ method private still_valid { edit_id = id } =
+ try ignore(Doc.find_id document (fun _ { edit_id = id1 } -> id = id1)); true
+ with Not_found -> false
+
method private mark_as_needed sentence =
- Minilib.log("Marking " ^
- Pp.string_of_ppcmds (dbg_to_string buffer false None sentence));
+ if self#still_valid sentence then begin
+ Minilib.log_pp Pp.(str "Marking " ++ dbg_to_string buffer false None sentence);
let start = buffer#get_iter_at_mark sentence.start in
let stop = buffer#get_iter_at_mark sentence.stop in
let to_process = Tags.Script.to_process in
@@ -398,11 +388,11 @@ object(self)
in
List.iter (fun t -> buffer#remove_tag t ~start ~stop) all_tags;
List.iter (fun t -> buffer#apply_tag t ~start ~stop) tags
+ end
- method private attach_tooltip sentence loc text =
+ method private attach_tooltip ?loc sentence text =
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_chars, post_chars = Option.cata Loc.unloc (0, String.length phrase) loc in
let pre = b2c phrase pre_chars in
let post = b2c phrase post_chars in
let start = start_sentence#forward_chars pre in
@@ -411,95 +401,93 @@ object(self)
buffer#apply_tag Tags.Script.tooltip ~start ~stop;
add_tooltip sentence pre post markup
- method private is_dummy_id id =
- match id with
- | Edit 0 -> true
- | State id when Stateid.equal id Stateid.dummy -> true
- | _ -> false
-
method private enqueue_feedback msg =
- let id = msg.id in
- if self#is_dummy_id id then () else Queue.add msg feedbacks
-
+ (* Minilib.log ("Feedback received: " ^ Xml_printer.to_string_fmt Xmlprotocol.(of_feedback Ppcmds msg)); *)
+ Queue.add msg feedbacks
+
method private process_feedback () =
let rec eat_feedback n =
if n = 0 then true else
let msg = Queue.pop feedbacks in
- let id = msg.id in
+ let id = msg.span_id in
let sentence =
let finder _ state_id s =
match state_id, id with
- | Some id', State id when Stateid.equal id id' -> Some (state_id, s)
- | _, Edit id when id = s.edit_id -> Some (state_id, s)
+ | Some id', id when Stateid.equal id id' -> Some (state_id, s)
| _ -> None in
try Some (Doc.find_map document finder)
with Not_found -> None in
- let log s state_id =
- Minilib.log ("Feedback " ^ s ^ " on " ^ Stateid.to_string
- (Option.default Stateid.dummy state_id)) in
+ let log_pp ?id s=
+ Minilib.log_pp Pp.(seq
+ [str "Feedback "; s; pr_opt (fun id -> str " on " ++ str (Stateid.to_string id)) id])
+ in
+ let log ?id s = log_pp ?id (Pp.str s) in
begin match msg.contents, sentence with
| AddedAxiom, Some (id,sentence) ->
- log "AddedAxiom" id;
+ log ?id "AddedAxiom";
remove_flag sentence `PROCESSING;
remove_flag sentence `ERROR;
add_flag sentence `UNSAFE;
self#mark_as_needed sentence
| Processed, Some (id,sentence) ->
- log "Processed" id;
+ log ?id "Processed" ;
remove_flag sentence `PROCESSING;
self#mark_as_needed sentence
| ProcessingIn _, Some (id,sentence) ->
- log "ProcessingIn" id;
+ log ?id "ProcessingIn";
add_flag sentence `PROCESSING;
self#mark_as_needed sentence
| Incomplete, Some (id, sentence) ->
- log "Incomplete" id;
+ log ?id "Incomplete";
add_flag sentence `INCOMPLETE;
self#mark_as_needed sentence
| Complete, Some (id, sentence) ->
- log "Complete" id;
+ log ?id "Complete";
remove_flag sentence `INCOMPLETE;
self#mark_as_needed sentence
| GlobRef(loc, filepath, modpath, ident, ty), Some (id,sentence) ->
- log "GlobRef" id;
- self#attach_tooltip sentence loc
+ log ?id "GlobRef";
+ self#attach_tooltip ~loc sentence
(Printf.sprintf "%s %s %s" filepath ident ty)
| 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;
+ log_pp ?id Pp.(str "ErrorMsg " ++ msg);
remove_flag sentence `PROCESSING;
- add_flag sentence (`ERROR (loc, msg));
+ let rmsg = Pp.string_of_ppcmds msg in
+ add_flag sentence (`ERROR (loc, rmsg));
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
+ self#attach_tooltip ?loc sentence rmsg;
+ self#position_tag_at_sentence ?loc Tags.Script.error sentence
+ | Message(Warning, loc, message), Some (id,sentence) ->
+ log_pp ?id Pp.(str "WarningMsg " ++ message);
+ let rmsg = Pp.string_of_ppcmds message in
+ add_flag sentence (`WARNING (loc, rmsg));
+ self#attach_tooltip ?loc sentence rmsg;
+ self#position_tag_at_sentence ?loc Tags.Script.warning sentence;
+ (messages#route msg.route)#push Warning message
+ | Message(lvl, loc, message), Some (id,sentence) ->
+ log_pp ?id Pp.(str "Msg " ++ message);
+ (messages#route msg.route)#push lvl message
+ (* We do nothing here as for BZ#5583 *)
+ | Message(Error, loc, msg), None ->
+ log_pp Pp.(str "Error Msg without a sentence" ++ msg)
+ | Message(lvl, loc, message), None ->
+ log_pp Pp.(str "Msg without a sentence " ++ message);
+ (messages#route msg.route)#push lvl message
| InProgress n, _ ->
if n < 0 then processed <- processed + abs n
else to_process <- to_process + n
| WorkerStatus(id,status), _ ->
- log "WorkerStatus" None;
+ log "WorkerStatus";
slaves_status <- CString.Map.add id status slaves_status
-
| _ ->
if sentence <> None then Minilib.log "Unsupported feedback message"
else if Doc.is_empty document then ()
else
try
match id, Doc.tip document with
- | Edit _, _ -> ()
- | State id1, id2 when Stateid.newer_than id2 id1 -> ()
+ | id1, id2 when Stateid.newer_than id2 id1 -> ()
| _ -> Queue.add msg feedbacks
- with Doc.Empty | Invalid_argument _ -> Queue.add msg feedbacks
+ with Doc.Empty | Invalid_argument _ -> Queue.add msg feedbacks
end;
eat_feedback (n-1)
in
@@ -513,40 +501,30 @@ object(self)
let stop = buffer#get_iter_at_mark sentence.stop in
buffer#move_mark ~where:stop (`NAME "start_of_input");
- method private position_error_tag_at_iter iter phrase = function
- | None -> ()
- | Some (start, stop) ->
- buffer#apply_tag Tags.Script.error
- ~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_tag_at_iter ?loc iter_start iter_stop tag phrase = match loc with
+ | None ->
+ buffer#apply_tag tag ~start:iter_start ~stop:iter_stop
+ | Some loc ->
+ let start, stop = Loc.unloc loc in
+ buffer#apply_tag tag
+ ~start:(iter_start#forward_chars (b2c phrase start))
+ ~stop:(iter_start#forward_chars (b2c phrase stop))
- method private position_warning_tag_at_sentence sentence loc =
+ method private position_tag_at_sentence ?loc tag sentence =
let start, stop, phrase = self#get_sentence sentence in
- self#position_warning_tag_at_iter start stop phrase loc
+ self#position_tag_at_iter ?loc start stop tag phrase
- method private process_interp_error queue sentence loc msg tip id =
+ method private process_interp_error ?loc queue sentence msg tip id =
Coq.bind (Coq.return ()) (function () ->
let start, stop, phrase = self#get_sentence sentence in
buffer#remove_tag Tags.Script.to_process ~start ~stop;
self#discard_command_queue queue;
pop_info ();
if Stateid.equal id tip || Stateid.equal id Stateid.dummy then begin
- self#position_error_tag_at_iter start phrase loc;
+ self#position_tag_at_iter ?loc start stop Tags.Script.error phrase;
buffer#place_cursor ~where:stop;
- messages#clear;
- messages#push Feedback.Error msg;
+ messages#default_route#clear;
+ messages#default_route#push Feedback.Error msg;
self#show_goals
end else
self#show_goals_aux ~move_insert:true ()
@@ -604,12 +582,12 @@ object(self)
(** Compute the phrases until [until] returns [true]. *)
method private process_until ?move_insert until verbose =
- let logger lvl msg = if verbose then messages#push lvl msg in
+ let logger lvl msg = if verbose then messages#default_route#push lvl msg in
let fill_queue = Coq.lift (fun () ->
let queue = Queue.create () in
(* Lock everything and fill the waiting queue *)
push_info "Coq is computing";
- messages#clear;
+ messages#default_route#clear;
script#set_editable false;
self#fill_command_queue until queue;
(* Now unlock and process asynchronously. Since [until]
@@ -628,10 +606,9 @@ object(self)
if Queue.is_empty queue then conclude topstack else
match Queue.pop queue, topstack with
| `Skip(start,stop), [] ->
-
- logger Feedback.Error (Richpp.richpp_of_string "You must close the proof with Qed or Admitted");
+ logger Feedback.Error (Pp.str "You must close the proof with Qed or Admitted");
self#discard_command_queue queue;
- conclude []
+ conclude []
| `Skip(start,stop), (_,s) :: topstack ->
assert(start#equal (buffer#get_iter_at_mark s.start));
assert(stop#equal (buffer#get_iter_at_mark s.stop));
@@ -641,11 +618,11 @@ object(self)
add_flag sentence `PROCESSING;
Doc.push document sentence;
let _, _, phrase = self#get_sentence sentence in
- let coq_query = Coq.add ~logger ((phrase,edit_id),(tip,verbose)) in
+ let coq_query = Coq.add ((phrase,edit_id),(tip,verbose)) in
let handle_answer = function
| Good (id, (Util.Inl (* NewTip *) (), msg)) ->
Doc.assign_tip_id document id;
- logger Feedback.Notice (Richpp.richpp_of_string msg);
+ logger Feedback.Notice (Pp.str msg);
self#commit_queue_transaction sentence;
loop id []
| Good (id, (Util.Inr (* Unfocus *) tip, msg)) ->
@@ -653,13 +630,14 @@ object(self)
let topstack, _ = Doc.context document in
self#exit_focus;
self#cleanup (Doc.cut_at document tip);
- logger Feedback.Notice (Richpp.richpp_of_string msg);
+ logger Feedback.Notice (Pp.str msg);
self#mark_as_needed sentence;
if Queue.is_empty queue then loop tip []
else loop tip (List.rev topstack)
| Fail (id, loc, msg) ->
+ let loc = Option.map Loc.make_loc loc in
let sentence = Doc.pop document in
- self#process_interp_error queue sentence loc msg tip id in
+ self#process_interp_error ?loc queue sentence msg tip id in
Coq.bind coq_query handle_answer
in
let tip =
@@ -667,15 +645,16 @@ object(self)
with Doc.Empty -> initial_state | Invalid_argument _ -> assert false in
loop tip [] in
Coq.bind fill_queue process_queue
-
+
method join_document =
let next = function
| Good _ ->
- messages#clear;
- messages#push Feedback.Info (Richpp.richpp_of_string "All proof terms checked by the kernel");
+ messages#default_route#clear;
+ messages#default_route#push
+ Feedback.Info (Pp.str "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
+ Coq.bind (Coq.status true) next
method stop_worker n =
Coq.bind (Coq.stop_worker n) (fun _ -> Coq.return ())
@@ -689,14 +668,13 @@ object(self)
let extract_error s =
match List.find (function `ERROR _ -> true | _ -> false) s.flags with
| `ERROR (loc, msg) ->
- let iter =
- if Loc.is_ghost loc then
- buffer#get_iter_at_mark s.start
- else
+ let iter = begin match loc with
+ | None -> buffer#get_iter_at_mark s.start
+ | Some loc ->
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
+ iter#forward_chars (b2c phrase start)
+ end in iter#line + 1, msg
| _ -> assert false in
List.rev
(Doc.fold_all document [] (fun acc _ _ s ->
@@ -775,7 +753,7 @@ object(self)
conclusion ()
| Fail (safe_id, loc, msg) ->
(* if loc <> None then messages#push Feedback.Error (Richpp.richpp_of_string "Fixme LOC"); *)
- messages#push Feedback.Error msg;
+ messages#default_route#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))
@@ -792,7 +770,7 @@ object(self)
method private handle_failure_aux
?(move_insert=false) (safe_id, (loc : (int * int) option), msg)
=
- messages#push Feedback.Error msg;
+ messages#default_route#push Feedback.Error msg;
ignore(self#process_feedback ());
if Stateid.equal safe_id Stateid.dummy then Coq.lift (fun () -> ())
else
@@ -804,7 +782,7 @@ object(self)
method handle_failure f = self#handle_failure_aux f
method backtrack_last_phrase =
- messages#clear;
+ messages#default_route#clear;
try
let tgt = Doc.before_tip document in
self#backtrack_to_id tgt
@@ -812,7 +790,7 @@ object(self)
method go_to_insert =
Coq.bind (Coq.return ()) (fun () ->
- messages#clear;
+ messages#default_route#clear;
let point = self#get_insert in
if point#compare self#get_start_of_input >= 0
then self#process_until_iter point
@@ -820,7 +798,7 @@ object(self)
method go_to_mark m =
Coq.bind (Coq.return ()) (fun () ->
- messages#clear;
+ messages#default_route#clear;
let point = buffer#get_iter_at_mark m in
if point#compare self#get_start_of_input >= 0
then Coq.seq (self#process_until_iter point)
@@ -845,25 +823,21 @@ object(self)
~stop:(`MARK (buffer#create_mark stop))
[] in
Doc.push document sentence;
- messages#clear;
+ messages#default_route#clear;
self#show_goals
in
let display_error (loc, s) =
- if not (validate s) then
- flash_info "This error is so nasty that I can't even display it."
- else messages#add s
- in
+ messages#default_route#add (Ideutils.validate s) in
let try_phrase phrase stop more =
let action = log "Sending to coq now" in
- let query = Coq.query (phrase,Stateid.dummy) in
+ let route_id = 0 in
+ let query = Coq.query (route_id,(phrase,Stateid.dummy)) in
let next = function
| Fail (_, l, str) -> (* FIXME: check *)
display_error (l, str);
- messages#add (Richpp.richpp_of_string ("Unsuccessfully tried: "^phrase));
+ messages#default_route#add (Pp.str ("Unsuccessfully tried: "^phrase));
more
- | Good msg ->
- messages#add_string msg;
- stop Tags.Script.processed
+ | Good () -> stop Tags.Script.processed
in
Coq.bind (Coq.seq action query) next
in
@@ -891,7 +865,7 @@ object(self)
buffer#move_mark ~where:buffer#end_iter (`NAME "stop_of_input");
Sentence.tag_all buffer;
(* clear the views *)
- messages#clear;
+ messages#default_route#clear;
proof#clear ();
clear_info ();
processed <- 0;
@@ -905,7 +879,7 @@ object(self)
let get_initial_state =
let next = function
| Fail (_, _, message) ->
- let message = "Couldn't initialize coqtop\n\n" ^ (Richpp.raw_print message) in
+ let message = "Couldn't initialize coqtop\n\n" ^ (Pp.string_of_ppcmds 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-07 14:08:42 +0000