maction layout added to notation

[helm.git] / helm / software / components / content_pres / cicNotationParser.ml

diff --git a/helm/software/components/content_pres/cicNotationParser.ml b/helm/software/components/content_pres/cicNotationParser.ml
index 60eb41424f23d7e802fb80d09f28f7ef2cee2619..8ddb78781a1f74214bb7ad4cdebc8de8241693fc 100644 (file)
--- a/helm/software/components/content_pres/cicNotationParser.ml
+++ b/helm/software/components/content_pres/cicNotationParser.ml
@@ -187,6 +187,7 @@ let extract_term_production pattern =
     | Ast.Group pl -> List.flatten (List.map aux pl)
     | Ast.Mstyle (_,pl) -> List.flatten (List.map aux pl)
     | Ast.Mpadded (_,pl) -> List.flatten (List.map aux pl)
+    | Ast.Maction l -> List.flatten (List.map aux l)
   and aux_magic magic =
     match magic with
     | Ast.Opt p ->
@@ -257,7 +258,7 @@ let owned_keywords = ref (initial_owned_keywords ())
 
 type checked_l1_pattern = CL1P of CicNotationPt.term * int
 
-let check_l1_pattern level1_pattern level associativity =
+let check_l1_pattern level1_pattern pponly level associativity =
   let variables = ref 0 in
   let symbols = ref 0 in
   let rec aux = function
@@ -283,6 +284,10 @@ let check_l1_pattern level1_pattern level associativity =
     | Ast.Group pl -> Ast.Group (List.map aux pl)
     | Ast.Mstyle (l,pl) -> Ast.Mstyle (l, List.map aux pl)
     | Ast.Mpadded (l,pl) -> Ast.Mpadded (l, List.map aux pl)
+    | Ast.Maction l as t -> 
+        if not pponly then 
+        raise(Parse_error("Maction can be used only in output notations")) 
+        else t
   and aux_magic magic =
     match magic with
     | Ast.Opt p -> Ast.Opt (aux p)
@@ -505,6 +510,10 @@ EXTEND
           return_term_of_level loc 
             (fun l -> 
                Ast.Layout (Ast.Mpadded (m, t l)))
+      | "maction"; m = LIST1 [ LPAREN; l = l1_pattern; RPAREN -> l ] ->
+           return_term_of_level loc 
+            (fun l -> Ast.Layout (Ast.Maction (List.map (fun x ->
+              CicNotationUtil.group (x l)) m)))
       | LPAREN; p = l1_pattern; RPAREN ->
           return_term_of_level loc (fun l -> CicNotationUtil.group (p l))
       ]