- cicNotationParser: added extra space to TeX control sequences accordind to previous...

[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 695db149e3f0c2bc722629d589b8bfc39f61adb9..bb3d29f069d336544546c1a22e86fbdfc9a71f4c 100644 (file)
--- a/helm/software/components/content_pres/cicNotationParser.ml
+++ b/helm/software/components/content_pres/cicNotationParser.ml
@@ -170,18 +170,18 @@ let extract_term_production pattern =
         [NoBinding, gram_keyword s]
     | `Number s -> [NoBinding, gram_number s]
   and aux_layout = function
-    | Ast.Sub (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\sub"] @ aux p2
-    | Ast.Sup (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\sup"] @ aux p2
-    | Ast.Below (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\below"] @ aux p2
-    | Ast.Above (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\above"] @ aux p2
-    | Ast.Frac (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\frac"] @ aux p2
-    | Ast.InfRule (p1, p2, p3) -> [NoBinding, gram_symbol "\\infrule"] @ aux p1 @ aux p2 @ aux p3
-    | Ast.Atop (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\atop"] @ aux p2
-    | Ast.Over (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\over"] @ aux p2
+    | Ast.Sub (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\sub "] @ aux p2
+    | Ast.Sup (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\sup "] @ aux p2
+    | Ast.Below (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\below "] @ aux p2
+    | Ast.Above (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\above "] @ aux p2
+    | Ast.Frac (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\frac "] @ aux p2
+    | Ast.InfRule (p1, p2, p3) -> [NoBinding, gram_symbol "\\infrule "] @ aux p1 @ aux p2 @ aux p3
+    | Ast.Atop (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\atop "] @ aux p2
+    | Ast.Over (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\over "] @ aux p2
     | Ast.Root (p1, p2) ->
-        [NoBinding, gram_symbol "\\root"] @ aux p2
-        @ [NoBinding, gram_symbol "\\of"] @ aux p1
-    | Ast.Sqrt p -> [NoBinding, gram_symbol "\\sqrt"] @ aux p
+        [NoBinding, gram_symbol "\\root "] @ aux p2
+        @ [NoBinding, gram_symbol "\\of "] @ aux p1
+    | Ast.Sqrt p -> [NoBinding, gram_symbol "\\sqrt "] @ aux p
     | Ast.Break -> []
     | Ast.Box (_, pl) -> List.flatten (List.map aux pl)
     | Ast.Group pl -> List.flatten (List.map aux pl)
@@ -460,33 +460,33 @@ EXTEND
       v = [ PERCENTAGE ] -> id, v]];
   l1_simple_pattern:
     [ "layout" LEFTA
-      [ p1 = SELF; SYMBOL "\\sub"; p2 = SELF ->
+      [ p1 = SELF; SYMBOL "\\sub "; p2 = SELF ->
           return_term_of_level loc 
             (fun l -> Ast.Layout (Ast.Sub (p1 l, p2 l)))
-      | p1 = SELF; SYMBOL "\\sup"; p2 = SELF ->
+      | p1 = SELF; SYMBOL "\\sup "; p2 = SELF ->
           return_term_of_level loc 
             (fun l -> Ast.Layout (Ast.Sup (p1 l, p2 l)))
-      | p1 = SELF; SYMBOL "\\below"; p2 = SELF ->
+      | p1 = SELF; SYMBOL "\\below "; p2 = SELF ->
           return_term_of_level loc 
             (fun l -> Ast.Layout (Ast.Below (p1 l, p2 l)))
-      | p1 = SELF; SYMBOL "\\above"; p2 = SELF ->
+      | p1 = SELF; SYMBOL "\\above "; p2 = SELF ->
           return_term_of_level loc 
             (fun l -> Ast.Layout (Ast.Above (p1 l, p2 l)))
-      | p1 = SELF; SYMBOL "\\over"; p2 = SELF ->
+      | p1 = SELF; SYMBOL "\\over "; p2 = SELF ->
           return_term_of_level loc 
             (fun l -> Ast.Layout (Ast.Over (p1 l, p2 l)))
-      | p1 = SELF; SYMBOL "\\atop"; p2 = SELF ->
+      | p1 = SELF; SYMBOL "\\atop "; p2 = SELF ->
           return_term_of_level loc 
             (fun l -> Ast.Layout (Ast.Atop (p1 l, p2 l)))
-      | p1 = SELF; SYMBOL "\\frac"; p2 = SELF ->
+      | p1 = SELF; SYMBOL "\\frac "; p2 = SELF ->
           return_term_of_level loc 
             (fun l -> Ast.Layout (Ast.Frac (p1 l, p2 l)))
-      | SYMBOL "\\infrule"; p1 = SELF; p2 = SELF; p3 = SELF ->
+      | SYMBOL "\\infrule "; p1 = SELF; p2 = SELF; p3 = SELF ->
           return_term_of_level loc 
             (fun l -> Ast.Layout (Ast.InfRule (p1 l, p2 l, p3 l)))
-      | SYMBOL "\\sqrt"; p = SELF -> 
+      | SYMBOL "\\sqrt "; p = SELF -> 
           return_term_of_level loc (fun l -> Ast.Layout (Ast.Sqrt p l))
-      | SYMBOL "\\root"; index = SELF; SYMBOL "\\of"; arg = SELF ->
+      | SYMBOL "\\root "; index = SELF; SYMBOL "\\of "; arg = SELF ->
           return_term_of_level loc 
             (fun l -> Ast.Layout (Ast.Root (arg l, index l)))
       | "hbox"; LPAREN; p = l1_pattern; RPAREN ->
@@ -588,7 +588,7 @@ EXTEND
     ]
   ];
   explicit_subst: [
-    [ SYMBOL "\\subst";  (* to avoid catching frequent "a [1]" cases *)
+    [ SYMBOL "\\subst ";  (* to avoid catching frequent "a [1]" cases *)
       SYMBOL "[";
       substs = LIST1 [
         i = IDENT; SYMBOL <:unicode<Assign>> (* ≔ *); t = term -> (i, t)