106 OuterSyntax.local_theory "typedecl" "type declaration" K.thy_decl |
106 OuterSyntax.local_theory "typedecl" "type declaration" K.thy_decl |
107 (P.type_args -- P.binding -- P.opt_mixfix |
107 (P.type_args -- P.binding -- P.opt_mixfix |
108 >> (fn ((args, a), mx) => Typedecl.typedecl (a, map (rpair dummyS) args, mx) #> snd)); |
108 >> (fn ((args, a), mx) => Typedecl.typedecl (a, map (rpair dummyS) args, mx) #> snd)); |
109 |
109 |
110 val _ = |
110 val _ = |
111 OuterSyntax.local_theory "type_abbrev" "type abbreviation (input only)" K.thy_decl |
|
112 (P.type_args -- P.binding -- P.opt_mixfix -- (P.$$$ "=" |-- P.!!! P.typ) |
|
113 >> (fn (((args, a), mx), rhs) => Typedecl.abbrev_cmd (a, args, mx) rhs #> snd)); |
|
114 |
|
115 val _ = |
|
116 OuterSyntax.local_theory "types" "declare type abbreviations" K.thy_decl |
111 OuterSyntax.local_theory "types" "declare type abbreviations" K.thy_decl |
117 (Scan.repeat1 |
112 (Scan.repeat1 |
118 (P.type_args -- P.binding -- (P.$$$ "=" |-- P.!!! (P.typ -- P.opt_mixfix'))) |
113 (P.type_args -- P.binding -- (P.$$$ "=" |-- P.!!! (P.typ -- P.opt_mixfix'))) |
119 >> (IsarCmd.add_tyabbrs o map (fn ((args, a), (T, mx)) => (a, args, T, mx)))); |
114 >> (fold (fn ((args, a), (rhs, mx)) => snd o Typedecl.abbrev_cmd (a, args, mx) rhs))); |
120 |
115 |
121 val _ = |
116 val _ = |
122 OuterSyntax.command "nonterminals" "declare types treated as grammar nonterminal symbols" |
117 OuterSyntax.command "nonterminals" "declare types treated as grammar nonterminal symbols" |
123 K.thy_decl (Scan.repeat1 P.binding >> (Toplevel.theory o Sign.add_nonterminals)); |
118 K.thy_decl (Scan.repeat1 P.binding >> (Toplevel.theory o Sign.add_nonterminals)); |
124 |
119 |