diff options
| author | ppedrot | 2013-02-18 19:45:36 +0000 |
|---|---|---|
| committer | ppedrot | 2013-02-18 19:45:36 +0000 |
| commit | 4c1ccb9e2a4b219ac5180115bc4267e1b059cdd1 (patch) | |
| tree | 9ecfc27037e02802b1e6884517ca930cb8197cbc /parsing | |
| parent | b101df5536146b9c3cd3569fc3b6334650f2a300 (diff) | |
Removing Exc_located and using the new exception enrichement
mechanism to retrieve the same information.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16215 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/compat.ml4 | 4 | ||||
| -rw-r--r-- | parsing/lexer.ml4 | 5 |
2 files changed, 5 insertions, 4 deletions
diff --git a/parsing/compat.ml4 b/parsing/compat.ml4 index 637b427a03..e82f352742 100644 --- a/parsing/compat.ml4 +++ b/parsing/compat.ml4 @@ -193,7 +193,7 @@ module GrammarMake (L:LexerSig) : GrammarSig = struct let entry_create = Entry.create let entry_parse e p = try Entry.parse e p - with Exc_located (loc,e) -> raise (Loc.Exc_located (to_coqloc loc,e)) + with Exc_located (loc,e) -> raise (Loc.add_loc e (to_coqloc loc)) IFDEF CAMLP5_6_02_1 THEN let entry_print ft x = Entry.print ft x ELSE @@ -221,7 +221,7 @@ end module GrammarMake (L:LexerSig) : GrammarSig = struct (* We need to refer to Coq's module Loc before it is hidden by include *) - let raise_coq_loc loc e = raise (Loc.Exc_located (to_coqloc loc,e)) + let raise_coq_loc loc e = raise (Loc.add_loc e (to_coqloc loc)) include Camlp4.Struct.Grammar.Static.Make (L) type 'a entry = 'a Entry.t type action = Action.t diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4 index 4b3a3f3a1a..91e7846dc0 100644 --- a/parsing/lexer.ml4 +++ b/parsing/lexer.ml4 @@ -171,8 +171,9 @@ let lookup_utf8 cs = | Some ('\x80'..'\xFF' as c) -> Utf8Token (lookup_utf8_tail c cs) | None -> EmptyStream -let unlocated f x = - try f x with Loc.Exc_located (_, exc) -> raise exc +let unlocated f x = f x + (** FIXME: should we still unloc the exception? *) +(* try f x with Loc.Exc_located (_, exc) -> raise exc *) let check_keyword str = let rec loop_symb = parser |
