diff options
| author | Hugo Herbelin | 2020-02-11 22:30:36 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-02-11 22:34:04 +0100 |
| commit | 6884867957d1cc361030cffd18d24cb8a231dd10 (patch) | |
| tree | 90edbcd57b1971bdd1237ef065cd7c2123c79892 | |
| parent | cbf5e7e49cfa243b6eac808241894fc504d84e5f (diff) | |
Fixing extra space in "Print Grammar" (i.e. Grammar.Entry.print in Gramlib).
| -rw-r--r-- | gramlib/grammar.ml | 3 | ||||
| -rw-r--r-- | 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 |