395 |
395 |
396 and parse_tree s = |
396 and parse_tree s = |
397 parse_basic s --| $$ "," -- parse_tree s >> Br || parse_basic s*} |
397 parse_basic s --| $$ "," -- parse_tree s >> Br || parse_basic s*} |
398 |
398 |
399 text {* |
399 text {* |
400 This parser corrsponds to the grammar: |
400 This parser corresponds to the grammar: |
401 |
401 |
402 \begin{center} |
402 \begin{center} |
403 \begin{tabular}{lcl} |
403 \begin{tabular}{lcl} |
404 @{text "<Basic>"} & @{text "::="} & @{text "<String> | (<Tree>)"}\\ |
404 @{text "<Basic>"} & @{text "::="} & @{text "<String> | (<Tree>)"}\\ |
405 @{text "<Tree>"} & @{text "::="} & @{text "<Basic>, <Tree> | <Basic>"}\\ |
405 @{text "<Tree>"} & @{text "::="} & @{text "<Basic>, <Tree> | <Basic>"}\\ |
938 |
938 |
939 section {* New Commands\label{sec:newcommand} *} |
939 section {* New Commands\label{sec:newcommand} *} |
940 |
940 |
941 text {* |
941 text {* |
942 Often new commands, for example for providing new definitional principles, |
942 Often new commands, for example for providing new definitional principles, |
943 need to be implemented. While this is not difficult on the ML-level and |
943 need to be implemented. While this is not difficult on the ML-level and for |
944 jEdit, in order to be backwards compatible, new commands need also to be recognised |
944 jEdit, in order to be backwards compatible, new commands need also to be recognised |
945 by Proof-General. This results in some subtle configuration issues, which we will |
945 by Proof-General. This results in some subtle configuration issues, which we will |
946 explain in the next section. Here we just describe how to define new commands |
946 explain in the next section. Here we just describe how to define new commands |
947 to work with jEdit. |
947 to work with jEdit. |
948 |
948 |
949 Let us start with a ``silly'' command that does nothing at all. We |
949 Let us start with a ``silly'' command that does nothing at all. We |
950 shall name this command \isacommand{foobar}. Before you can |
950 shall name this command \isacommand{foobar}. Before you can |
951 implement any new command, you have to ``announce'' it in the |
951 implement any new command, you have to ``announce'' it in the |
952 \isacommand{keyword}-section of theory header. For \isacommand{foobar} |
952 \isacommand{keywords}-section of your theory header. For \isacommand{foobar} |
953 we need to write something like |
953 we need to write something like |
954 |
954 |
955 \begin{graybox} |
955 \begin{graybox} |
956 \isacommand{theory}~@{text Foo}\\ |
956 \isacommand{theory}~@{text Foo}\\ |
957 \isacommand{imports}~@{text Main}\\ |
957 \isacommand{imports}~@{text Main}\\ |
959 ... |
959 ... |
960 \end{graybox} |
960 \end{graybox} |
961 |
961 |
962 whereby @{ML_ind "thy_decl" in Keyword} indicates the kind of the |
962 whereby @{ML_ind "thy_decl" in Keyword} indicates the kind of the |
963 command. Another possible kind is @{text "thy_goal"}, or you can |
963 command. Another possible kind is @{text "thy_goal"}, or you can |
964 also to omit the kind entirely, in which case you declare a keyword |
964 also omit the kind entirely, in which case you declare a keyword |
965 (something that is part of a command). |
965 (something that is part of a command). |
966 |
966 |
967 Now you can implement \isacommand{foobar} as follows. |
967 Now you can implement \isacommand{foobar} as follows. |
968 *} |
968 *} |
969 |
969 |