# HG changeset patch # User wenzelm # Date 1729100642 -7200 # Node ID 3c262e273ebdc758de48cfe8ac1a5b983a66522a # Parent 6002cb6bfb0ac08076af850291c4435fef935e6f tuned signature; diff -r 6002cb6bfb0a -r 3c262e273ebd src/Pure/Syntax/printer.ML --- a/src/Pure/Syntax/printer.ML Wed Oct 16 16:20:35 2024 +0200 +++ b/src/Pure/Syntax/printer.ML Wed Oct 16 19:44:02 2024 +0200 @@ -69,7 +69,7 @@ datatype symb = Arg of int | - TypArg of int | + Arg_Type of int | String of Markup.T list * string | Break of int | Block of Syntax_Ext.block * symb list; @@ -89,7 +89,7 @@ local fun is_arg (Arg _) = true - | is_arg (TypArg _) = true + | is_arg (Arg_Type _) = true | is_arg _ = false; fun is_space str = forall_string (fn s => s = " ") str; @@ -120,7 +120,7 @@ |> map_filter (fn (symbs, _, p) => (case clean symbs of [Arg p1, String (_, d), Arg p2] => SOME (p1, p2, d, p) - | [TypArg p1, String (_, d), TypArg p2] => SOME (p1, p2, d, p) + | [Arg_Type p1, String (_, d), Arg_Type p2] => SOME (p1, p2, d, p) | _ => NONE)) |> get_first (fn (p1, p2, d, p) => if p1 = p + 1 andalso p2 = p + 1 then SOME {assoc = No_Assoc, delim = d, pri = p} @@ -137,7 +137,7 @@ fun make_literal s = String (Lexicon.literal_markup s, s); fun make_arg (s, p) = - (if s = "type" then TypArg else Arg) + (if s = "type" then Arg_Type else Arg) (if Lexicon.is_terminal s then 1000 else p); fun xprod_to_fmt (Syntax_Ext.XProd (_, _, "", _)) = NONE @@ -156,7 +156,7 @@ | make_symbs [] = ([], []); fun count_args (Arg _ :: syms) = Integer.add 1 #> count_args syms - | count_args (TypArg _ :: syms) = Integer.add 1 #> count_args syms + | count_args (Arg_Type _ :: syms) = Integer.add 1 #> count_args syms | count_args (String _ :: syms) = count_args syms | count_args (Break _ :: syms) = count_args syms | count_args (Block (_, bsyms) :: syms) = count_args syms #> count_args bsyms @@ -294,7 +294,7 @@ | syntax m (Arg p :: symbs, arg :: args) = let val (prts, args') = syntax m (symbs, args); in (main p arg @ prts, args') end - | syntax m (TypArg p :: symbs, arg :: args) = + | 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) =