From 6884867957d1cc361030cffd18d24cb8a231dd10 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 11 Feb 2020 22:30:36 +0100
Subject: Fixing extra space in "Print Grammar" (i.e. Grammar.Entry.print in
 Gramlib).

---
 gramlib/grammar.ml               | 3 ++-
 test-suite/output/Notations4.out | 6 +++---
 2 files changed, 5 insertions(+), 4 deletions(-)

diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml
index ff0b90dcff..e1b9c6b7cb 100644
--- a/gramlib/grammar.ml
+++ b/gramlib/grammar.ml
@@ -831,8 +831,9 @@ let rec print_symbol : type s tr r. formatter -> (s, tr, r) ty_symbol -> unit =
       fprintf ppf "LIST1 %a SEP %a%s" print_symbol1 s print_symbol1 t
         (if osep then " OPT_SEP" else "")
   | Sopt s -> fprintf ppf "OPT %a" print_symbol1 s
-  | Stoken p when L.tok_pattern_strings p <> ("", None) ->
+  | Stoken p ->
      begin match L.tok_pattern_strings p with
+     | "", Some s -> print_str ppf s
      | con, Some prm -> fprintf ppf "%s@ %a" con print_str prm
      | con, None -> fprintf ppf "%s" con end
   | Snterml (e, l) ->
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index 43f88f42a5..f65696e464 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -4,11 +4,11 @@ Entry constr:myconstr is
 [ "6" RIGHTA
   [  ]
 | "5" RIGHTA
-  [ SELF;  "+"; NEXT ]
+  [ SELF; "+"; NEXT ]
 | "4" RIGHTA
-  [ SELF;  "*"; NEXT ]
+  [ SELF; "*"; NEXT ]
 | "3" RIGHTA
-  [  "<"; constr:operconstr LEVEL "10";  ">" ] ]
+  [ "<"; constr:operconstr LEVEL "10"; ">" ] ]
 
 [< b > + < b > * < 2 >]
      : nat
-- 
cgit v1.2.3