aboutsummaryrefslogtreecommitdiff
path: root/ide
diff options
context:
space:
mode:
Diffstat (limited to 'ide')
-rw-r--r--ide/coq.ml11
-rw-r--r--ide/coq.mli2
-rw-r--r--ide/coqOps.ml10
-rw-r--r--ide/coqOps.mli2
-rw-r--r--ide/ide_slave.ml6
-rw-r--r--ide/ideutils.ml2
-rw-r--r--ide/texmacspp.ml3
-rw-r--r--ide/xmlprotocol.ml30
-rw-r--r--ide/xmlprotocol.mli4
9 files changed, 37 insertions, 33 deletions
diff --git a/ide/coq.ml b/ide/coq.ml
index 61f002576b..6d44ca59e3 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -227,7 +227,7 @@ type coqtop = {
(* non quoted command-line arguments of coqtop *)
mutable sup_args : string list;
(* called whenever coqtop dies *)
- mutable reset_handler : reset_kind -> unit task;
+ mutable reset_handler : unit task;
(* called whenever coqtop sends a feedback message *)
mutable feedback_handler : Feedback.feedback -> unit;
(* actual coqtop process and its status *)
@@ -298,7 +298,7 @@ let handle_intermediate_message handle level content =
| Feedback.Info -> fun s -> Minilib.log ~level:`INFO (xml_to_string s)
| Feedback.Notice -> fun s -> Minilib.log ~level:`NOTICE (xml_to_string s)
| Feedback.Warning -> fun s -> Minilib.log ~level:`WARNING (xml_to_string s)
- | Feedback.Debug _ -> fun s -> Minilib.log ~level:`DEBUG (xml_to_string s)
+ | Feedback.Debug -> fun s -> Minilib.log ~level:`DEBUG (xml_to_string s)
in
logger level content
@@ -333,7 +333,7 @@ let unsafe_handle_input handle feedback_processor state conds ~read_all =
state.fragment <- String.sub s l_end (String.length s - l_end);
state.lexerror <- None;
match Xmlprotocol.is_message xml with
- | Some (lvl, msg) ->
+ | Some (lvl, _loc, msg) ->
handle_intermediate_message handle lvl msg;
loop ()
| None ->
@@ -421,6 +421,7 @@ let mkready coqtop =
fun () -> coqtop.status <- Ready; Void
let rec respawn_coqtop ?(why=Unexpected) coqtop =
+ if why = Unexpected then warning "Coqtop died badly. Resetting.";
clear_handle coqtop.handle;
ignore_error (fun () ->
coqtop.handle <-
@@ -432,7 +433,7 @@ let rec respawn_coqtop ?(why=Unexpected) coqtop =
If not, there isn't much we can do ... *)
assert (coqtop.handle.alive = true);
coqtop.status <- New;
- ignore (coqtop.reset_handler why coqtop.handle (mkready coqtop))
+ ignore (coqtop.reset_handler coqtop.handle (mkready coqtop))
let spawn_coqtop sup_args =
bind_self_as (fun this -> {
@@ -440,7 +441,7 @@ let spawn_coqtop sup_args =
(fun () -> respawn_coqtop (this ()))
(fun msg -> (this ()).feedback_handler msg);
sup_args = sup_args;
- reset_handler = (fun _ _ k -> k ());
+ reset_handler = (fun _ k -> k ());
feedback_handler = (fun _ -> ());
status = New;
})
diff --git a/ide/coq.mli b/ide/coq.mli
index 7cef6a4d0a..8a1fa3ed15 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -60,7 +60,7 @@ val is_computing : coqtop -> bool
val spawn_coqtop : string list -> coqtop
(** Create a coqtop process with some command-line arguments. *)
-val set_reset_handler : coqtop -> (reset_kind -> unit task) -> unit
+val set_reset_handler : coqtop -> unit task -> unit
(** Register a handler called when a coqtop dies (badly or on purpose) *)
val set_feedback_handler : coqtop -> (Feedback.feedback -> unit) -> unit
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 6ffe771da3..f0e767cba3 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -136,7 +136,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
@@ -460,7 +460,9 @@ 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 (loc, msg));
@@ -842,10 +844,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
diff --git a/ide/coqOps.mli b/ide/coqOps.mli
index 4a37a1fa55..332c18f2f0 100644
--- a/ide/coqOps.mli
+++ b/ide/coqOps.mli
@@ -15,7 +15,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
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 9f10b2502a..86e09922c5 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -472,11 +472,11 @@ let print_xml =
with e -> let e = Errors.push e in Mutex.unlock m; iraise e
-let slave_logger xml_oc level message =
+let slave_logger xml_oc ?loc level message =
(* convert the message into XML *)
let msg = hov 0 message in
- let () = pr_debug (Printf.sprintf "-> %S" (string_of_ppcmds msg)) in
- let xml = Xmlprotocol.of_message level (Richpp.richpp_of_pp message) in
+ let () = pr_debug (Printf.sprintf "-> %S" (string_of_ppcmds msg)) in
+ let xml = Xmlprotocol.of_message level loc (Richpp.richpp_of_pp message) in
print_xml xml_oc xml
let slave_feeder xml_oc msg =
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 00c3f88e56..f0698a54a3 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -301,7 +301,7 @@ type logger = Feedback.level -> Richpp.richpp -> unit
let default_logger level message =
let level = match level with
- | Feedback.Debug _ -> `DEBUG
+ | Feedback.Debug -> `DEBUG
| Feedback.Info -> `INFO
| Feedback.Notice -> `NOTICE
| Feedback.Warning -> `WARNING
diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml
index f445f2e08d..53a29008ad 100644
--- a/ide/texmacspp.ml
+++ b/ide/texmacspp.ml
@@ -238,6 +238,8 @@ and pp_local_binder lb = (* don't know what it is for now *)
let ppl =
List.map (fun (loc, nam) -> (xmlCst (string_of_name nam) loc)) namll in
xmlTyped (ppl @ [pp_expr ce])
+ | LocalPattern _ ->
+ assert false
and pp_local_decl_expr lde = (* don't know what it is for now *)
match lde with
| AssumExpr (_, ce) -> pp_expr ce
@@ -351,6 +353,7 @@ and pp_cases_pattern_expr cpe =
xmlApply loc
(xmlOperator "delimiter" ~attr:["name", delim] loc ::
[pp_cases_pattern_expr cpe])
+ | CPatCast _ -> assert false
and pp_case_expr (e, name, pat) =
match name, pat with
| None, None -> xmlScrutinee [pp_expr e]
diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml
index a55d19aa1b..79509fe021 100644
--- a/ide/xmlprotocol.ml
+++ b/ide/xmlprotocol.ml
@@ -769,34 +769,37 @@ let document to_string_fmt =
open Feedback
let of_message_level = function
- | Debug s ->
- Serialize.constructor "message_level" "debug" [Xml_datatype.PCData s]
+ | Debug ->
+ Serialize.constructor "message_level" "debug" []
| Info -> Serialize.constructor "message_level" "info" []
| Notice -> Serialize.constructor "message_level" "notice" []
| Warning -> Serialize.constructor "message_level" "warning" []
| Error -> Serialize.constructor "message_level" "error" []
let to_message_level =
Serialize.do_match "message_level" (fun s args -> match s with
- | "debug" -> Debug (Serialize.raw_string args)
+ | "debug" -> Debug
| "info" -> Info
| "notice" -> Notice
| "warning" -> Warning
| "error" -> Error
| x -> raise Serialize.(Marshal_error("error level",PCData x)))
-let of_message lvl msg =
+let of_message lvl loc msg =
let lvl = of_message_level lvl in
+ let xloc = of_option of_loc loc in
let content = of_richpp msg in
- Xml_datatype.Element ("message", [], [lvl; content])
+ Xml_datatype.Element ("message", [], [lvl; xloc; content])
+
let to_message xml = match xml with
- | Xml_datatype.Element ("message", [], [lvl; content]) ->
- Message(to_message_level lvl, to_richpp content)
+ | Xml_datatype.Element ("message", [], [lvl; xloc; content]) ->
+ Message(to_message_level lvl, to_option to_loc xloc, to_richpp content)
| x -> raise (Marshal_error("message",x))
-let is_message = function
- | Xml_datatype.Element ("message", [], [lvl; content]) ->
- Some (to_message_level lvl, to_richpp content)
- | _ -> None
+let is_message xml =
+ try begin match to_message xml with
+ | Message(l,c,m) -> Some (l,c,m)
+ | _ -> None
+ end with | Marshal_error _ -> None
let to_feedback_content = do_match "feedback_content" (fun s a -> match s,a with
| "addedaxiom", _ -> AddedAxiom
@@ -809,7 +812,6 @@ let to_feedback_content = do_match "feedback_content" (fun s a -> match s,a with
to_string modpath, to_string ident, to_string ty)
| "globdef", [loc; ident; secpath; ty] ->
GlobDef(to_loc loc, to_string ident, to_string secpath, to_string ty)
- | "errormsg", [loc; s] -> ErrorMsg (to_loc loc, to_string s)
| "inprogress", [n] -> InProgress (to_int n)
| "workerstatus", [ns] ->
let n, s = to_pair to_string to_string ns in
@@ -843,8 +845,6 @@ let of_feedback_content = function
of_string ident;
of_string secpath;
of_string ty ]
- | ErrorMsg(loc, s) ->
- constructor "feedback_content" "errormsg" [of_loc loc; of_string s]
| InProgress n -> constructor "feedback_content" "inprogress" [of_int n]
| WorkerStatus(n,s) ->
constructor "feedback_content" "workerstatus"
@@ -861,7 +861,7 @@ let of_feedback_content = function
constructor "feedback_content" "fileloaded" [
of_string dirpath;
of_string filename ]
- | Message (l,m) -> constructor "feedback_content" "message" [ of_message l m ]
+ | Message (l,loc,m) -> constructor "feedback_content" "message" [ of_message l loc m ]
let of_edit_or_state_id = function
| Edit id -> ["object","edit"], of_edit_id id
diff --git a/ide/xmlprotocol.mli b/ide/xmlprotocol.mli
index 6bca8772ed..1bb9989704 100644
--- a/ide/xmlprotocol.mli
+++ b/ide/xmlprotocol.mli
@@ -66,7 +66,7 @@ val of_feedback : Feedback.feedback -> xml
val to_feedback : xml -> Feedback.feedback
val is_feedback : xml -> bool
-val is_message : xml -> (Feedback.level * Richpp.richpp) option
-val of_message : Feedback.level -> Richpp.richpp -> xml
+val is_message : xml -> (Feedback.level * Loc.t option * Richpp.richpp) option
+val of_message : Feedback.level -> Loc.t option -> Richpp.richpp -> xml
(* val to_message : xml -> Feedback.message *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 21:50:03 +0000