432 the function |
432 the function |
433 @{ML [display] "Toplevel.local_theory : string option -> |
433 @{ML [display] "Toplevel.local_theory : string option -> |
434 (local_theory -> local_theory) -> |
434 (local_theory -> local_theory) -> |
435 Toplevel.transition -> Toplevel.transition"} |
435 Toplevel.transition -> Toplevel.transition"} |
436 which, apart from the local theory transformer, takes an optional name of a locale |
436 which, apart from the local theory transformer, takes an optional name of a locale |
437 to be used as a basis for the local theory. The whole parser for our command has type |
437 to be used as a basis for the local theory. |
438 @{ML_type [display] "OuterLex.token list -> |
438 |
|
439 (FIXME : needs to be adjusted to new parser type) |
|
440 |
|
441 {\it |
|
442 The whole parser for our command has type |
|
443 @{ML_text [display] "OuterLex.token list -> |
439 (Toplevel.transition -> Toplevel.transition) * OuterLex.token list"} |
444 (Toplevel.transition -> Toplevel.transition) * OuterLex.token list"} |
440 which is abbreviated by @{ML_type OuterSyntax.parser_fn}. The new command can be added |
445 which is abbreviated by @{ML_text OuterSyntax.parser_fn}. The new command can be added |
441 to the system via the function |
446 to the system via the function |
442 @{ML [display] "OuterSyntax.command : |
447 @{ML_text [display] "OuterSyntax.command : |
443 string -> string -> OuterKeyword.T -> OuterSyntax.parser_fn -> unit"} |
448 string -> string -> OuterKeyword.T -> OuterSyntax.parser_fn -> unit"} |
444 which imperatively updates the parser table behind the scenes. In addition to the parser, this |
449 which imperatively updates the parser table behind the scenes. } |
|
450 |
|
451 In addition to the parser, this |
445 function takes two strings representing the name of the command and a short description, |
452 function takes two strings representing the name of the command and a short description, |
446 as well as an element of type @{ML_type OuterKeyword.T} describing which \emph{kind} of |
453 as well as an element of type @{ML_type OuterKeyword.T} describing which \emph{kind} of |
447 command we intend to add. Since we want to add a command for declaring new concepts, |
454 command we intend to add. Since we want to add a command for declaring new concepts, |
448 we choose the kind @{ML "OuterKeyword.thy_decl"}. Other kinds include |
455 we choose the kind @{ML "OuterKeyword.thy_decl"}. Other kinds include |
449 @{ML "OuterKeyword.thy_goal"}, which is similar to @{ML thy_decl in OuterKeyword}, |
456 @{ML "OuterKeyword.thy_goal"}, which is similar to @{ML thy_decl in OuterKeyword}, |