aboutsummaryrefslogtreecommitdiff
path: root/parsing
diff options
context:
space:
mode:
authorppedrot2013-02-18 19:45:36 +0000
committerppedrot2013-02-18 19:45:36 +0000
commit4c1ccb9e2a4b219ac5180115bc4267e1b059cdd1 (patch)
tree9ecfc27037e02802b1e6884517ca930cb8197cbc /parsing
parentb101df5536146b9c3cd3569fc3b6334650f2a300 (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.ml44
-rw-r--r--parsing/lexer.ml45
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