--- a/src/Doc/Isar_Ref/Inner_Syntax.thy Sat Jan 27 16:37:41 2018 +0100
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy Sat Jan 27 16:45:27 2018 +0100
@@ -850,12 +850,11 @@
\<^descr> \<open>lexicon\<close> lists the delimiters of the inner token language; see
\secref{sec:inner-lex}.
- \<^descr> \<open>prods\<close> lists the productions of the underlying priority grammar; see
- \secref{sec:priority-grammar}.
+ \<^descr> \<open>productions\<close> lists the productions of the underlying priority grammar;
+ see \secref{sec:priority-grammar}.
- The nonterminal \<open>A\<^sup>(\<^sup>p\<^sup>)\<close> is rendered in plain text as \<open>A[p]\<close>; delimiters
- are quoted. Many productions have an extra \<open>\<dots> => name\<close>. These names later
- become the heads of parse trees; they also guide the pretty printer.
+ Many productions have an extra \<open>\<dots> \<^bold>\<Rightarrow> name\<close>. These names later become the
+ heads of parse trees; they also guide the pretty printer.
Productions without such parse tree names are called \<^emph>\<open>copy productions\<close>.
Their right-hand side must have exactly one nonterminal symbol (or named
@@ -866,8 +865,7 @@
nonterminal without any delimiters, then it is called a \<^emph>\<open>chain
production\<close>. Chain productions act as abbreviations: conceptually, they
are removed from the grammar by adding new productions. Priority
- information attached to chain productions is ignored; only the dummy value
- \<open>-1\<close> is displayed.
+ information attached to chain productions is ignored.
\<^descr> \<open>print modes\<close> lists the alternative print modes provided by this
grammar; see \secref{sec:print-modes}.
--- a/src/Pure/Syntax/parser.ML Sat Jan 27 16:37:41 2018 +0100
+++ b/src/Pure/Syntax/parser.ML Sat Jan 27 16:45:27 2018 +0100
@@ -402,34 +402,25 @@
fun pretty_gram (Gram {tags, prods, chains, ...}) =
let
- fun pretty_name name = [Pretty.str (name ^ " =")];
-
- val nt_name = the o Inttab.lookup (Inttab.make (map swap (Symtab.dest tags)));
+ val print_nt = the o Inttab.lookup (Inttab.make (map swap (Symtab.dest tags)));
+ fun print_pri p = if p < 0 then "" else Symbol.make_sup ("(" ^ signed_string_of_int p ^ ")");
- fun pretty_symb (Terminal (Lexicon.Token (Lexicon.Literal, s, _))) = Pretty.quote (Pretty.str s)
- | pretty_symb (Terminal tok) = Pretty.str (Lexicon.str_of_token tok)
- | pretty_symb (Nonterminal (tag, p)) =
- Pretty.str (nt_name tag ^ "[" ^ signed_string_of_int p ^ "]");
+ fun pretty_symb (Terminal (Lexicon.Token (kind, s, _))) =
+ if kind = Lexicon.Literal then Pretty.quote (Pretty.keyword1 s) else Pretty.str s
+ | pretty_symb (Nonterminal (tag, p)) = Pretty.str (print_nt tag ^ print_pri p);
fun pretty_const "" = []
- | pretty_const c = [Pretty.str ("=> " ^ quote c)];
-
- fun pretty_pri p = [Pretty.str ("(" ^ signed_string_of_int p ^ ")")];
+ | pretty_const c = [Pretty.str ("\<^bold>\<Rightarrow> " ^ quote c)];
- fun pretty_prod name (symbs, const, pri) =
- Pretty.block (Pretty.breaks (pretty_name name @
- map pretty_symb symbs @ pretty_const const @ pretty_pri pri));
+ fun prod_of_chain from = ([Nonterminal (from, ~1)], "", ~1);
- fun pretty_nt (name, tag) =
- let
- fun prod_of_chain from = ([Nonterminal (from, ~1)], "", ~1);
-
- val nt_prods =
- fold (union (op =) o snd) (snd (Vector.sub (prods, tag))) [] @
- map prod_of_chain (these (AList.lookup (op =) chains tag));
- in map (pretty_prod name) nt_prods end;
-
- in maps pretty_nt (sort_by fst (Symtab.dest tags)) end;
+ fun pretty_prod (name, tag) =
+ (fold (union (op =) o #2) (#2 (Vector.sub (prods, tag))) [] @
+ map prod_of_chain (these (AList.lookup (op =) chains tag)))
+ |> map (fn (symbs, const, p) =>
+ Pretty.block (Pretty.breaks
+ (Pretty.str (name ^ print_pri p ^ " =") :: map pretty_symb symbs @ pretty_const const)));
+ in maps pretty_prod (sort_by #1 (Symtab.dest tags)) end;
--- a/src/Pure/Syntax/syntax.ML Sat Jan 27 16:37:41 2018 +0100
+++ b/src/Pure/Syntax/syntax.ML Sat Jan 27 16:45:27 2018 +0100
@@ -573,8 +573,9 @@
val {lexicon, prmodes, gram, ...} = tabs;
val prmodes' = sort_strings (filter_out (fn s => s = "") prmodes);
in
- [pretty_strs_qs "lexicon:" (Scan.dest_lexicon lexicon),
- Pretty.big_list "prods:" (Parser.pretty_gram (Lazy.force gram)),
+ [Pretty.block (Pretty.breaks
+ (Pretty.str "lexicon:" :: map (Pretty.quote o Pretty.keyword1) (Scan.dest_lexicon lexicon))),
+ Pretty.big_list "productions:" (Parser.pretty_gram (Lazy.force gram)),
pretty_strs_qs "print modes:" prmodes']
end;