aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--ide/coq.mli2
-rw-r--r--ide/coqide.ml20
-rw-r--r--toplevel/ide_intf.ml56
-rw-r--r--toplevel/ide_intf.mli9
-rw-r--r--toplevel/ide_slave.ml11
5 files changed, 75 insertions, 23 deletions
diff --git a/ide/coq.mli b/ide/coq.mli
index 047a26587..b3b51d3fc 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -48,7 +48,7 @@ val interrupter : (int -> unit) ref
val interp :
coqtop -> ?raw:bool -> ?verbose:bool -> string -> string Ide_intf.value
val rewind : coqtop -> int -> int Ide_intf.value
-val status : coqtop -> string Ide_intf.value
+val status : coqtop -> Ide_intf.status Ide_intf.value
val goals : coqtop -> Ide_intf.goals Ide_intf.value
val inloadpath : coqtop -> string -> bool Ide_intf.value
val mkcases : coqtop -> string -> string list list Ide_intf.value
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 899d0d6ca..d224e72b5 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -2179,11 +2179,21 @@ let main files =
let av = current.analyzed_view in
ignore (f av);
pop_info ();
- push_info
- (match Coq.status !(current.toplvl) with
- | Ide_intf.Fail (l,str) ->
- "Oops, problem while fetching coq status."
- | Ide_intf.Good str -> str)
+ let msg = match Coq.status !(current.toplvl) with
+ | Ide_intf.Fail (l, str) ->
+ "Oops, problem while fetching coq status."
+ | Ide_intf.Good status ->
+ let path = match status.Ide_intf.status_path with
+ | None -> ""
+ | Some p -> " in " ^ p
+ in
+ let name = match status.Ide_intf.status_proofname with
+ | None -> ""
+ | Some n -> ", proving " ^ n
+ in
+ "Ready" ^ path ^ name
+ in
+ push_info msg
)
[session_notebook#current_term]
in
diff --git a/toplevel/ide_intf.ml b/toplevel/ide_intf.ml
index 18a602af2..ac190c122 100644
--- a/toplevel/ide_intf.ml
+++ b/toplevel/ide_intf.ml
@@ -14,6 +14,11 @@ type xml = Xml_parser.xml
type 'a menu = 'a * (string * string) list
+type status = {
+ status_path : string option;
+ status_proofname : string option;
+}
+
type goal = {
goal_hyp : string list;
goal_ccl : string;
@@ -42,7 +47,7 @@ type 'a call =
let interp (r,b,s) : string call = Interp (r,b,s)
let rewind i : int call = Rewind i
let goals : goals call = Goal
-let status : string call = Status
+let status : status call = Status
let inloadpath s : bool call = InLoadPath s
let mkcases s : string list list call = MkCases s
@@ -58,7 +63,7 @@ type handler = {
interp : raw * verbose * string -> string;
rewind : int -> int;
goals : unit -> goals;
- status : unit -> string;
+ status : unit -> status;
inloadpath : string -> bool;
mkcases : string -> string list list;
}
@@ -182,6 +187,15 @@ let to_call = function
end
| _ -> raise Marshal_error
+let of_option f = function
+| None -> Element ("option", ["val", "none"], [])
+| Some x -> Element ("option", ["val", "some"], [f x])
+
+let to_option f = function
+| Element ("option", ["val", "none"], []) -> None
+| Element ("option", ["val", "some"], [x]) -> Some (f x)
+| _ -> raise Marshal_error
+
let of_string s = Element ("string", [], [PCData s])
let to_string = function
@@ -200,6 +214,18 @@ let to_pair f g = function
| Element ("pair", [], [x; y]) -> (f x, g y)
| _ -> raise Marshal_error
+let of_status s =
+ let of_so = of_option of_string in
+ Element ("status", [], [of_so s.status_path; of_so s.status_proofname])
+
+let to_status = function
+| Element ("status", [], [path; name]) ->
+ {
+ status_path = to_option to_string path;
+ status_proofname = to_option to_string name;
+ }
+| _ -> raise Marshal_error
+
let of_goal g =
let hyp = of_list of_string g.goal_hyp in
let ccl = of_string g.goal_ccl in
@@ -248,7 +274,7 @@ let of_answer (q : 'a call) (r : 'a value) =
| Interp _ -> Obj.magic (of_string : string -> xml)
| Rewind _ -> Obj.magic (of_int : int -> xml)
| Goal -> Obj.magic (of_goals : goals -> xml)
- | Status -> Obj.magic (of_string : string -> xml)
+ | Status -> Obj.magic (of_status : status -> xml)
| InLoadPath _ -> Obj.magic (of_bool : bool -> xml)
| MkCases _ -> Obj.magic (of_list (of_list of_string) : string list list -> xml)
in
@@ -261,6 +287,7 @@ let to_answer xml =
| "string" -> Obj.magic (to_string elt)
| "int" -> Obj.magic (to_int elt)
| "goals" -> Obj.magic (to_goals elt)
+ | "status" -> Obj.magic (to_status elt)
| "bool" -> Obj.magic (to_bool elt)
| "list" -> Obj.magic (to_list convert elt)
| _ -> raise Marshal_error
@@ -291,6 +318,17 @@ let pr_value v = pr_value_gen (fun _ -> "") v
let pr_string s = "["^s^"]"
let pr_bool b = if b then "true" else "false"
+let pr_status s =
+ let path = match s.status_path with
+ | None -> "no path; "
+ | Some p -> "path = " ^ p ^ "; "
+ in
+ let name = match s.status_proofname with
+ | None -> "no proof;"
+ | Some n -> "proof = " ^ n ^ ";"
+ in
+ "Status: " ^ path ^ name
+
let pr_mkcases l =
let l = List.map (String.concat " ") l in
"[" ^ String.concat " | " l ^ "]"
@@ -309,9 +347,9 @@ let pr_goals = function
let pr_full_value call value =
match call with
- | Interp _ -> pr_value_gen pr_string (Obj.magic value)
- | Rewind i -> pr_value_gen string_of_int (Obj.magic value)
- | Goal -> pr_value_gen pr_goals (Obj.magic value)
- | Status -> pr_value_gen pr_string (Obj.magic value)
- | InLoadPath s -> pr_value_gen pr_bool (Obj.magic value)
- | MkCases s -> pr_value_gen pr_mkcases (Obj.magic value)
+ | Interp _ -> pr_value_gen pr_string (Obj.magic value : string value)
+ | Rewind i -> pr_value_gen string_of_int (Obj.magic value : int value)
+ | Goal -> pr_value_gen pr_goals (Obj.magic value : goals value)
+ | Status -> pr_value_gen pr_status (Obj.magic value : status value)
+ | InLoadPath s -> pr_value_gen pr_bool (Obj.magic value : bool value)
+ | MkCases s -> pr_value_gen pr_mkcases (Obj.magic value : string list list value)
diff --git a/toplevel/ide_intf.mli b/toplevel/ide_intf.mli
index 3752d0142..f1590e852 100644
--- a/toplevel/ide_intf.mli
+++ b/toplevel/ide_intf.mli
@@ -15,6 +15,11 @@ type goal = {
goal_ccl : string;
}
+type status = {
+ status_path : string option;
+ status_proofname : string option;
+}
+
type goals =
| No_current_proof
| Proof_completed
@@ -50,7 +55,7 @@ val rewind : int -> int call
val goals : goals call
(** The status, for instance "Ready in SomeSection, proving Foo" *)
-val status : string call
+val status : status call
(** Is a directory part of Coq's loadpath ? *)
val inloadpath : string -> bool call
@@ -75,7 +80,7 @@ type handler = {
interp : raw * verbose * string -> string;
rewind : int -> int;
goals : unit -> goals;
- status : unit -> string;
+ status : unit -> status;
inloadpath : string -> bool;
mkcases : string -> string list list;
}
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index a276f3292..7bfca463a 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -447,16 +447,15 @@ let status () =
let path =
let l = Names.repr_dirpath (Lib.cwd ()) in
let l = snd (Util.list_sep_last l) in
- if l = [] then "" else
- (" in "^Names.string_of_dirpath (Names.make_dirpath l))
+ if l = [] then None
+ else Some (Names.string_of_dirpath (Names.make_dirpath l))
in
let proof =
try
- ", proving " ^ (Names.string_of_id (Pfedit.get_current_proof_name ()))
- with _ -> ""
+ Some (Names.string_of_id (Pfedit.get_current_proof_name ()))
+ with _ -> None
in
- "Ready"^path^proof
-
+ { Ide_intf.status_path = path; Ide_intf.status_proofname = proof }
(** Grouping all call handlers together + error handling *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-01 21:49:34 +0000