From 5b318ca418ef27d1bf2b155bebbf2425f65b4f1f Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 17 Apr 2003 15:01:24 +0000
Subject: Ajout "at next level" dans Notation Mise en place structure pour
 définir un objet en même temps que sa notation

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3939 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/symbols.ml  | 11 +++++++++++
 interp/symbols.mli |  3 +++
 2 files changed, 14 insertions(+)

(limited to 'interp')

diff --git a/interp/symbols.ml b/interp/symbols.ml
index 0c988f315c..ef2cf6b0b8 100644
--- a/interp/symbols.ml
+++ b/interp/symbols.ml
@@ -396,6 +396,17 @@ let locate_notation prraw ntn =
 	  fnl ()))
       l
 
+let find_notation_level ntn =
+  let l = 
+    Stringmap.fold 
+      (fun _ sc l ->
+	try fst (snd (Stringmap.find ntn sc.notations)) :: l
+	with Not_found -> l) !scope_map [] in
+  match l with
+  | [] -> raise Not_found
+  | [prec] -> prec
+  | prec::_ -> warning ("Several parsing rules for notation \""^ntn^"\""); prec
+
 (**********************************************************************)
 (* Mapping notations to concrete syntax *)
 
diff --git a/interp/symbols.mli b/interp/symbols.mli
index 42eedaf81c..fa3d778f1b 100644
--- a/interp/symbols.mli
+++ b/interp/symbols.mli
@@ -117,6 +117,9 @@ val pr_scope : (rawconstr -> std_ppcmds) -> scope_name -> std_ppcmds
 val pr_scopes : (rawconstr -> std_ppcmds) -> std_ppcmds
 val locate_notation : (rawconstr -> std_ppcmds) -> notation -> std_ppcmds
 
+(* [raise Not_found] if non existing notation *)
+val find_notation_level : notation -> level
+
 (**********************************************************************)
 (*s Printing rules for notations *)
 
-- 
cgit v1.2.3