diff options
| author | herbelin | 2010-12-02 17:43:56 +0000 |
|---|---|---|
| committer | herbelin | 2010-12-02 17:43:56 +0000 |
| commit | e895f9ca19247f4fe58833f91e948e200bc9a6e5 (patch) | |
| tree | b6be61c1a3c94e8db8ed2f293ce8ad6b56fbcb6b /toplevel | |
| parent | 6342bc95a166d224ea64f1e3b8977e4f3560b485 (diff) | |
Fixing a bug introduced in r12304 (move of interpretation of
Local/Global modifiers in interpretation loop so as to support
Local/Global for grammar extension) that made use of
DuringSyntaxChecking error wrapper inappropriately nested with the
DuringCommandInterp error wrapper, what disturbed the error
processors. Good thing, we can now simplify things and completely
remove the DuringSyntaxChecking wrapper.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13667 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/ide_blob.ml | 3 | ||||
| -rw-r--r-- | toplevel/toplevel.ml | 7 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 3 | ||||
| -rw-r--r-- | toplevel/vernacexpr.ml | 5 |
4 files changed, 5 insertions, 13 deletions
diff --git a/toplevel/ide_blob.ml b/toplevel/ide_blob.ml index b90b44687c..3bd9462cef 100644 --- a/toplevel/ide_blob.ml +++ b/toplevel/ide_blob.ml @@ -529,8 +529,7 @@ type 'a value = let eval_call c = let filter_compat_exn = function - | Vernac.DuringCommandInterp (loc,inner) - | Vernacexpr.DuringSyntaxChecking (loc,inner) -> inner + | Vernac.DuringCommandInterp (loc,inner) -> inner | Vernacexpr.Quit -> raise Vernacexpr.Quit | e -> e in diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index 7b3acfa619..ddf3ac6575 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -275,7 +275,6 @@ let rec is_pervasive_exn = function | Error_in_file (_,_,e) -> is_pervasive_exn e | Loc.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 @@ -284,8 +283,7 @@ let rec is_pervasive_exn = function let print_toplevel_error exc = let (dloc,exc) = match exc with - | DuringCommandInterp (loc,ie) - | DuringSyntaxChecking (loc,ie) -> + | DuringCommandInterp (loc,ie) -> if loc = dummy_loc then (None,ie) else (Some loc, ie) | _ -> (None, exc) in @@ -334,8 +332,7 @@ let rec discard_to_dot () = * in encountered. *) let process_error = function - | DuringCommandInterp _ - | DuringSyntaxChecking _ as e -> e + | DuringCommandInterp _ as e -> e | e -> if is_pervasive_exn e then e diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 1df58a10ae..2293707e2d 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -33,8 +33,7 @@ exception HasNotFailed let raise_with_file file exc = let (cmdloc,re) = match exc with - | DuringCommandInterp(loc,e) - | DuringSyntaxChecking(loc,e) -> (loc,e) + | DuringCommandInterp(loc,e) -> (loc,e) | e -> (dummy_loc,e) in let (inner,inex) = diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 36c2b26c01..797fc79c6c 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -351,10 +351,7 @@ 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 located - -let syntax_checking_error loc s = - raise (DuringSyntaxChecking (loc,UserError ("",Pp.str s))) +let syntax_checking_error loc s = user_err_loc (loc,"",Pp.str s) (**********************************************************************) (* Managing locality *) |