summaryrefslogtreecommitdiff
path: root/toplevel/ide_intf.mli
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2012-01-12 16:02:20 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2012-01-12 16:02:20 +0100
commit97fefe1fcca363a1317e066e7f4b99b9c1e9987b (patch)
tree97ec6b7d831cc5fb66328b0c63a11db1cbb2f158 /toplevel/ide_intf.mli
parent300293c119981054c95182a90c829058530a6b6f (diff)
Imported Upstream version 8.4~betaupstream/8.4_beta
Diffstat (limited to 'toplevel/ide_intf.mli')
-rw-r--r--toplevel/ide_intf.mli87
1 files changed, 87 insertions, 0 deletions
diff --git a/toplevel/ide_intf.mli b/toplevel/ide_intf.mli
new file mode 100644
index 00000000..69204da1
--- /dev/null
+++ b/toplevel/ide_intf.mli
@@ -0,0 +1,87 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(** * Applicative part of the interface of CoqIde calls to Coq *)
+
+open Interface
+
+type xml = Xml_parser.xml
+
+type 'a call
+
+(** Running a command (given as a string).
+ - The 1st flag indicates whether to use "raw" mode
+ (less sanity checks, no impact on the undo stack).
+ Suitable e.g. for queries, or for the Set/Unset
+ of display options that coqide performs all the time.
+ - The 2nd flag controls the verbosity.
+ - The returned string contains the messages produced
+ by this command, but not the updated goals (they are
+ to be fetch by a separated [current_goals]). *)
+val interp : raw * verbose * string -> string call
+
+(** Backtracking by at least a certain number of phrases.
+ No finished proofs will be re-opened. Instead,
+ we continue backtracking until before these proofs,
+ and answer the amount of extra backtracking performed.
+ Backtracking by more than the number of phrases already
+ interpreted successfully (and not yet undone) will fail. *)
+val rewind : int -> int call
+
+(** Fetching the list of current goals. Return [None] if no proof is in
+ progress, [Some gl] otherwise. *)
+val goals : goals option call
+
+(** Retrieving the tactics applicable to the current goal. [None] if there is
+ no proof in progress. *)
+val hints : (hint list * hint) option call
+
+(** The status, for instance "Ready in SomeSection, proving Foo" *)
+val status : status call
+
+(** Is a directory part of Coq's loadpath ? *)
+val inloadpath : string -> bool call
+
+(** Create a "match" template for a given inductive type.
+ For each branch of the match, we list the constructor name
+ followed by enough pattern variables. *)
+val mkcases : string -> string list list call
+
+(** Retrieve the list of unintantiated evars in the current proof. [None] if no
+ proof is in progress. *)
+val evars : evar list option call
+
+(** Retrieve the list of options of the current toplevel, together with their
+ state. *)
+val get_options : (option_name * option_state) list call
+
+(** Set the options to the given value. Warning: this is not atomic, so whenever
+ the call fails, the option state can be messed up... This is the caller duty
+ to check that everything is correct. *)
+val set_options : (option_name * option_value) list -> unit call
+
+val abstract_eval_call : handler -> 'a call -> 'a value
+
+(** * XML data marshalling *)
+
+exception Marshal_error
+
+val of_value : ('a -> xml) -> 'a value -> xml
+val to_value : (xml -> 'a) -> xml -> 'a value
+
+val of_call : 'a call -> xml
+val to_call : xml -> 'a call
+
+val of_answer : 'a call -> 'a value -> xml
+val to_answer : xml -> 'a value
+
+(** * Debug printing *)
+
+val pr_call : 'a call -> string
+val pr_value : 'a value -> string
+val pr_full_value : 'a call -> 'a value -> string