aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--parsing/g_proofs.ml48
-rw-r--r--parsing/g_vernac.ml426
-rw-r--r--parsing/pcoq.ml43
-rw-r--r--parsing/pcoq.mli2
-rw-r--r--toplevel/protectedtoplevel.ml7
-rw-r--r--toplevel/toplevel.ml8
-rw-r--r--toplevel/vernac.ml3
-rw-r--r--toplevel/vernacexpr.ml24
8 files changed, 46 insertions, 35 deletions
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index d5053dc82..0a486cb1e 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -90,10 +90,10 @@ GEXTEND Gram
| IDENT "Go"; IDENT "next" -> VernacGo GoNext
| IDENT "Guarded" -> VernacCheckGuard
(* Hints for Auto and EAuto *)
- | IDENT "Create"; local = locality; IDENT "HintDb" ;
+ | IDENT "Create"; IDENT "HintDb" ;
id = IDENT ; b = [ "discriminated" -> true | -> false ] ->
- VernacCreateHintDb (enforce_locality_of local, id, b)
- | IDENT "Hint"; local = locality; h = hint;
+ VernacCreateHintDb (use_locality (), id, b)
+ | IDENT "Hint"; local = obsolete_locality; h = hint;
dbnames = opt_hintbases ->
VernacHints (enforce_locality_of local,dbnames, h)
@@ -104,7 +104,7 @@ GEXTEND Gram
[Genarg.in_gen Genarg.rawwit_constr c])
] ];
- locality:
+ obsolete_locality:
[ [ IDENT "Local" -> true | -> false ] ]
;
hint:
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 57c2ef677..4b79113f3 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -114,13 +114,6 @@ GEXTEND Gram
;
END
-GEXTEND Gram
- GLOBAL: locality non_locality;
- locality:
- [ [ IDENT "Local" -> true | -> false ] ]
- ;
-END
-
let test_plurial_form = function
| [(_,([_],_))] ->
Flags.if_verbose warning
@@ -789,10 +782,10 @@ GEXTEND Gram
GLOBAL: syntax;
syntax:
- [ [ IDENT "Open"; local = locality; IDENT "Scope"; sc = IDENT ->
+ [ [ IDENT "Open"; local = obsolete_locality; IDENT "Scope"; sc = IDENT ->
VernacOpenCloseScope (enforce_locality_of local,true,sc)
- | IDENT "Close"; local = locality; IDENT "Scope"; sc = IDENT ->
+ | IDENT "Close"; local = obsolete_locality; IDENT "Scope"; sc = IDENT ->
VernacOpenCloseScope (enforce_locality_of local,false,sc)
| IDENT "Delimit"; IDENT "Scope"; sc = IDENT; "with"; key = IDENT ->
@@ -805,16 +798,17 @@ GEXTEND Gram
"["; scl = LIST0 opt_scope; "]" ->
VernacArgumentsScope (use_non_locality (),qid,scl)
- | IDENT "Infix"; local = locality;
+ | IDENT "Infix"; local = obsolete_locality;
op = ne_string; ":="; p = global;
modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
sc = OPT [ ":"; sc = IDENT -> sc ] ->
VernacInfix (enforce_locality_of local,(op,modl),p,sc)
- | IDENT "Notation"; local = locality; id = identref; idl = LIST0 ident;
- ":="; c = constr;
+ | IDENT "Notation"; local = obsolete_locality; id = identref;
+ idl = LIST0 ident; ":="; c = constr;
b = [ "("; IDENT "only"; IDENT "parsing"; ")" -> true | -> false ] ->
VernacSyntacticDefinition (id,(idl,c),enforce_locality_of local,b)
- | IDENT "Notation"; local = locality; s = ne_string; ":="; c = constr;
+ | IDENT "Notation"; local = obsolete_locality; s = ne_string; ":=";
+ c = constr;
modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
sc = OPT [ ":"; sc = IDENT -> sc ] ->
VernacNotation (enforce_locality_of local,c,(s,modl),sc)
@@ -823,7 +817,8 @@ GEXTEND Gram
pil = LIST1 production_item; ":="; t = Tactic.tactic
-> VernacTacticNotation (n,pil,t)
- | IDENT "Reserved"; IDENT "Notation"; local = locality; s = ne_string;
+ | IDENT "Reserved"; IDENT "Notation"; local = obsolete_locality;
+ s = ne_string;
l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]
-> VernacSyntaxExtension (enforce_locality_of local,(s,l))
@@ -831,6 +826,9 @@ GEXTEND Gram
to factorize with other "Print"-based vernac entries *)
] ]
;
+ obsolete_locality:
+ [ [ IDENT "Local" -> true | -> false ] ]
+ ;
tactic_level:
[ [ "("; "at"; IDENT "level"; n = natural; ")" -> n | -> 0 ] ]
;
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index ed4f41c4e..d81727487 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -496,9 +496,6 @@ module Vernac_ =
struct
let gec_vernac s = Gram.Entry.create ("vernac:" ^ s)
- let locality = gec_vernac "locality"
- let non_locality = gec_vernac "non_locality"
-
(* The different kinds of vernacular commands *)
let gallina = gec_vernac "gallina"
let gallina_ext = gec_vernac "gallina_ext"
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index e089389fe..f084c74f0 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -200,8 +200,6 @@ module Tactic :
module Vernac_ :
sig
open Decl_kinds
- val locality : bool Gram.Entry.e
- val non_locality : bool Gram.Entry.e
val gallina : vernac_expr Gram.Entry.e
val gallina_ext : vernac_expr Gram.Entry.e
val command : vernac_expr Gram.Entry.e
diff --git a/toplevel/protectedtoplevel.ml b/toplevel/protectedtoplevel.ml
index f62d1c81c..db5a5c4c5 100644
--- a/toplevel/protectedtoplevel.ml
+++ b/toplevel/protectedtoplevel.ml
@@ -11,6 +11,7 @@
open Pp
open Line_oriented_parser
open Vernac
+open Vernacexpr
(* The toplevel parsing loop we propose here is more robust to printing
errors. The philosophy is that all commands should be individually wrapped
@@ -130,7 +131,8 @@ let rec parse_one_command_group input_channel =
!global_request_id !count None)
| Some(rank, e) ->
(match e with
- DuringCommandInterp(a,e1) ->
+ | DuringCommandInterp(a,e1)
+ | Stdpp.Exc_located (a,DuringSyntaxChecking e1) ->
output_results_nl
(acknowledge_command
!global_request_id rank (Some e1))
@@ -164,7 +166,8 @@ let protected_loop input_chan =
| End_of_file -> exit 0
| DuringCommandInterp(loc, Vernacexpr.Quit) -> raise Vernacexpr.Quit
| DuringCommandInterp(loc, Vernacexpr.Drop) -> raise Vernacexpr.Drop
- | DuringCommandInterp(loc, e) ->
+ | DuringCommandInterp(loc, e)
+ | Stdpp.Exc_located (loc,DuringSyntaxChecking e) ->
explain_and_restart e
| e -> explain_and_restart e in
begin
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index 14207b5e5..7f869c166 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -13,6 +13,7 @@ open Util
open Flags
open Cerrors
open Vernac
+open Vernacexpr
open Pcoq
open Protectedtoplevel
@@ -262,6 +263,7 @@ let rec is_pervasive_exn = function
| Error_in_file (_,_,e) -> is_pervasive_exn e
| Stdpp.Exc_located (_,e) -> is_pervasive_exn e
| DuringCommandInterp (_,e) -> is_pervasive_exn e
+ | DuringSyntaxChecking e -> is_pervasive_exn e
| _ -> false
(* Toplevel error explanation, dealing with locations, Drop, Ctrl-D
@@ -270,7 +272,8 @@ let rec is_pervasive_exn = function
let print_toplevel_error exc =
let (dloc,exc) =
match exc with
- | DuringCommandInterp (loc,ie) ->
+ | DuringCommandInterp (loc,ie)
+ | Stdpp.Exc_located (loc, DuringSyntaxChecking ie) ->
if loc = dummy_loc then (None,ie) else (Some loc, ie)
| _ -> (None, exc)
in
@@ -321,7 +324,8 @@ let rec discard_to_dot () =
* in encountered. *)
let process_error = function
- | DuringCommandInterp _ as e -> e
+ | DuringCommandInterp _
+ | Stdpp.Exc_located (_,DuringSyntaxChecking _) as e -> e
| e ->
if is_pervasive_exn e then
e
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index cdfa85328..c7224ddaa 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -32,7 +32,8 @@ exception DuringCommandInterp of Util.loc * exn
let raise_with_file file exc =
let (cmdloc,re) =
match exc with
- | DuringCommandInterp(loc,e) -> (loc,e)
+ | DuringCommandInterp(loc,e)
+ | Stdpp.Exc_located (loc,DuringSyntaxChecking e) -> (loc,e)
| e -> (dummy_loc,e)
in
let (inner,inex) =
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 14bcb1ef7..5ea0235a5 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -338,6 +338,14 @@ type vernac_expr =
and located_vernac_expr = loc * vernac_expr
+(* Locating errors raised just after the dot is parsed but before the
+ interpretation phase *)
+
+exception DuringSyntaxChecking of exn
+
+let syntax_checking_error s =
+ raise (DuringSyntaxChecking (UserError ("",Pp.str s)))
+
(* Managing locality *)
let locality_flag = ref None
@@ -346,9 +354,9 @@ let local_of_bool = function true -> Local | false -> Global
let check_locality () =
if !locality_flag = Some true then
- error "This command does not support the \"Local\" prefix";
+ syntax_checking_error "This command does not support the \"Local\" prefix.";
if !locality_flag = Some false then
- error "This command does not support the \"Global\" prefix"
+ syntax_checking_error "This command does not support the \"Global\" prefix."
let use_locality () =
let local = match !locality_flag with Some true -> true | _ -> false in
@@ -373,9 +381,10 @@ let enforce_locality () =
let local =
match !locality_flag with
| Some false ->
- error "Cannot be simultaneously Local and Global"
+ error "Cannot be simultaneously Local and Global."
| _ ->
- Flags.if_verbose Pp.warning "Obsolete syntax: use \"Local\" prefix";
+ Flags.if_verbose
+ Pp.warning "Obsolete syntax: use \"Local\" as a prefix.";
true in
locality_flag := None;
local
@@ -386,12 +395,13 @@ let enforce_locality_of local =
let local =
match !locality_flag with
| Some false when local ->
- error "Cannot be simultaneously Local and Global"
+ error "Cannot be simultaneously Local and Global."
| Some true when local ->
- error "Use only prefix \"Local\""
+ error "Use only prefix \"Local\"."
| None ->
if local then
- Flags.if_verbose Pp.warning "Obsolete syntax: use \"Local\" prefix";
+ Flags.if_verbose
+ Pp.warning "Obsolete syntax: use \"Local\" as a prefix.";
local
| Some b -> b in
locality_flag := None;
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-15 09:54:21 +0000