aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/ide_slave.mli
blob: fb927cf33f6e9547cb374de86e1d800e88fcb90e (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(** [Ide_slave] : an implementation of [Ide_intf], i.e. mainly an interp
    function and a rewind function. This specialized loop is triggered
    when the -ideslave option is passed to Coqtop. Currently CoqIDE is
    the only one using this mode, but we try here to be as generic as
    possible, so this may change in the future... *)

val init_stdout : unit -> unit

val loop : unit -> unit