# HG changeset patch
# User wenzelm
# Date 1726563971 -7200
# Node ID 68a3defc73d06c2a7429139bb9d0909c8d48b64c
# Parent  59c91b2380344eccb00bf7907462c32845c8a40e
clarified signature;
tuned comments;

diff -r 59c91b238034 -r 68a3defc73d0 src/Pure/Syntax/printer.ML
--- a/src/Pure/Syntax/printer.ML	Tue Sep 17 11:00:03 2024 +0200
+++ b/src/Pure/Syntax/printer.ML	Tue Sep 17 11:06:11 2024 +0200
@@ -70,7 +70,7 @@
   TypArg of int |
   String of bool * string |
   Break of int |
-  Block of Syntax_Ext.block_info * symb list;
+  Block of Syntax_Ext.block * symb list;
 
 type prtabs = (string * ((symb list * int * int) list) Symtab.table) list;
 
diff -r 59c91b238034 -r 68a3defc73d0 src/Pure/Syntax/syntax_ext.ML
--- a/src/Pure/Syntax/syntax_ext.ML	Tue Sep 17 11:00:03 2024 +0200
+++ b/src/Pure/Syntax/syntax_ext.ML	Tue Sep 17 11:06:11 2024 +0200
@@ -1,20 +1,20 @@
 (*  Title:      Pure/Syntax/syntax_ext.ML
-    Author:     Markus Wenzel and Carsten Clasohm, TU Muenchen
+    Author:     Makarius
 
-Syntax extension.
+Syntax extension as internal record.
 *)
 
 signature SYNTAX_EXT =
 sig
   datatype mfix = Mfix of Symbol_Pos.T list * typ * string * int list * int * Position.T
   val typ_to_nonterm: typ -> string
-  type block_info = {markup: Markup.T, consistent: bool, unbreakable: bool, indent: int}
-  val block_indent: int -> block_info
+  type block = {markup: Markup.T, consistent: bool, unbreakable: bool, indent: int}
+  val block_indent: int -> block
   datatype xsymb =
     Delim of string |
     Argument of string * int |
     Space of string |
-    Bg of block_info |
+    Bg of block |
     Brk of int |
     En
   datatype xprod = XProd of string * xsymb list * string * int
@@ -61,16 +61,16 @@
   Space s: some white space for printing
   Bg, Brk, En: blocks and breaks for pretty printing*)
 
-type block_info = {markup: Markup.T, consistent: bool, unbreakable: bool, indent: int};
+type block = {markup: Markup.T, consistent: bool, unbreakable: bool, indent: int};
 
-fun block_indent indent : block_info =
+fun block_indent indent : block =
   {markup = Markup.empty, consistent = false, unbreakable = false, indent = indent};
 
 datatype xsymb =
   Delim of string |
   Argument of string * int |
   Space of string |
-  Bg of block_info |
+  Bg of block |
   Brk of int |
   En;