# 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> \lexicon\ lists the delimiters of the inner token language; see \secref{sec:inner-lex}. - \<^descr> \prods\ lists the productions of the underlying priority grammar; see - \secref{sec:priority-grammar}. + \<^descr> \productions\ lists the productions of the underlying priority grammar; + see \secref{sec:priority-grammar}. - The nonterminal \A\<^sup>(\<^sup>p\<^sup>)\ is rendered in plain text as \A[p]\; delimiters - are quoted. Many productions have an extra \\ => name\. These names later - become the heads of parse trees; they also guide the pretty printer. + Many productions have an extra \\ \<^bold>\ name\. These names later become the + heads of parse trees; they also guide the pretty printer. Productions without such parse tree names are called \<^emph>\copy productions\. 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>\chain production\. 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 - \-1\ is displayed. + information attached to chain productions is ignored. \<^descr> \print modes\ 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>\ " ^ 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;