author | wenzelm |
Tue, 17 Sep 2024 11:14:25 +0200 | |
changeset 80894 | 3e0ca6af6738 |
parent 80893 | 68a3defc73d0 |
child 80895 | 2870315eea9e |
--- a/src/Pure/Syntax/syntax_ext.ML Tue Sep 17 11:06:11 2024 +0200 +++ b/src/Pure/Syntax/syntax_ext.ML Tue Sep 17 11:14:25 2024 +0200 @@ -7,7 +7,6 @@ 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 = {markup: Markup.T, consistent: bool, unbreakable: bool, indent: int} val block_indent: int -> block datatype xsymb =