summaryrefslogtreecommitdiff
path: root/interp/notation.ml
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2007-08-18 20:34:57 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2007-08-18 20:34:57 +0000
commit72b9a7df489ea47b3e5470741fd39f6100d31676 (patch)
tree60108a573d2a80d2dd4e3833649890e32427ff8d /interp/notation.ml
parent55ce117e8083477593cf1ff2e51a3641c7973830 (diff)
Imported Upstream version 8.1.pl1+dfsgupstream/8.1.pl1+dfsg
Diffstat (limited to 'interp/notation.ml')
-rw-r--r--interp/notation.ml12
1 files changed, 9 insertions, 3 deletions
diff --git a/interp/notation.ml b/interp/notation.ml
index 7d70b296..08c6f31f 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: notation.ml 9481 2007-01-11 19:17:56Z herbelin $ *)
+(* $Id: notation.ml 9694 2007-03-09 18:09:53Z herbelin $ *)
(*i*)
open Util
@@ -393,8 +393,14 @@ let uninterp_prim_token_cases_pattern c =
| Some n -> (na,sc,n)
with Not_found -> raise No_match
-let availability_of_prim_token printer_scope local_scopes =
- let f scope = Hashtbl.mem prim_token_interpreter_tab scope in
+let availability_of_prim_token printer_scope local_scopes t =
+ let f scope =
+ try
+ (* raise Not_found if no primitive interpreter for scope *)
+ let interp = Hashtbl.find prim_token_interpreter_tab scope in
+ (* raise Not_found if no primitive interpreter for this token in scope *)
+ let _ = interp dummy_loc t in true
+ with Not_found -> false in
let scopes = make_current_scopes local_scopes in
option_map snd (find_without_delimiters f (Some printer_scope,None) scopes)