# HG changeset patch # User wenzelm # Date 1728995994 -7200 # Node ID b9d701041add1958db9524ee987f54ffe40de971 # Parent aaf9e7535a1a6d387cc06345bba3db0b132d3310 tuned; diff -r aaf9e7535a1a -r b9d701041add src/Pure/Syntax/syntax_phases.ML --- a/src/Pure/Syntax/syntax_phases.ML Tue Oct 15 14:36:37 2024 +0200 +++ b/src/Pure/Syntax/syntax_phases.ML Tue Oct 15 14:39:54 2024 +0200 @@ -664,6 +664,10 @@ val show_markup = Config.get ctxt show_markup; val show_consts_markup = Config.get ctxt show_consts_markup; + val show_const_types = show_markup andalso show_consts_markup; + val show_var_types = show_types orelse show_markup; + val clean_var_types = show_markup andalso not show_types; + fun constrain_ast clean T ast = let val U = Type_Annotation.print clean T in Ast.Appl [Ast.Constant "_constrain", ast, ast_of_termT ctxt trf (term_of_typ ctxt U)] end; @@ -690,16 +694,12 @@ (case SOME (trf a ctxt (Type_Annotation.smash T) args) handle Match => NONE of SOME t => ast_of t | NONE => - let - val c = - Ast.Constant a - |> (show_markup andalso show_consts_markup) ? constrain_ast {clean = true} T; + let val c = Ast.Constant a |> show_const_types ? constrain_ast {clean = true} T in Ast.mk_appl c (map ast_of args) end) and var_ast v T = simple_ast_of ctxt v - |> (show_types orelse show_markup) ? - constrain_ast {clean = show_markup andalso not show_types} T; + |> show_var_types ? constrain_ast {clean = clean_var_types} T; in term |> mark_aprop