aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.travis.yml6
-rw-r--r--TODO53
-rw-r--r--ide/coqOps.ml49
-rw-r--r--ide/ide_slave.ml11
-rw-r--r--ide/session.ml2
-rw-r--r--ide/wg_Command.ml13
-rw-r--r--ide/wg_Command.mli2
-rw-r--r--plugins/funind/functional_principles_proofs.ml13
-rw-r--r--plugins/funind/functional_principles_proofs.mli2
-rw-r--r--plugins/funind/indfun_common.ml5
-rw-r--r--plugins/funind/indfun_common.mli5
-rw-r--r--plugins/funind/recdef.ml14
-rw-r--r--plugins/funind/recdef.mli2
-rw-r--r--test-suite/bugs/closed/4306.v32
-rw-r--r--vernac/topfmt.ml27
15 files changed, 115 insertions, 121 deletions
diff --git a/.travis.yml b/.travis.yml
index d35b7a8422..72ce17a09f 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -22,6 +22,7 @@ env:
- NJOBS=2
# system is == 4.02.3
- COMPILER="system"
+ - CAMLP5_VER="6.14"
# Main test suites
matrix:
- TEST_TARGET="test-suite" COMPILER="4.02.3+32bit"
@@ -81,6 +82,7 @@ matrix:
- env:
- TEST_TARGET="test-suite"
- COMPILER="4.04.0"
+ - CAMLP5_VER="6.17"
- EXTRA_CONF="-coqide opt -with-doc yes"
- EXTRA_OPAM="lablgtk-extras hevea"
addons:
@@ -106,8 +108,8 @@ matrix:
install:
- opam init -j ${NJOBS} --compiler=${COMPILER} -n -y
- eval $(opam config env)
-- opam config var root
-- opam install -j ${NJOBS} -y camlp5 ocamlfind ${EXTRA_OPAM}
+- opam config list
+- opam install -j ${NJOBS} -y camlp5.${CAMLP5_VER} ocamlfind ${EXTRA_OPAM}
- opam list
script:
diff --git a/TODO b/TODO
deleted file mode 100644
index f24a37f389..0000000000
--- a/TODO
+++ /dev/null
@@ -1,53 +0,0 @@
-Langage:
-
-Distribution:
-
-Environnement:
-
-- Porter SearchIsos
-
-Noyau:
-
-Tactic:
-
-- Que contradiction raisonne a isomorphisme pres de False
-
-Vernac:
-
-- Print / Print Proof en fait identiques ; Print ne devrait pas afficher
- les constantes opaques (devrait afficher qqchose comme <opaque>)
-
-Theories:
-
-- Rendre transparent tous les theoremes prouvant {A}+{B}
-- Faire demarrer PolyList.nth a` l'indice 0
- Renommer l'actuel nth en nth1 ??
-
-Doc:
-
-- Mettre à jour les messages d'erreurs de Discriminate/Simplify_eq/Injection
-- Documenter le filtrage sur les types inductifs avec let-ins (dont la
- compatibilite V6)
-
-- Ajouter let dans les règles du CIC
- -> FAIT, mais reste a documenter le let dans les inductifs
- et les champs manifestes dans les Record
-- revoir le chapitre sur les tactiques utilisateur
-- faut-il mieux spécifier la sémantique de Simpl (??)
-
-- Préciser la clarification syntaxique de IntroPattern
-- preciser que Goal vient en dernier dans une clause pattern list et
- qu'il doit apparaitre si il y a un "in"
-
-- Omega Time debranche mais Omega System et Omega Action remarchent ?
-- Ajout "Replace in" (mais TODO)
-- Syntaxe Conditional tac Rewrite marche, à documenter
-- Documenter Dependent Rewrite et CutRewrite ?
-- Ajouter les motifs sous-termes de ltac
-
-- ajouter doc de GenFixpoint (mais avant: changer syntaxe) (J. Forest ou Pierre C.)
-- mettre à jour la doc de induction (arguments multiples) (Pierre C.)
-- mettre à jour la doc de functional induction/scheme (J. Forest ou Pierre C.)
---> mettre à jour le CHANGES (vers la ligne 72)
-
-
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index eb97755fa6..222b9eed9f 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -366,6 +366,9 @@ object(self)
(* This method is intended to perform stateless commands *)
method raw_coq_query phrase =
+ let sid = try Document.tip document
+ with Document.Empty -> Stateid.initial
+ in
let action = log "raw_coq_query starting now" in
let display_error s =
if not (validate s) then
@@ -373,11 +376,10 @@ object(self)
else messages#add s;
in
let query =
- Coq.query (phrase,Stateid.dummy) in
+ Coq.query (phrase,sid) in
let next = function
| Fail (_, _, err) -> display_error err; Coq.return ()
- | Good msg ->
- messages#add_string msg; Coq.return ()
+ | Good msg -> Coq.return ()
in
Coq.bind (Coq.seq action query) next
@@ -414,12 +416,9 @@ object(self)
buffer#apply_tag Tags.Script.tooltip ~start ~stop;
add_tooltip sentence pre post markup
- method private is_dummy_id id = Stateid.equal id Stateid.dummy
-
method private enqueue_feedback msg =
- (* Minilib.log ("Feedback received: " ^ Xml_printer.to_string_fmt (Xmlprotocol.of_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 =
@@ -433,41 +432,41 @@ object(self)
| _ -> None in
try Some (Doc.find_map document finder)
with Not_found -> None in
- let log_pp s state_id =
+ let log_pp ?id s=
Minilib.log_pp Pp.(seq
- [str "Feedback "; s; str " on ";
- str (Stateid.to_string (Option.default Stateid.dummy state_id))]) in
- let log s state_id = log_pp (Pp.str s) state_id in
+ [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;
+ log ?id "GlobRef";
self#attach_tooltip ~loc sentence
(Printf.sprintf "%s %s %s" filepath ident ty)
| Message(Error, loc, msg), Some (id,sentence) ->
let uloc = Option.default Loc.ghost loc in
- log_pp Pp.(str "ErrorMsg" ++ msg) id;
+ log_pp ?id Pp.(str "ErrorMsg" ++ msg);
remove_flag sentence `PROCESSING;
let rmsg = Pp.string_of_ppcmds msg in
add_flag sentence (`ERROR (uloc, rmsg));
@@ -476,22 +475,24 @@ object(self)
self#position_tag_at_sentence ?loc Tags.Script.error sentence
| Message(Warning, loc, msg), Some (id,sentence) ->
let uloc = Option.default Loc.ghost loc in
- log_pp Pp.(str "WarningMsg" ++ msg) id;
+ log_pp ?id Pp.(str "WarningMsg" ++ msg);
let rmsg = Pp.string_of_ppcmds msg in
add_flag sentence (`WARNING (uloc, rmsg));
self#attach_tooltip sentence ?loc rmsg;
self#position_tag_at_sentence ?loc Tags.Script.warning sentence;
messages#push Warning msg
| Message(lvl, loc, msg), Some (id,sentence) ->
- log_pp Pp.(str "Msg" ++ msg) id;
+ log_pp ?id Pp.(str "Msg" ++ msg);
+ messages#push lvl msg
+ | Message(lvl, loc, msg), None ->
+ log_pp Pp.(str "Msg" ++ msg);
messages#push lvl msg
| 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 ()
@@ -500,7 +501,7 @@ object(self)
match id, Doc.tip document with
| 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
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 4b95e983d6..bf86db08ff 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -63,25 +63,26 @@ let is_known_option cmd = match cmd with
(** Check whether a command is forbidden in the IDE *)
-let ide_cmd_checks (loc,ast) =
+let ide_cmd_checks ~id (loc,ast) =
let user_error s = CErrors.user_err ~loc ~hdr:"CoqIde" (str s) in
+ let warn msg = Feedback.(feedback ~id (Message (Warning, Some loc, strbrk msg))) in
if is_debug ast then
user_error "Debug mode not available in the IDE";
if is_known_option ast then
- Feedback.msg_warning ~loc (strbrk "Set this option from the IDE menu instead");
+ warn "Set this option from the IDE menu instead";
if is_navigation_vernac ast || is_undo ast then
- Feedback.msg_warning ~loc (strbrk "Use IDE navigation instead");
+ warn "Use IDE navigation instead";
if is_query ast then
- Feedback.msg_warning ~loc (strbrk "Query commands should not be inserted in scripts")
+ warn "Query commands should not be inserted in scripts"
(** Interpretation (cf. [Ide_intf.interp]) *)
let add ((s,eid),(sid,verbose)) =
let pa = Pcoq.Gram.parsable (Stream.of_string s) in
let loc_ast = Stm.parse_sentence sid pa in
- ide_cmd_checks loc_ast;
let newid, rc = Stm.add ~ontop:sid verbose loc_ast in
let rc = match rc with `NewTip -> CSig.Inl () | `Unfocus id -> CSig.Inr id in
+ ide_cmd_checks newid loc_ast;
(* TODO: the "" parameter is a leftover of the times the protocol
* used to include stderr/stdout output.
*
diff --git a/ide/session.ml b/ide/session.ml
index fc6340d283..6262820e7b 100644
--- a/ide/session.ml
+++ b/ide/session.ml
@@ -386,12 +386,12 @@ let create file coqtop_args =
let proof = create_proof () in
let messages = create_messages () in
let segment = new Wg_Segment.segment () in
- let command = new Wg_Command.command_window basename coqtop in
let finder = new Wg_Find.finder basename (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 segment coqtop (fun () -> fops#filename) in
+ let command = new Wg_Command.command_window basename coqtop cops in
let errpage = create_errpage script in
let jobpage = create_jobpage coqtop cops in
let _ = set_buffer_handlers (buffer :> GText.buffer) script cops coqtop in
diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml
index 47dad8f196..3fcb7ce49e 100644
--- a/ide/wg_Command.ml
+++ b/ide/wg_Command.ml
@@ -8,7 +8,7 @@
open Preferences
-class command_window name coqtop =
+class command_window name coqtop coqops =
let frame = Wg_Detachable.detachable
~title:(Printf.sprintf "Query pane (%s)" name) () in
let _ = frame#hide in
@@ -26,6 +26,11 @@ object(self)
val notebook = notebook
+ (* We need access to coqops in order to place queries in the proper
+ document stint. This should remove access from this module to the
+ low-level Coq one. *)
+ val coqops = coqops
+
method pack_in (f : GObj.widget -> unit) = f frame#coerce
val mutable new_page : GObj.widget = (GMisc.label ())#coerce
@@ -101,7 +106,10 @@ object(self)
else com ^ " " ^ arg ^" . "
in
let process =
- Coq.bind (Coq.query (phrase,Stateid.dummy)) (function
+ (* We need to adapt this to route_id and redirect to the result buffer below *)
+ coqops#raw_coq_query phrase
+ (*
+ Coq.bind (Coq.query (phrase,sid)) (function
| Interface.Fail (_,l,str) ->
let width = Ideutils.textview_width result in
Ideutils.insert_xml result#buffer (Richpp.richpp_of_pp width str);
@@ -111,6 +119,7 @@ object(self)
result#buffer#insert res;
notebook#set_page ~tab_label:(new_tab_lbl arg) frame#coerce;
Coq.return ())
+ *)
in
result#buffer#set_text ("Result for command " ^ phrase ^ ":\n");
Coq.try_grab coqtop process ignore
diff --git a/ide/wg_Command.mli b/ide/wg_Command.mli
index fa50ba5fdd..341322be1b 100644
--- a/ide/wg_Command.mli
+++ b/ide/wg_Command.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-class command_window : string -> Coq.coqtop ->
+class command_window : string -> Coq.coqtop -> CoqOps.coqops ->
object
method new_query : ?command:string -> ?term:string -> unit -> unit
method pack_in : (GObj.widget -> unit) -> unit
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 48c0f5f04c..8dae17d69e 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -299,7 +299,7 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type =
Can be safely replaced by the next comment for Ocaml >= 3.08.4
*)
let sub = Int.Map.bindings sub in
- List.fold_left (fun end_of_type (i,t) -> lift 1 (substnl [t] (i-1) end_of_type))
+ List.fold_left (fun end_of_type (i,t) -> liftn 1 i (substnl [t] (i-1) end_of_type))
end_of_type_with_pop
sub
in
@@ -1401,8 +1401,8 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
let prove_with_tcc tcc_lemma_constr eqs : tactic =
match !tcc_lemma_constr with
- | None -> anomaly (Pp.str "No tcc proof !!")
- | Some lemma ->
+ | Undefined -> anomaly (Pp.str "No tcc proof !!")
+ | Value lemma ->
fun gls ->
(* let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in *)
(* let ids = hid::pf_ids_of_hyps gls in *)
@@ -1420,7 +1420,7 @@ let prove_with_tcc tcc_lemma_constr eqs : tactic =
Proofview.V82.of_tactic (Eauto.gen_eauto (false,5) [] (Some []))
]
gls
-
+ | Not_needed -> tclIDTAC
let backtrack_eqs_until_hrec hrec eqs : tactic =
fun gls ->
@@ -1599,8 +1599,9 @@ let prove_principle_for_gen
let args_ids = List.map (get_name %> Nameops.out_name) princ_info.args in
let lemma =
match !tcc_lemma_ref with
- | None -> error "No tcc proof !!"
- | Some lemma -> EConstr.of_constr lemma
+ | Undefined -> error "No tcc proof !!"
+ | Value lemma -> EConstr.of_constr lemma
+ | Not_needed -> EConstr.of_constr (Coqlib.build_coq_I ())
in
(* let rec list_diff del_list check_list = *)
(* match del_list with *)
diff --git a/plugins/funind/functional_principles_proofs.mli b/plugins/funind/functional_principles_proofs.mli
index 769d726d70..7ddc84d015 100644
--- a/plugins/funind/functional_principles_proofs.mli
+++ b/plugins/funind/functional_principles_proofs.mli
@@ -9,7 +9,7 @@ val prove_princ_for_struct :
val prove_principle_for_gen :
constant*constant*constant -> (* name of the function, the functional and the fixpoint equation *)
- constr option ref -> (* a pointer to the obligation proofs lemma *)
+ Indfun_common.tcc_lemma_value ref -> (* a pointer to the obligation proofs lemma *)
bool -> (* is that function uses measure *)
int -> (* the number of recursive argument *)
EConstr.types -> (* the type of the recursive argument *)
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 20da12f395..7b0d7d27d7 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -543,3 +543,8 @@ let prodn n env b =
(* compose_prod [xn:Tn;..;x1:T1] b = (x1:T1)..(xn:Tn)b *)
let compose_prod l b = prodn (List.length l) l b
+
+type tcc_lemma_value =
+ | Undefined
+ | Value of Constr.constr
+ | Not_needed
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 5c3e73e9d7..5ef8f05bb7 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -119,3 +119,8 @@ val decompose_lam_n : Evd.evar_map -> int -> EConstr.t ->
(Names.Name.t * EConstr.t) list * EConstr.t
val compose_lam : (Names.Name.t * EConstr.t) list -> EConstr.t -> EConstr.t
val compose_prod : (Names.Name.t * EConstr.t) list -> EConstr.t -> EConstr.t
+
+type tcc_lemma_value =
+ | Undefined
+ | Value of Constr.constr
+ | Not_needed
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 5460d6fb73..26ba5ef40e 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -45,12 +45,6 @@ open Indfun_common
open Sigma.Notations
open Context.Rel.Declaration
-let local_assum (na, t) =
- LocalAssum (na, EConstr.Unsafe.to_constr t)
-
-let local_def (na, b, t) =
- LocalDef (na, EConstr.Unsafe.to_constr b, EConstr.Unsafe.to_constr t)
-
(* Ugly things which should not be here *)
let coq_constant m s =
@@ -1323,7 +1317,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
| _ -> anomaly ~label:"equation_lemma" (Pp.str "not a constant")
in
let lemma = mkConst (Names.Constant.make1 (Lib.make_kn na)) in
- ref_ := Some (EConstr.Unsafe.to_constr lemma);
+ ref_ := Value (EConstr.Unsafe.to_constr lemma);
let lid = ref [] in
let h_num = ref (-1) in
let env = Global.env () in
@@ -1411,7 +1405,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
let com_terminate
tcc_lemma_name
- (tcc_lemma_ref : Constr.t option ref)
+ tcc_lemma_ref
is_mes
fonctional_ref
input_type
@@ -1440,6 +1434,7 @@ let com_terminate
(new_goal_type);
with Failure "empty list of subgoals!" ->
(* a non recursive function declared with measure ! *)
+ tcc_lemma_ref := Not_needed;
defined ()
@@ -1515,7 +1510,6 @@ let (com_eqn : int -> Id.t ->
(* Pp.msgnl (str "eqn finished"); *)
);;
-
let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num eq
generate_induction_principle using_lemmas : unit =
let open Term in
@@ -1561,7 +1555,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
in
let evm = Evd.from_ctx evuctx in
let tcc_lemma_name = add_suffix function_name "_tcc" in
- let tcc_lemma_constr = ref None in
+ let tcc_lemma_constr = ref Undefined in
(* let _ = Pp.msgnl (str "relation := " ++ Printer.pr_lconstr_env env_with_pre_rec_args relation) in *)
let hook _ _ =
let term_ref = Nametab.locate (qualid_of_ident term_id) in
diff --git a/plugins/funind/recdef.mli b/plugins/funind/recdef.mli
index 9c1081b9d2..80f02e01c4 100644
--- a/plugins/funind/recdef.mli
+++ b/plugins/funind/recdef.mli
@@ -13,7 +13,7 @@ bool ->
Constrexpr.constr_expr ->
Constrexpr.constr_expr ->
int -> Constrexpr.constr_expr -> (Term.pconstant ->
- Term.constr option ref ->
+ Indfun_common.tcc_lemma_value ref ->
Term.pconstant ->
Term.pconstant -> int -> EConstr.types -> int -> EConstr.constr -> 'a) -> Constrexpr.constr_expr list -> unit
diff --git a/test-suite/bugs/closed/4306.v b/test-suite/bugs/closed/4306.v
new file mode 100644
index 0000000000..4aef5bb95e
--- /dev/null
+++ b/test-suite/bugs/closed/4306.v
@@ -0,0 +1,32 @@
+Require Import List.
+Require Import Arith.
+Require Import Recdef.
+Require Import Omega.
+
+Function foo (xys : (list nat * list nat)) {measure (fun xys => length (fst xys) + length (snd xys))} : list nat :=
+ match xys with
+ | (nil, _) => snd xys
+ | (_, nil) => fst xys
+ | (x :: xs', y :: ys') => match Compare_dec.nat_compare x y with
+ | Lt => x :: foo (xs', y :: ys')
+ | Eq => x :: foo (xs', ys')
+ | Gt => y :: foo (x :: xs', ys')
+ end
+ end.
+Proof.
+ intros; simpl; omega.
+ intros; simpl; omega.
+ intros; simpl; omega.
+Qed.
+
+Function bar (xys : (list nat * list nat)) {measure (fun xys => length (fst xys) + length (snd xys))} : list nat :=
+ let (xs, ys) := xys in
+ match (xs, ys) with
+ | (nil, _) => ys
+ | (_, nil) => xs
+ | (x :: xs', y :: ys') => match Compare_dec.nat_compare x y with
+ | Lt => x :: foo (xs', ys)
+ | Eq => x :: foo (xs', ys')
+ | Gt => y :: foo (xs, ys')
+ end
+ end. \ No newline at end of file
diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml
index a4acd3f24e..c25dd55fb7 100644
--- a/vernac/topfmt.ml
+++ b/vernac/topfmt.ml
@@ -112,26 +112,23 @@ let msgnl_with ?pre_hdr fmt strm =
pp_with fmt (strm ++ fnl ());
Format.pp_print_flush fmt ()
-(* XXX: This is really painful! *)
module Emacs = struct
(* Special chars for emacs, to detect warnings inside goal output *)
- let emacs_quote_start = String.make 1 (Char.chr 254)
- let emacs_quote_end = String.make 1 (Char.chr 255)
+ let quote_warning_start = "<warning>"
+ let quote_warning_end = "</warning>"
- let emacs_quote_err g =
- hov 0 (str emacs_quote_start ++ g ++ str emacs_quote_end)
+ let quote_info_start = "<infomsg>"
+ let quote_info_end = "</infomsg>"
- let emacs_quote_info_start = "<infomsg>"
- let emacs_quote_info_end = "</infomsg>"
+ let quote_emacs q_start q_end msg =
+ hov 0 (seq [str q_start; brk(0,0); msg; brk(0,0); str q_end])
- let emacs_quote_info g =
- hov 0 (str emacs_quote_info_start++ brk(0,0) ++ g ++ brk(0,0) ++ str emacs_quote_info_end)
+ let quote_warning = quote_emacs quote_warning_start quote_warning_end
+ let quote_info = quote_emacs quote_info_start quote_info_end
end
-open Emacs
-
let dbg_hdr = tag Tag.debug (str "Debug:") ++ spc ()
let info_hdr = mt ()
let warn_hdr = tag Tag.warning (str "Warning:") ++ spc ()
@@ -144,13 +141,13 @@ let make_body quoter info ?pre_hdr s =
(* The empty quoter *)
let noq x = x
(* Generic logger *)
-let gen_logger dbg err ?pre_hdr level msg = match level with
+let gen_logger dbg warn ?pre_hdr level msg = match level with
| Debug -> msgnl_with !std_ft (make_body dbg dbg_hdr ?pre_hdr msg)
| Info -> msgnl_with !std_ft (make_body dbg info_hdr ?pre_hdr msg)
| Notice -> msgnl_with !std_ft (make_body noq info_hdr ?pre_hdr msg)
| Warning -> Flags.if_warn (fun () ->
- msgnl_with !err_ft (make_body err warn_hdr ?pre_hdr msg)) ()
- | Error -> msgnl_with !err_ft (make_body err err_hdr ?pre_hdr msg)
+ msgnl_with !err_ft (make_body warn warn_hdr ?pre_hdr msg)) ()
+ | Error -> msgnl_with !err_ft (make_body noq err_hdr ?pre_hdr msg)
(** Standard loggers *)
@@ -261,7 +258,7 @@ let init_color_output () =
- Warning/Error: emacs_quote_err
- Notice: unquoted
*)
-let emacs_logger = gen_logger emacs_quote_info emacs_quote_err
+let emacs_logger = gen_logger Emacs.quote_info Emacs.quote_warning
(* Output to file, used only in extraction so a candidate for removal *)
let ft_logger old_logger ft ?loc level mesg =
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 08:28:47 +0000