src/Pure/Syntax/type_ext.ML
changeset 24613 bc889c3d55a3
parent 23167 b9bbdf7eab3b
child 24680 0d355aa59e67
equal deleted inserted replaced
24612:d1b315bdb8d7 24613:bc889c3d55a3
   170 
   170 
   171 val bracketsN = "brackets";
   171 val bracketsN = "brackets";
   172 val no_bracketsN = "no_brackets";
   172 val no_bracketsN = "no_brackets";
   173 
   173 
   174 fun no_brackets () =
   174 fun no_brackets () =
   175   find_first (fn mode => mode = bracketsN orelse mode = no_bracketsN) (! print_mode)
   175   find_first (fn mode => mode = bracketsN orelse mode = no_bracketsN)
   176     = SOME no_bracketsN;
   176     (print_mode_value ()) = SOME no_bracketsN;
   177 
   177 
   178 val type_bracketsN = "type_brackets";
   178 val type_bracketsN = "type_brackets";
   179 val no_type_bracketsN = "no_type_brackets";
   179 val no_type_bracketsN = "no_type_brackets";
   180 
   180 
   181 fun no_type_brackets () =
   181 fun no_type_brackets () =
   182   find_first (fn mode => mode = type_bracketsN orelse mode = no_type_bracketsN) (! print_mode)
   182   find_first (fn mode => mode = type_bracketsN orelse mode = no_type_bracketsN)
   183     <> SOME type_bracketsN;
   183     (print_mode_value ()) <> SOME type_bracketsN;
   184 
   184 
   185 
   185 
   186 (* parse ast translations *)
   186 (* parse ast translations *)
   187 
   187 
   188 fun tapp_ast_tr (*"_tapp"*) [ty, f] = Ast.Appl [f, ty]
   188 fun tapp_ast_tr (*"_tapp"*) [ty, f] = Ast.Appl [f, ty]