# HG changeset patch # User wenzelm # Date 1227029155 -3600 # Node ID 1987ef778a025e45e2eea26eba5b6adb34a4f015 # Parent e44fae2b721dafb577ba4e66fe66a9ce97b25ede signed_string_of_int for priorities; tuned; diff -r e44fae2b721d -r 1987ef778a02 src/Pure/Syntax/parser.ML --- a/src/Pure/Syntax/parser.ML Tue Nov 18 18:25:52 2008 +0100 +++ b/src/Pure/Syntax/parser.ML Tue Nov 18 18:25:55 2008 +0100 @@ -397,12 +397,13 @@ fun pretty_symb (Terminal (Token (Literal, s, _))) = Pretty.quote (Pretty.str s) | pretty_symb (Terminal tok) = Pretty.str (str_of_token tok) - | pretty_symb (Nonterminal (tag, p)) = Pretty.str (nt_name tag ^ "[" ^ string_of_int p ^ "]"); + | pretty_symb (Nonterminal (tag, p)) = + Pretty.str (nt_name tag ^ "[" ^ signed_string_of_int p ^ "]"); fun pretty_const "" = [] - | pretty_const c = [Pretty.str ("=> " ^ Library.quote c)]; + | pretty_const c = [Pretty.str ("=> " ^ quote c)]; - fun pretty_pri p = [Pretty.str ("(" ^ string_of_int p ^ ")")]; + fun pretty_pri p = [Pretty.str ("(" ^ signed_string_of_int p ^ ")")]; fun pretty_prod name (symbs, const, pri) = Pretty.block (Pretty.breaks (pretty_name name @