maction layout added to notation

diff --git a/helm/software/components/acic_content/cicNotationPp.ml b/helm/software/components/acic_content/cicNotationPp.ml
index 4d68dadf9f682e89743593f00bcc0a2322494247..a994c9fd166b83feb063e6e27a4cca1eed38ebaa 100644 (file)
--- a/helm/software/components/acic_content/cicNotationPp.ml
+++ b/helm/software/components/acic_content/cicNotationPp.ml
@@ -212,7 +212,10 @@ and pp_layout = function
   | Ast.Over (t1, t2) -> sprintf "[%s \\OVER %s]" (pp_term t1) (pp_term t2)
   | Ast.Atop (t1, t2) -> sprintf "[%s \\ATOP %s]" (pp_term t1) (pp_term t2)
   | Ast.Frac (t1, t2) -> sprintf "\\FRAC %s %s" (pp_term t1) (pp_term t2)
-  | Ast.InfRule (t1, t2, t3) -> sprintf "\\INFRULE %s %s %s" (pp_term t1) (pp_term t2) (pp_term t3)
+  | Ast.InfRule (t1, t2, t3) -> sprintf "\\INFRULE %s %s %s" (pp_term t1)
+  (pp_term t2) (pp_term t3)
+  | Ast.Maction l -> sprintf "\\MACTION (%s)" 
+     (String.concat "," (List.map pp_term l))
   | Ast.Sqrt t -> sprintf "\\SQRT %s" (pp_term t)
   | Ast.Root (arg, index) ->
       sprintf "\\ROOT %s \\OF %s" (pp_term index) (pp_term arg)

diff --git a/helm/software/components/acic_content/cicNotationPt.ml b/helm/software/components/acic_content/cicNotationPt.ml
index cfbd21b3a7f0c61f48e07e97dcdd8993ec53b6f7..3ffa9525808119fcd64a423bb1251feab46ea294 100644 (file)
--- a/helm/software/components/acic_content/cicNotationPt.ml
+++ b/helm/software/components/acic_content/cicNotationPt.ml
@@ -122,6 +122,7 @@ and layout_pattern =
   | InfRule of term * term * term
 (*   | array of term * literal option * literal option
       |+ column separator, row separator +| *)
+  | Maction of term list
   | Sqrt of term
   | Root of term * term (* argument, index *)
   | Break

diff --git a/helm/software/components/acic_content/cicNotationUtil.ml b/helm/software/components/acic_content/cicNotationUtil.ml
index 1ddd5c9c3b1572c74034fb70b4f2563867ee6786..48258d7bafffc17a66d23846cdc2f2fcdb1ceb35 100644 (file)
--- a/helm/software/components/acic_content/cicNotationUtil.ml
+++ b/helm/software/components/acic_content/cicNotationUtil.ml
@@ -99,6 +99,7 @@ let visit_layout k = function
   | Ast.Group terms -> Ast.Group (List.map k terms)
   | Ast.Mstyle (l, term) -> Ast.Mstyle (l, List.map k term)
   | Ast.Mpadded (l, term) -> Ast.Mpadded (l, List.map k term)
+  | Ast.Maction terms -> Ast.Maction (List.map k terms)
 
 let visit_magic k = function
   | Ast.List0 (t, l) -> Ast.List0 (k t, l)

diff --git a/helm/software/components/content_pres/cicNotationLexer.ml b/helm/software/components/content_pres/cicNotationLexer.ml
index bbc901dab7db3e2f139e37e6e65639efe1d2abd4..ac3b1142252dda604e88ccde5c86b32af757865b 100644 (file)
--- a/helm/software/components/content_pres/cicNotationLexer.ml
+++ b/helm/software/components/content_pres/cicNotationLexer.ml
@@ -88,7 +88,8 @@ let level1_layouts =
   [ "sub"; "sup";
     "below"; "above";
     "over"; "atop"; "frac";
-    "sqrt"; "root"
+    "sqrt"; "root"; "mstyle" ; "mpadded"; "maction"
+
   ]
 
 let level1_keywords =
@@ -96,7 +97,7 @@ let level1_keywords =
     "break";
     "list0"; "list1"; "sep";
     "opt";
-    "term"; "ident"; "number"; "mstyle" ; "mpadded"
+    "term"; "ident"; "number";
   ] @ level1_layouts
 
 let level2_meta_keywords =
@@ -131,9 +132,7 @@ let _ =
   List.iter
     (fun (ligature, symbol) -> Hashtbl.add ligatures ligature symbol)
     [ ("->", <:unicode<to>>);   ("=>", <:unicode<Rightarrow>>);
-      ("<=", <:unicode<leq>>);  (">=", <:unicode<geq>>);
-      ("<>", <:unicode<neq>>);  (":=", <:unicode<def>>);
-      ("==", <:unicode<equiv>>);
+      (":=", <:unicode<def>>);
     ]
 
 let regexp uri_step = [ 'a' - 'z' 'A' - 'Z' '0' - '9' '_' '-' ''' ]+

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))
       ]

diff --git a/helm/software/components/content_pres/cicNotationParser.mli b/helm/software/components/content_pres/cicNotationParser.mli
index 433711edd29ab9c5620641ace4704fa073b0c352..ba9003e90619594f5edcf108edb85cd6a4542e7c 100644 (file)
--- a/helm/software/components/content_pres/cicNotationParser.mli
+++ b/helm/software/components/content_pres/cicNotationParser.mli
@@ -44,8 +44,8 @@ type rule_id
 
 val compare_rule_id : rule_id -> rule_id -> int
 
-val check_l1_pattern: (* level1_pattern *)
- CicNotationPt.term -> int -> Gramext.g_assoc -> checked_l1_pattern
+val check_l1_pattern: (* level1_pattern, pponly, precedence, assoc *)
+ CicNotationPt.term -> bool ->  int -> Gramext.g_assoc -> checked_l1_pattern
 
 val extend:
   checked_l1_pattern ->

diff --git a/helm/software/components/content_pres/cicNotationPres.ml b/helm/software/components/content_pres/cicNotationPres.ml
index c4dd944b4b956c65479adc70e7d424ae220638a5..1a092909e113cdafcd00343281d5b9192c2056b8 100644 (file)
--- a/helm/software/components/content_pres/cicNotationPres.ml
+++ b/helm/software/components/content_pres/cicNotationPres.ml
@@ -411,6 +411,8 @@ let render ids_to_uris ?(prec=(-1)) =
            box_of mathonly (A.H, false, false) attrs 
             (aux_children mathonly false xref  prec 
               (CicNotationUtil.ungroup terms)))
+    | A.Maction alternatives -> 
+         toggle_action (List.map invoke_reinit alternatives)
     | A.Group terms ->
        let children =
           aux_children mathonly false xref  prec

diff --git a/helm/software/components/lexicon/cicNotation.ml b/helm/software/components/lexicon/cicNotation.ml
index 2b963e94e410e1307f219cdd10ca7dfacd20cd33..ebc9463ee6b457ed8ae3395d419f13c3872c7440 100644 (file)
--- a/helm/software/components/lexicon/cicNotation.ml
+++ b/helm/software/components/lexicon/cicNotation.ml
@@ -49,7 +49,8 @@ let process_notation st =
   match st with
   | Notation (loc, dir, l1, associativity, precedence, l2) ->
       let l1 = 
-        CicNotationParser.check_l1_pattern l1 precedence associativity
+        CicNotationParser.check_l1_pattern
+         l1 (dir = Some `RightToLeft) precedence associativity
       in
       let item = (l1, precedence, associativity, l2) in
       let rule_id = ref [] in