summaryrefslogtreecommitdiff
path: root/toplevel/vernacinterp.ml
blob: 41669c478a8b3cb555951f0f00623340211eee94 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(* $Id: vernacinterp.ml 11309 2008-08-06 10:30:35Z herbelin $ *)

open Pp
open Util
open Names
open Libnames
open Himsg
open Proof_type
open Tacinterp
open Vernacexpr

let disable_drop e =
  if e <> Drop then e
  else UserError("Vernac.disable_drop",(str"Drop is forbidden."))

(* Table of vernac entries *)
let vernac_tab =
  (Hashtbl.create 51 :
    (string, Tacexpr.raw_generic_argument list -> unit -> unit) Hashtbl.t)

let vinterp_add s f =
  try 
    Hashtbl.add vernac_tab s f
  with Failure _ ->
    errorlabstrm "vinterp_add"
      (str"Cannot add the vernac command " ++ str s ++ str" twice.")

let overwriting_vinterp_add s f =
  begin 
    try 
      let _ = Hashtbl.find vernac_tab s in Hashtbl.remove vernac_tab s 
    with Not_found -> ()
  end;
  Hashtbl.add vernac_tab s f

let vinterp_map s =
  try 
    Hashtbl.find vernac_tab s
  with Not_found -> 
    errorlabstrm "Vernac Interpreter"
      (str"Cannot find vernac command " ++ str s ++ str".")

let vinterp_init () = Hashtbl.clear vernac_tab

(* Interpretation of a vernac command *)

let call (opn,converted_args) =
  let loc = ref "Looking up command" in
  try
    let callback = vinterp_map opn in
    loc:= "Checking arguments";
    let hunk = callback converted_args in
    loc:= "Executing command";
    hunk()
  with
    | Drop -> raise Drop
    | ProtectedLoop -> raise ProtectedLoop
    | e ->
        if !Flags.debug then
	  msgnl (str"Vernac Interpreter " ++ str !loc);
        raise e

let bad_vernac_args s =
  anomalylabstrm s
    (str"Vernac " ++ str s ++ str" called with bad arguments")