# HG changeset patch
# User wenzelm
# Date 1517067927 -3600
# Node ID 731b1ad6759a6090c999a7946afb4a07e35cd9f8
# Parent  166c1659ac75a49c67859c0c1205d95a6420e692
tuned output;

diff -r 166c1659ac75 -r 731b1ad6759a src/Doc/Isar_Ref/Inner_Syntax.thy
--- 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}.
diff -r 166c1659ac75 -r 731b1ad6759a src/Pure/Syntax/parser.ML
--- 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;
 
 
 
diff -r 166c1659ac75 -r 731b1ad6759a src/Pure/Syntax/syntax.ML
--- 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;