(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

{
open Pcoq
open Pcoq.Prim
open Vernacexpr

(* Vernaculars specific to the toplevel *)
type vernac_toplevel =
  | VernacBackTo of int
  | VernacDrop
  | VernacQuit
  | VernacControl of vernac_control
  | VernacShowGoal of { gid : int; sid: int }
  | VernacShowProofDiffs of Proof_diffs.diffOpt

module Toplevel_ : sig
  val vernac_toplevel : vernac_toplevel option Entry.t
end = struct
  let gec_vernac s = Entry.create ("toplevel:" ^ s)
  let vernac_toplevel = gec_vernac "vernac_toplevel"
end

open Toplevel_

let err () = raise Stream.Failure

let test_show_goal =
  let open Pcoq.Lookahead in
  to_entry "test_show_goal" begin
   lk_kw "Show" >> lk_kw "Goal" >> lk_nat
  end

}

GRAMMAR EXTEND Gram
  GLOBAL: vernac_toplevel;
  vernac_toplevel: FIRST
    [ [ IDENT "Drop"; "." -> { Some VernacDrop }
      | IDENT "Quit"; "." -> { Some VernacQuit }
      | IDENT "BackTo"; n = natural; "." ->
        { Some (VernacBackTo n) }
      (* show a goal for the specified proof state *)
      | test_show_goal; IDENT "Show"; IDENT "Goal"; gid = natural; IDENT "at"; sid = natural; "." ->
          { Some (VernacShowGoal {gid; sid}) }
      | IDENT "Show"; IDENT "Proof"; IDENT "Diffs"; removed = OPT [ IDENT "removed" -> { () } ]; "." ->
        { Some (VernacShowProofDiffs
          (if removed = None then Proof_diffs.DiffOn else Proof_diffs.DiffRemoved)) }
      | cmd = Pvernac.Vernac_.main_entry ->
              { match cmd with
              | None -> None
              | Some v -> Some (VernacControl v) }
      ]
    ]
  ;
END

{

let vernac_toplevel pm =
  Pvernac.Unsafe.set_tactic_entry pm;
  vernac_toplevel

}