tuned output;
authorwenzelm
Sat Jan 27 16:45:27 2018 +0100 (20 months ago)
changeset 67513731b1ad6759a
parent 67512 166c1659ac75
child 67514 6877af8bc18d
tuned output;
src/Doc/Isar_Ref/Inner_Syntax.thy
src/Pure/Syntax/parser.ML
src/Pure/Syntax/syntax.ML
     1.1 --- a/src/Doc/Isar_Ref/Inner_Syntax.thy	Sat Jan 27 16:37:41 2018 +0100
     1.2 +++ b/src/Doc/Isar_Ref/Inner_Syntax.thy	Sat Jan 27 16:45:27 2018 +0100
     1.3 @@ -850,12 +850,11 @@
     1.4      \<^descr> \<open>lexicon\<close> lists the delimiters of the inner token language; see
     1.5      \secref{sec:inner-lex}.
     1.6  
     1.7 -    \<^descr> \<open>prods\<close> lists the productions of the underlying priority grammar; see
     1.8 -    \secref{sec:priority-grammar}.
     1.9 +    \<^descr> \<open>productions\<close> lists the productions of the underlying priority grammar;
    1.10 +    see \secref{sec:priority-grammar}.
    1.11  
    1.12 -    The nonterminal \<open>A\<^sup>(\<^sup>p\<^sup>)\<close> is rendered in plain text as \<open>A[p]\<close>; delimiters
    1.13 -    are quoted. Many productions have an extra \<open>\<dots> => name\<close>. These names later
    1.14 -    become the heads of parse trees; they also guide the pretty printer.
    1.15 +    Many productions have an extra \<open>\<dots> \<^bold>\<Rightarrow> name\<close>. These names later become the
    1.16 +    heads of parse trees; they also guide the pretty printer.
    1.17  
    1.18      Productions without such parse tree names are called \<^emph>\<open>copy productions\<close>.
    1.19      Their right-hand side must have exactly one nonterminal symbol (or named
    1.20 @@ -866,8 +865,7 @@
    1.21      nonterminal without any delimiters, then it is called a \<^emph>\<open>chain
    1.22      production\<close>. Chain productions act as abbreviations: conceptually, they
    1.23      are removed from the grammar by adding new productions. Priority
    1.24 -    information attached to chain productions is ignored; only the dummy value
    1.25 -    \<open>-1\<close> is displayed.
    1.26 +    information attached to chain productions is ignored.
    1.27  
    1.28      \<^descr> \<open>print modes\<close> lists the alternative print modes provided by this
    1.29      grammar; see \secref{sec:print-modes}.
     2.1 --- a/src/Pure/Syntax/parser.ML	Sat Jan 27 16:37:41 2018 +0100
     2.2 +++ b/src/Pure/Syntax/parser.ML	Sat Jan 27 16:45:27 2018 +0100
     2.3 @@ -402,34 +402,25 @@
     2.4  
     2.5  fun pretty_gram (Gram {tags, prods, chains, ...}) =
     2.6    let
     2.7 -    fun pretty_name name = [Pretty.str (name ^ " =")];
     2.8 -
     2.9 -    val nt_name = the o Inttab.lookup (Inttab.make (map swap (Symtab.dest tags)));
    2.10 +    val print_nt = the o Inttab.lookup (Inttab.make (map swap (Symtab.dest tags)));
    2.11 +    fun print_pri p = if p < 0 then "" else Symbol.make_sup ("(" ^ signed_string_of_int p ^ ")");
    2.12  
    2.13 -    fun pretty_symb (Terminal (Lexicon.Token (Lexicon.Literal, s, _))) = Pretty.quote (Pretty.str s)
    2.14 -      | pretty_symb (Terminal tok) = Pretty.str (Lexicon.str_of_token tok)
    2.15 -      | pretty_symb (Nonterminal (tag, p)) =
    2.16 -          Pretty.str (nt_name tag ^ "[" ^ signed_string_of_int p ^ "]");
    2.17 +    fun pretty_symb (Terminal (Lexicon.Token (kind, s, _))) =
    2.18 +          if kind = Lexicon.Literal then Pretty.quote (Pretty.keyword1 s) else Pretty.str s
    2.19 +      | pretty_symb (Nonterminal (tag, p)) = Pretty.str (print_nt tag ^ print_pri p);
    2.20  
    2.21      fun pretty_const "" = []
    2.22 -      | pretty_const c = [Pretty.str ("=> " ^ quote c)];
    2.23 -
    2.24 -    fun pretty_pri p = [Pretty.str ("(" ^ signed_string_of_int p ^ ")")];
    2.25 +      | pretty_const c = [Pretty.str ("\<^bold>\<Rightarrow> " ^ quote c)];
    2.26  
    2.27 -    fun pretty_prod name (symbs, const, pri) =
    2.28 -      Pretty.block (Pretty.breaks (pretty_name name @
    2.29 -        map pretty_symb symbs @ pretty_const const @ pretty_pri pri));
    2.30 +    fun prod_of_chain from = ([Nonterminal (from, ~1)], "", ~1);
    2.31  
    2.32 -    fun pretty_nt (name, tag) =
    2.33 -      let
    2.34 -        fun prod_of_chain from = ([Nonterminal (from, ~1)], "", ~1);
    2.35 -
    2.36 -        val nt_prods =
    2.37 -          fold (union (op =) o snd) (snd (Vector.sub (prods, tag))) [] @
    2.38 -            map prod_of_chain (these (AList.lookup (op =) chains tag));
    2.39 -      in map (pretty_prod name) nt_prods end;
    2.40 -
    2.41 -  in maps pretty_nt (sort_by fst (Symtab.dest tags)) end;
    2.42 +    fun pretty_prod (name, tag) =
    2.43 +      (fold (union (op =) o #2) (#2 (Vector.sub (prods, tag))) [] @
    2.44 +        map prod_of_chain (these (AList.lookup (op =) chains tag)))
    2.45 +      |> map (fn (symbs, const, p) =>
    2.46 +          Pretty.block (Pretty.breaks
    2.47 +            (Pretty.str (name ^ print_pri p ^ " =") :: map pretty_symb symbs @ pretty_const const)));
    2.48 +  in maps pretty_prod (sort_by #1 (Symtab.dest tags)) end;
    2.49  
    2.50  
    2.51  
     3.1 --- a/src/Pure/Syntax/syntax.ML	Sat Jan 27 16:37:41 2018 +0100
     3.2 +++ b/src/Pure/Syntax/syntax.ML	Sat Jan 27 16:45:27 2018 +0100
     3.3 @@ -573,8 +573,9 @@
     3.4      val {lexicon, prmodes, gram, ...} = tabs;
     3.5      val prmodes' = sort_strings (filter_out (fn s => s = "") prmodes);
     3.6    in
     3.7 -    [pretty_strs_qs "lexicon:" (Scan.dest_lexicon lexicon),
     3.8 -      Pretty.big_list "prods:" (Parser.pretty_gram (Lazy.force gram)),
     3.9 +    [Pretty.block (Pretty.breaks
    3.10 +      (Pretty.str "lexicon:" :: map (Pretty.quote o Pretty.keyword1) (Scan.dest_lexicon lexicon))),
    3.11 +      Pretty.big_list "productions:" (Parser.pretty_gram (Lazy.force gram)),
    3.12        pretty_strs_qs "print modes:" prmodes']
    3.13    end;
    3.14