# HG changeset patch # User wenzelm # Date 1291471024 -3600 # Node ID 95fe8598c0c995c0efb21b1f873f0758d38ef846 # Parent 2dbce761696ab6ac2fc62ca4d9f5b51b7db4658e added Syntax.pretty_priority; diff -r 2dbce761696a -r 95fe8598c0c9 NEWS --- a/NEWS Fri Dec 03 22:40:26 2010 +0100 +++ b/NEWS Sat Dec 04 14:57:04 2010 +0100 @@ -582,6 +582,9 @@ *** ML *** +* Syntax.pretty_priority (default 0) configures the required priority +of pretty-printed output and thus affects insertion of parentheses. + * Former exception Library.UnequalLengths now coincides with ListPair.UnequalLengths. diff -r 2dbce761696a -r 95fe8598c0c9 src/Pure/Syntax/printer.ML --- a/src/Pure/Syntax/printer.ML Fri Dec 03 22:40:26 2010 +0100 +++ b/src/Pure/Syntax/printer.ML Sat Dec 04 14:57:04 2010 +0100 @@ -22,6 +22,7 @@ val show_question_marks_default: bool Unsynchronized.ref val show_question_marks_raw: Config.raw val show_question_marks: bool Config.T + val pretty_priority: int Config.T end; signature PRINTER = @@ -314,7 +315,9 @@ | is_chain [Arg _] = true | is_chain _ = false; -fun pretty extern ctxt tabs trf tokentrf type_mode curried ast0 p0 = +val pretty_priority = Config.int (Config.declare "Syntax.pretty_priority" (K (Config.Int 0))); + +fun pretty extern ctxt tabs trf tokentrf type_mode curried ast0 = let val {extern_class, extern_type, extern_const} = extern; val show_brackets = Config.get ctxt show_brackets; @@ -341,7 +344,9 @@ val (Ts, args') = synT markup (symbs, args); in if type_mode then (astT (t, p) @ Ts, args') - else (pretty extern ctxt tabs trf tokentrf true curried t p @ Ts, args') + else + (pretty extern (Config.put pretty_priority p ctxt) + tabs trf tokentrf true curried t @ Ts, args') end | synT markup (String s :: symbs, args) = let val (Ts, args') = synT markup (symbs, args); @@ -414,21 +419,19 @@ | astT (Ast.Appl ((c as Ast.Constant a) :: (args as _ :: _)), p) = combT (c, a, args, p) | astT (Ast.Appl (f :: (args as _ :: _)), p) = astT (appT (f, args), p) | astT (ast as Ast.Appl _, _) = raise Ast.AST ("pretty: malformed ast", [ast]); - in astT (ast0, p0) end; + in astT (ast0, Config.get ctxt pretty_priority) end; (* pretty_term_ast *) fun pretty_term_ast extern ctxt curried prtabs trf tokentrf ast = - pretty extern ctxt (mode_tabs prtabs (print_mode_value ())) - trf tokentrf false curried ast 0; + pretty extern ctxt (mode_tabs prtabs (print_mode_value ())) trf tokentrf false curried ast; (* pretty_typ_ast *) fun pretty_typ_ast {extern_class, extern_type} ctxt _ prtabs trf tokentrf ast = pretty {extern_class = extern_class, extern_type = extern_type, extern_const = I} - ctxt (mode_tabs prtabs (print_mode_value ())) - trf tokentrf true false ast 0; + ctxt (mode_tabs prtabs (print_mode_value ())) trf tokentrf true false ast; end;