equal
deleted
inserted
replaced
95 (* types *) |
95 (* types *) |
96 |
96 |
97 val typedeclP = |
97 val typedeclP = |
98 OuterSyntax.command "typedecl" "type declaration" K.thy_decl |
98 OuterSyntax.command "typedecl" "type declaration" K.thy_decl |
99 (P.type_args -- P.name -- P.opt_infix >> (fn ((args, a), mx) => |
99 (P.type_args -- P.name -- P.opt_infix >> (fn ((args, a), mx) => |
100 Toplevel.theory (PureThy.add_typedecls [(a, args, mx)]))); |
100 Toplevel.theory (Theory.add_typedecls [(a, args, mx)]))); |
101 |
101 |
102 val typeabbrP = |
102 val typeabbrP = |
103 OuterSyntax.command "types" "declare type abbreviations" K.thy_decl |
103 OuterSyntax.command "types" "declare type abbreviations" K.thy_decl |
104 (Scan.repeat1 |
104 (Scan.repeat1 |
105 (P.type_args -- P.name -- (P.$$$ "=" |-- P.!!! (P.typ -- P.opt_infix'))) |
105 (P.type_args -- P.name -- (P.$$$ "=" |-- P.!!! (P.typ -- P.opt_infix'))) |
219 |
219 |
220 (* name space entry path *) |
220 (* name space entry path *) |
221 |
221 |
222 val globalP = |
222 val globalP = |
223 OuterSyntax.command "global" "disable prefixing of theory name" K.thy_decl |
223 OuterSyntax.command "global" "disable prefixing of theory name" K.thy_decl |
224 (Scan.succeed (Toplevel.theory PureThy.global_path)); |
224 (Scan.succeed (Toplevel.theory Sign.root_path)); |
225 |
225 |
226 val localP = |
226 val localP = |
227 OuterSyntax.command "local" "enable prefixing of theory name" K.thy_decl |
227 OuterSyntax.command "local" "enable prefixing of theory name" K.thy_decl |
228 (Scan.succeed (Toplevel.theory PureThy.local_path)); |
228 (Scan.succeed (Toplevel.theory Sign.local_path)); |
229 |
229 |
230 val hideP = |
230 val hideP = |
231 OuterSyntax.command "hide" "hide names from given name space" K.thy_decl |
231 OuterSyntax.command "hide" "hide names from given name space" K.thy_decl |
232 (P.name -- Scan.repeat1 P.xname >> (Toplevel.theory o IsarThy.hide_names)); |
232 (P.name -- Scan.repeat1 P.xname >> (Toplevel.theory o IsarThy.hide_names)); |
233 |
233 |