src/Pure/Syntax/type_ext.ML
changeset 19305 5c16895d548b
parent 16614 a493a50e6c0a
child 20854 f9cf9e62d11c
equal deleted inserted replaced
19304:15f001295a7b 19305:5c16895d548b
   138 
   138 
   139 val bracketsN = "brackets";
   139 val bracketsN = "brackets";
   140 val no_bracketsN = "no_brackets";
   140 val no_bracketsN = "no_brackets";
   141 
   141 
   142 fun no_brackets () =
   142 fun no_brackets () =
   143   find_first (equal bracketsN orf equal no_bracketsN) (! print_mode)
   143   find_first (fn mode => mode = bracketsN orelse mode = no_bracketsN) (! print_mode)
   144     = SOME no_bracketsN;
   144     = SOME no_bracketsN;
   145 
   145 
   146 val type_bracketsN = "type_brackets";
   146 val type_bracketsN = "type_brackets";
   147 val no_type_bracketsN = "no_type_brackets";
   147 val no_type_bracketsN = "no_type_brackets";
   148 
   148 
   149 fun no_type_brackets () =
   149 fun no_type_brackets () =
   150   Library.find_first (equal type_bracketsN orf equal no_type_bracketsN) (! print_mode)
   150   find_first (fn mode => mode = type_bracketsN orelse mode = no_type_bracketsN) (! print_mode)
   151     <> SOME type_bracketsN;
   151     <> SOME type_bracketsN;
   152 
   152 
   153 
   153 
   154 (* parse ast translations *)
   154 (* parse ast translations *)
   155 
   155