diff options
Diffstat (limited to 'toplevel/ide_intf.mli')
| -rw-r--r-- | toplevel/ide_intf.mli | 9 |
1 files changed, 7 insertions, 2 deletions
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; } |