84 |
84 |
85 (* classes and sorts *) |
85 (* classes and sorts *) |
86 |
86 |
87 val _ = |
87 val _ = |
88 OuterSyntax.command "classes" "declare type classes" K.thy_decl |
88 OuterSyntax.command "classes" "declare type classes" K.thy_decl |
89 (Scan.repeat1 (P.name -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- |
89 (Scan.repeat1 (P.binding -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- |
90 P.!!! (P.list1 P.xname)) []) >> (Toplevel.theory o fold AxClass.axiomatize_class_cmd)); |
90 P.!!! (P.list1 P.xname)) []) >> (Toplevel.theory o fold AxClass.axiomatize_class_cmd)); |
91 |
91 |
92 val _ = |
92 val _ = |
93 OuterSyntax.command "classrel" "state inclusion of type classes (axiomatic!)" K.thy_decl |
93 OuterSyntax.command "classrel" "state inclusion of type classes (axiomatic!)" K.thy_decl |
94 (P.and_list1 (P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname)) |
94 (P.and_list1 (P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname)) |
98 OuterSyntax.command "defaultsort" "declare default sort" K.thy_decl |
98 OuterSyntax.command "defaultsort" "declare default sort" K.thy_decl |
99 (P.sort >> (Toplevel.theory o Sign.add_defsort)); |
99 (P.sort >> (Toplevel.theory o Sign.add_defsort)); |
100 |
100 |
101 val _ = |
101 val _ = |
102 OuterSyntax.command "axclass" "define axiomatic type class" K.thy_decl |
102 OuterSyntax.command "axclass" "define axiomatic type class" K.thy_decl |
103 (P.name -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- |
103 (P.binding -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- |
104 P.!!! (P.list1 P.xname)) [] |
104 P.!!! (P.list1 P.xname)) [] |
105 -- Scan.repeat (SpecParse.thm_name ":" -- (P.prop >> single)) |
105 -- Scan.repeat (SpecParse.thm_name ":" -- (P.prop >> single)) |
106 >> (fn (x, y) => Toplevel.theory (snd o Class.axclass_cmd x y))); |
106 >> (fn (x, y) => Toplevel.theory (snd o Class.axclass_cmd x y))); |
107 |
107 |
108 |
108 |
109 (* types *) |
109 (* types *) |
110 |
110 |
111 val _ = |
111 val _ = |
112 OuterSyntax.command "typedecl" "type declaration" K.thy_decl |
112 OuterSyntax.command "typedecl" "type declaration" K.thy_decl |
113 (P.type_args -- P.name -- P.opt_infix >> (fn ((args, a), mx) => |
113 (P.type_args -- P.binding -- P.opt_infix >> (fn ((args, a), mx) => |
114 Toplevel.theory (ObjectLogic.typedecl (a, args, mx) #> snd))); |
114 Toplevel.theory (ObjectLogic.typedecl (a, args, mx) #> snd))); |
115 |
115 |
116 val _ = |
116 val _ = |
117 OuterSyntax.command "types" "declare type abbreviations" K.thy_decl |
117 OuterSyntax.command "types" "declare type abbreviations" K.thy_decl |
118 (Scan.repeat1 |
118 (Scan.repeat1 |
119 (P.type_args -- P.name -- (P.$$$ "=" |-- P.!!! (P.typ -- P.opt_infix'))) |
119 (P.type_args -- P.binding -- (P.$$$ "=" |-- P.!!! (P.typ -- P.opt_infix'))) |
120 >> (Toplevel.theory o Sign.add_tyabbrs o |
120 >> (Toplevel.theory o Sign.add_tyabbrs o |
121 map (fn ((args, a), (T, mx)) => (a, args, T, mx)))); |
121 map (fn ((args, a), (T, mx)) => (a, args, T, mx)))); |
122 |
122 |
123 val _ = |
123 val _ = |
124 OuterSyntax.command "nonterminals" "declare types treated as grammar nonterminal symbols" |
124 OuterSyntax.command "nonterminals" "declare types treated as grammar nonterminal symbols" |
125 K.thy_decl (Scan.repeat1 P.name >> (Toplevel.theory o Sign.add_nonterminals)); |
125 K.thy_decl (Scan.repeat1 P.binding >> (Toplevel.theory o Sign.add_nonterminals)); |
126 |
126 |
127 val _ = |
127 val _ = |
128 OuterSyntax.command "arities" "state type arities (axiomatic!)" K.thy_decl |
128 OuterSyntax.command "arities" "state type arities (axiomatic!)" K.thy_decl |
129 (Scan.repeat1 P.arity >> (Toplevel.theory o fold AxClass.axiomatize_arity_cmd)); |
129 (Scan.repeat1 P.arity >> (Toplevel.theory o fold AxClass.axiomatize_arity_cmd)); |
130 |
130 |
131 |
131 |
132 (* consts and syntax *) |
132 (* consts and syntax *) |
133 |
133 |
134 val _ = |
134 val _ = |
135 OuterSyntax.command "judgment" "declare object-logic judgment" K.thy_decl |
135 OuterSyntax.command "judgment" "declare object-logic judgment" K.thy_decl |
136 (P.const >> (Toplevel.theory o ObjectLogic.add_judgment)); |
136 (P.const_binding >> (Toplevel.theory o ObjectLogic.add_judgment_cmd)); |
137 |
137 |
138 val _ = |
138 val _ = |
139 OuterSyntax.command "consts" "declare constants" K.thy_decl |
139 OuterSyntax.command "consts" "declare constants" K.thy_decl |
140 (Scan.repeat1 P.const >> (Toplevel.theory o Sign.add_consts)); |
140 (Scan.repeat1 P.const_binding >> (Toplevel.theory o Sign.add_consts)); |
141 |
141 |
142 val opt_overloaded = P.opt_keyword "overloaded"; |
142 val opt_overloaded = P.opt_keyword "overloaded"; |
143 |
143 |
144 val _ = |
144 val _ = |
145 OuterSyntax.command "finalconsts" "declare constants as final" K.thy_decl |
145 OuterSyntax.command "finalconsts" "declare constants as final" K.thy_decl |
390 Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 SpecParse.context_element)) [] || |
390 Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 SpecParse.context_element)) [] || |
391 Scan.repeat1 SpecParse.context_element >> pair ([], []); |
391 Scan.repeat1 SpecParse.context_element >> pair ([], []); |
392 |
392 |
393 val _ = |
393 val _ = |
394 OuterSyntax.command "locale" "define named proof context" K.thy_decl |
394 OuterSyntax.command "locale" "define named proof context" K.thy_decl |
395 (P.name -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (([], []), []) -- P.opt_begin |
395 (P.binding -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (([], []), []) -- P.opt_begin |
396 >> (fn ((name, (expr, elems)), begin) => |
396 >> (fn ((name, (expr, elems)), begin) => |
397 (begin ? Toplevel.print) o Toplevel.begin_local_theory begin |
397 (begin ? Toplevel.print) o Toplevel.begin_local_theory begin |
398 (Expression.add_locale_cmd name "" expr elems #> snd))); |
398 (Expression.add_locale_cmd name Binding.empty expr elems #> snd))); |
399 |
399 |
400 val _ = |
400 val _ = |
401 OuterSyntax.command "sublocale" |
401 OuterSyntax.command "sublocale" |
402 "prove sublocale relation between a locale and a locale expression" K.thy_goal |
402 "prove sublocale relation between a locale and a locale expression" K.thy_goal |
403 (P.xname --| (P.$$$ "\\<subseteq>" || P.$$$ "<") -- P.!!! SpecParse.locale_expression |
403 (P.xname --| (P.$$$ "\\<subseteq>" || P.$$$ "<") -- P.!!! SpecParse.locale_expression |
428 Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 SpecParse.context_element)) [] || |
428 Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 SpecParse.context_element)) [] || |
429 Scan.repeat1 SpecParse.context_element >> pair []; |
429 Scan.repeat1 SpecParse.context_element >> pair []; |
430 |
430 |
431 val _ = |
431 val _ = |
432 OuterSyntax.command "class" "define type class" K.thy_decl |
432 OuterSyntax.command "class" "define type class" K.thy_decl |
433 (P.name -- Scan.optional (P.$$$ "=" |-- class_val) ([], []) -- P.opt_begin |
433 (P.binding -- Scan.optional (P.$$$ "=" |-- class_val) ([], []) -- P.opt_begin |
434 >> (fn ((name, (supclasses, elems)), begin) => |
434 >> (fn ((name, (supclasses, elems)), begin) => |
435 (begin ? Toplevel.print) o Toplevel.begin_local_theory begin |
435 (begin ? Toplevel.print) o Toplevel.begin_local_theory begin |
436 (Class.class_cmd name supclasses elems #> snd))); |
436 (Class.class_cmd name supclasses elems #> snd))); |
437 |
437 |
438 val _ = |
438 val _ = |