--- a/NEWS Fri Oct 18 19:00:51 2024 +0200
+++ b/NEWS Fri Oct 18 20:48:01 2024 +0200
@@ -46,14 +46,16 @@
hyperlinks work properly e.g. for "['a, 'b] \<Rightarrow> 'c" or "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> C" in
Pure, and "\<forall>x\<in>A. B x" or "\<exists>x\<in>A. B x" in HOL.
-* Inner syntax printing now supports type constraints for constants:
-this is guarded by the configuration options "show_consts_markup"
-(default true) and "show_markup" (default true for PIDE interaction).
-Ast translation rules (command 'translations') and mixfix notation work
-with or without such extra constraints, but ML translation functions
-(command 'print_ast_translation') need may need to be changed slightly.
-Rare INCOMPATIBILITY. The Prover IDE displays type constraints for
-constants as for variables, e.g. via C-mouse hovering.
+* Inner syntax printing now supports type constraints for constants,
+optionally with mixfix syntax (infix, binder etc.). This is guarded by
+the configuration options "show_consts_markup" (default true) and
+"show_markup" (default true for PIDE interaction). The Prover IDE
+displays type constraints as usual via C-mouse hovering. Ast translation
+rules (command 'translations') already work with extra type constraints,
+but the result omits the type of a matched constant. ML translation
+functions (command 'print_ast_translation') based on Ast.unfold_ast etc.
+work in the same manner, but more complex translations may require
+manual changes: rare INCOMPATIBILITY.
* The Simplifier now supports special "congprocs", using keyword
'congproc' or 'weak_congproc' in the 'simproc_setup' command (or ML
--- a/src/Pure/Syntax/printer.ML Fri Oct 18 19:00:51 2024 +0200
+++ b/src/Pure/Syntax/printer.ML Fri Oct 18 20:48:01 2024 +0200
@@ -36,6 +36,7 @@
val merge_prtabs: prtabs * prtabs -> prtabs
val pretty: {type_mode: bool, curried: bool} -> Proof.context -> prtab list ->
(string -> Proof.context -> Ast.ast list -> Ast.ast) ->
+ (Ast.ast -> Pretty.T -> Pretty.T) ->
(string -> Ast.ast list -> Pretty.T option) ->
((string -> Markup.T list) * (string -> string)) ->
Ast.ast -> Pretty.T list
@@ -222,7 +223,7 @@
val type_mode_flags = {type_mode = true, curried = false};
-fun pretty {type_mode, curried} ctxt prtabs trf markup_trans (markup, extern) =
+fun pretty {type_mode, curried} ctxt prtabs trf constrain_output markup_trans (markup, extern) =
let
val show_brackets = Config.get ctxt show_brackets;
@@ -253,7 +254,7 @@
if type_mode then main p ast
else
pretty type_mode_flags (Config.put pretty_priority p ctxt)
- prtabs trf markup_trans (markup, extern) ast
+ prtabs trf constrain_output markup_trans (markup, extern) ast
and combination p c a args constraint =
(case translation p a args of
@@ -261,6 +262,7 @@
| NONE =>
(*find matching table entry, or print as prefix / postfix*)
let
+ val cc = the_default c constraint;
val nargs = length args;
val entry =
prtabs |> get_first (fn prtab =>
@@ -273,10 +275,10 @@
(case Option.mapPartial constrain_trans constraint of
SOME prt => [prt]
| NONE => [Pretty.marks_str (markup a, extern a)])
- else main p (application (the_default c constraint, args))
+ else main p (application (cc, args))
| SOME (symbs, n, q) =>
- if nargs = n then parens p q a (symbs, args)
- else main p (application (split_args n [c] args)))
+ if nargs = n then parens p q a (symbs, args) constraint
+ else main p (application (split_args n [cc] args)))
end)
and translation p a args =
@@ -284,12 +286,16 @@
SOME prt => SOME [prt]
| NONE => Option.map (main p) (SOME (trf a ctxt args) handle Match => NONE))
- and parens p q a (symbs, args) =
+ and parens p q a (symbs, args) constraint =
let
val symbs' =
if p > q orelse (show_brackets andalso q <> 1000 andalso not (is_chain symbs))
then [Block (par_block, par_bg :: symbs @ [par_en])] else symbs;
- in #1 (syntax (markup a) (symbs', args)) end
+ val output =
+ (case constraint of
+ SOME (Ast.Appl [Ast.Constant "_constrain", _, ty]) => constrain_output ty
+ | _ => I);
+ in #1 (syntax (markup a, output) (symbs', args)) end
and syntax _ ([], args) = ([], args)
| syntax m (Arg p :: symbs, arg :: args) =
@@ -298,11 +304,13 @@
| syntax m (Arg_Type p :: symbs, arg :: args) =
let val (prts, args') = syntax m (symbs, args);
in (main_type p arg @ prts, args') end
- | syntax m (String (literal_markup, s) :: symbs, args) =
+ | syntax (m as (ms, output)) (String (literal_markup, s) :: symbs, args) =
let
val (prts, args') = syntax m (symbs, args);
- val m' = if null literal_markup then [] else m @ literal_markup
- in (Pretty.marks_str (m', s) :: prts, args') end
+ val prt =
+ if null literal_markup then Pretty.str s
+ else output (Pretty.marks_str (ms @ literal_markup, s));
+ in (prt :: prts, args') end
| syntax m (Block (block, bsymbs) :: symbs, args) =
let
val (body, args') = syntax m (bsymbs, args);
--- a/src/Pure/Syntax/syntax_phases.ML Fri Oct 18 19:00:51 2024 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML Fri Oct 18 20:48:01 2024 +0200
@@ -806,29 +806,33 @@
then SOME (markup_ast false ty s) else NONE
and pretty_typ_ast m ast = ast
- |> pretty_type_mode ctxt prtabs trf markup_trans markup_extern
+ |> pretty_type_mode ctxt prtabs trf constrain_output markup_trans markup_extern
|> Pretty.markup m
and pretty_ast m ast = ast
- |> prt_t ctxt prtabs trf markup_trans markup_extern
+ |> prt_t ctxt prtabs trf constrain_output markup_trans markup_extern
|> Pretty.markup m
and markup_ast is_typing a A =
- Pretty.make_block (markup_block is_typing A)
- [(if is_typing then pretty_ast else pretty_typ_ast) Markup.empty a]
+ make_block is_typing A
+ ((if is_typing then pretty_ast else pretty_typ_ast) Markup.empty a)
- and markup_block is_typing A =
- let val cache = if is_typing then cache1 else cache2 in
- (case Ast.Table.lookup (! cache) A of
- SOME block => block
- | NONE =>
- let
- val ((bg1, bg2), en) = if is_typing then typing_elem else sorting_elem;
- val B = Pretty.symbolic_output (pretty_typ_ast Markup.empty A);
- val bg = implode (bg1 :: Bytes.contents B @ [bg2]);
- val block = {markup = (bg, en), open_block = false, consistent = false, indent = 0};
- in Unsynchronized.change cache (Ast.Table.update (A, block)); block end)
- end;
+ and make_block is_typing A =
+ let
+ val cache = if is_typing then cache1 else cache2;
+ val block =
+ (case Ast.Table.lookup (! cache) A of
+ SOME block => block
+ | NONE =>
+ let
+ val ((bg1, bg2), en) = if is_typing then typing_elem else sorting_elem;
+ val B = Pretty.symbolic_output (pretty_typ_ast Markup.empty A);
+ val bg = implode (bg1 :: Bytes.contents B @ [bg2]);
+ val block = {markup = (bg, en), open_block = false, consistent = false, indent = 0};
+ in Unsynchronized.change cache (Ast.Table.update (A, block)); block end);
+ in Pretty.make_block block o single end
+
+ and constrain_output A prt = make_block true A prt;
in
t_to_ast ctxt (Syntax.print_translation syn) t
|> Ast.normalize ctxt (Syntax.print_rules syn)