diff options
| author |  gmelquio <gmelquio@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-12-14 13:44:13 +0000 |
|---|---|---|
| committer | gmelquio <gmelquio@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-12-14 13:44:13 +0000 |
| commit | ed39b35b780c1fac9eb110f303014683e6640c01 (patch) | |
| tree | a014575b204996d16f7bfc817920e0046d6e73a4 /toplevel | |
| parent | 90ceeebb707149808061232a9c0e8b2d2bde0800 (diff) | |
Add improved indenters that rely on the current proof state to choose the indentation depth.
Patch by Cedric Auger.
These two indenters need to be exercised a bit to see if they are actually useful to users.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13715 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/ide_blob.ml | 9 | ||||
| -rw-r--r-- | toplevel/ide_blob.mli | 2 |
2 files changed, 10 insertions, 1 deletions
diff --git a/toplevel/ide_blob.ml b/toplevel/ide_blob.ml index c4036af9f..1fd42e419 100644 --- a/toplevel/ide_blob.ml +++ b/toplevel/ide_blob.ml @@ -512,6 +512,7 @@ let explain_exn e = in toploc,(Cerrors.explain_exn exc) +let contents () = Lib.contents_after None (** * Wrappers around Coq calls. We use phantom types and GADT to protect ourselves @@ -527,6 +528,7 @@ type 'a call = | Cur_goals | Cur_status | Cases of string + | Contents type 'a value = | Good of 'a @@ -546,7 +548,9 @@ let eval_call c = | Read_stdout -> Obj.magic (read_stdout ()) | Cur_goals -> Obj.magic (current_goals ()) | Cur_status -> Obj.magic (current_status ()) - | Cases s -> Obj.magic (make_cases s)) + | Cases s -> Obj.magic (make_cases s) + | Contents -> Obj.magic (contents ()) + ) with e -> let (l,pp) = explain_exn (filter_compat_exn e) in (* force evaluation of format stream *) @@ -576,6 +580,9 @@ let current_status : string call = let make_cases s : string list list call = Cases s +let contents : Lib.library_segment call = + Contents + (* End of wrappers *) let loop () = diff --git a/toplevel/ide_blob.mli b/toplevel/ide_blob.mli index 34879f057..b1261e496 100644 --- a/toplevel/ide_blob.mli +++ b/toplevel/ide_blob.mli @@ -43,4 +43,6 @@ val current_goals : goals call val read_stdout : string call +val contents : Lib.library_segment call + val loop : unit -> unit |