author  wenzelm 
Thu, 13 Nov 2008 21:56:23 +0100  
changeset 28770  93a372e2dc7a 
parent 28769  8fc228f21861 
child 28771  4510201c6aaf 
permissions  rwrr 
28762  1 
(* $Id$ *) 
2 

3 
theory Inner_Syntax 

4 
imports Main 

5 
begin 

6 

7 
chapter {* Inner syntax  the term language *} 

8 

9 
section {* Printing logical entities *} 

10 

11 
subsection {* Diagnostic commands *} 

12 

13 
text {* 

14 
\begin{matharray}{rcl} 

28766
accab7594b8e
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28765
diff
changeset

15 
@{command_def "typ"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ 
28762  16 
@{command_def "term"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ 
17 
@{command_def "prop"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ 

28766
accab7594b8e
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28765
diff
changeset

18 
@{command_def "thm"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ 
28762  19 
@{command_def "prf"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ 
20 
@{command_def "full_prf"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ 

28766
accab7594b8e
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28765
diff
changeset

21 
@{command_def "pr"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\ 
28762  22 
\end{matharray} 
23 

24 
These diagnostic commands assist interactive development by printing 

25 
internal logical entities in a humanreadable fashion. 

26 

27 
\begin{rail} 

28766
accab7594b8e
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28765
diff
changeset

28 
'typ' modes? type 
28762  29 
; 
30 
'term' modes? term 

31 
; 

32 
'prop' modes? prop 

33 
; 

28766
accab7594b8e
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28765
diff
changeset

34 
'thm' modes? thmrefs 
28762  35 
; 
28766
accab7594b8e
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28765
diff
changeset

36 
( 'prf'  'full\_prf' ) modes? thmrefs? 
28762  37 
; 
28766
accab7594b8e
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28765
diff
changeset

38 
'pr' modes? nat? (',' nat)? 
28762  39 
; 
40 

41 
modes: '(' (name + ) ')' 

42 
; 

43 
\end{rail} 

44 

45 
\begin{description} 

46 

28766
accab7594b8e
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28765
diff
changeset

47 
\item @{command "typ"}~@{text \<tau>} reads and prints types of the 
accab7594b8e
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28765
diff
changeset

48 
metalogic according to the current theory or proof context. 
accab7594b8e
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28765
diff
changeset

49 

accab7594b8e
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28765
diff
changeset

50 
\item @{command "term"}~@{text t} and @{command "prop"}~@{text \<phi>} 
accab7594b8e
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28765
diff
changeset

51 
read, typecheck and print terms or propositions according to the 
accab7594b8e
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28765
diff
changeset

52 
current theory or proof context; the inferred type of @{text t} is 
accab7594b8e
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28765
diff
changeset

53 
output as well. Note that these commands are also useful in 
accab7594b8e
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28765
diff
changeset

54 
inspecting the current environment of term abbreviations. 
28762  55 

56 
\item @{command "thm"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} retrieves 

57 
theorems from the current theory or proof context. Note that any 

58 
attributes included in the theorem specifications are applied to a 

59 
temporary context derived from the current theory or proof; the 

60 
result is discarded, i.e.\ attributes involved in @{text "a\<^sub>1, 

61 
\<dots>, a\<^sub>n"} do not have any permanent effect. 

62 

63 
\item @{command "prf"} displays the (compact) proof term of the 

64 
current proof state (if present), or of the given theorems. Note 

65 
that this requires proof terms to be switched on for the current 

66 
object logic (see the ``Proof terms'' section of the Isabelle 

67 
reference manual for information on how to do this). 

68 

69 
\item @{command "full_prf"} is like @{command "prf"}, but displays 

70 
the full proof term, i.e.\ also displays information omitted in the 

71 
compact proof term, which is denoted by ``@{text _}'' placeholders 

72 
there. 

73 

28766
accab7594b8e
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28765
diff
changeset

74 
\item @{command "pr"}~@{text "goals, prems"} prints the current 
accab7594b8e
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28765
diff
changeset

75 
proof state (if present), including the proof context, current facts 
accab7594b8e
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28765
diff
changeset

76 
and goals. The optional limit arguments affect the number of goals 
accab7594b8e
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28765
diff
changeset

77 
and premises to be displayed, which is initially 10 for both. 
accab7594b8e
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28765
diff
changeset

78 
Omitting limit values leaves the current setting unchanged. 
accab7594b8e
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28765
diff
changeset

79 

28762  80 
\end{description} 
81 

82 
All of the diagnostic commands above admit a list of @{text modes} 

83 
to be specified, which is appended to the current print mode (see 

84 
also \cite{isabelleref}). Thus the output behavior may be modified 

85 
according particular print mode features. For example, @{command 

86 
"pr"}~@{text "(latex xsymbols)"} would print the current proof state 

87 
with mathematical symbols and special characters represented in 

88 
{\LaTeX} source, according to the Isabelle style 

89 
\cite{isabellesys}. 

90 

91 
Note that antiquotations (cf.\ \secref{sec:antiq}) provide a more 

92 
systematic way to include formal items into the printed text 

93 
document. 

94 
*} 

95 

96 

28763
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

97 
subsection {* Details of printed content *} 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

98 

b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

99 
text {* 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

100 
\begin{mldecls} 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

101 
@{index_ML show_types: "bool ref"} & default @{ML false} \\ 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

102 
@{index_ML show_sorts: "bool ref"} & default @{ML false} \\ 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

103 
@{index_ML show_consts: "bool ref"} & default @{ML false} \\ 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

104 
@{index_ML long_names: "bool ref"} & default @{ML false} \\ 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

105 
@{index_ML short_names: "bool ref"} & default @{ML false} \\ 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

106 
@{index_ML unique_names: "bool ref"} & default @{ML true} \\ 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

107 
@{index_ML show_brackets: "bool ref"} & default @{ML false} \\ 
28765
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

108 
@{index_ML eta_contract: "bool ref"} & default @{ML true} \\ 
28763
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

109 
@{index_ML goals_limit: "int ref"} & default @{ML 10} \\ 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

110 
@{index_ML Proof.show_main_goal: "bool ref"} & default @{ML false} \\ 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

111 
@{index_ML show_hyps: "bool ref"} & default @{ML false} \\ 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

112 
@{index_ML show_tags: "bool ref"} & default @{ML false} \\ 
28765
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

113 
@{index_ML show_question_marks: "bool ref"} & default @{ML true} \\ 
28763
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

114 
\end{mldecls} 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

115 

b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

116 
These global ML variables control the detail of information that is 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

117 
displayed for types, terms, theorems, goals etc. 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

118 

28765
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

119 
In interactive sessions, the user interface usually manages these 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

120 
global parameters of the Isabelle process, even with some concept of 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

121 
persistence. Nonetheless it is occasionally useful to manipulate ML 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

122 
variables directly, e.g.\ using @{command "ML_val"} or @{command 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

123 
"ML_command"}. 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

124 

da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

125 
Batchmode logic sessions may be configured by putting appropriate 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

126 
ML text directly into the @{verbatim ROOT.ML} file. 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

127 

28763
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

128 
\begin{description} 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

129 

b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

130 
\item @{ML show_types} and @{ML show_sorts} control printing of type 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

131 
constraints for term variables, and sort constraints for type 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

132 
variables. By default, neither of these are shown in output. If 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

133 
@{ML show_sorts} is set to @{ML true}, types are always shown as 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

134 
well. 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

135 

b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

136 
Note that displaying types and sorts may explain why a polymorphic 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

137 
inference rule fails to resolve with some goal, or why a rewrite 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

138 
rule does not apply as expected. 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

139 

b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

140 
\item @{ML show_consts} controls printing of types of constants when 
28765
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

141 
displaying a goal state. 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

142 

da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

143 
Note that the output can be enormous, because polymorphic constants 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

144 
often occur at several different type instances. 
28763
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

145 

b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

146 
\item @{ML long_names}, @{ML short_names}, and @{ML unique_names} 
28765
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

147 
control the way of printing fully qualified internal names in 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

148 
external form. See also \secref{sec:antiq} for the document 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

149 
antiquotation options of the same names. 
28763
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

150 

28765
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

151 
\item @{ML show_brackets} controls bracketing in pretty printed 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

152 
output. If set to @{ML true}, all subexpressions of the pretty 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

153 
printing tree will be parenthesized, even if this produces malformed 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

154 
term syntax! This crude way of showing the internal structure of 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

155 
pretty printed entities may occasionally help to diagnose problems 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

156 
with operator priorities, for example. 
28763
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

157 

b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

158 
\item @{ML eta_contract} controls @{text "\<eta>"}contracted printing of 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

159 
terms. 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

160 

b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

161 
The @{text \<eta>}contraction law asserts @{prop "(\<lambda>x. f x) \<equiv> f"}, 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

162 
provided @{text x} is not free in @{text f}. It asserts 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

163 
\emph{extensionality} of functions: @{prop "f \<equiv> g"} if @{prop "f x \<equiv> 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

164 
g x"} for all @{text x}. Higherorder unification frequently puts 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

165 
terms into a fully @{text \<eta>}expanded form. For example, if @{text 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

166 
F} has type @{text "(\<tau> \<Rightarrow> \<tau>) \<Rightarrow> \<tau>"} then its expanded form is @{term 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

167 
"\<lambda>h. F (\<lambda>x. h x)"}. 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

168 

b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

169 
Setting @{ML eta_contract} makes Isabelle perform @{text 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

170 
\<eta>}contractions before printing, so that @{term "\<lambda>h. F (\<lambda>x. h x)"} 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

171 
appears simply as @{text F}. 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

172 

b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

173 
Note that the distinction between a term and its @{text \<eta>}expanded 
28765
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

174 
form occasionally matters. While higherorder resolution and 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

175 
rewriting operate modulo @{text "\<alpha>\<beta>\<eta>"}conversion, some other tools 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

176 
might look at terms more discretely. 
28763
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

177 

b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

178 
\item @{ML goals_limit} controls the maximum number of subgoals to 
28765
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

179 
be shown in goal output. 
28763
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

180 

b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

181 
\item @{ML Proof.show_main_goal} controls whether the main result to 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

182 
be proven should be displayed. This information might be relevant 
28765
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

183 
for schematic goals, to inspect the current claim that has been 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

184 
synthesized so far. 
28763
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

185 

b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

186 
\item @{ML show_hyps} controls printing of implicit hypotheses of 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

187 
local facts. Normally, only those hypotheses are displayed that are 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

188 
\emph{not} covered by the assumptions of the current context: this 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

189 
situation indicates a fault in some tool being used. 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

190 

28765
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

191 
By setting @{ML show_hyps} to @{ML true}, output of \emph{all} 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

192 
hypotheses can be enforced, which is occasionally useful for 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

193 
diagnostic purposes. 
28763
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

194 

b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

195 
\item @{ML show_tags} controls printing of extra annotations within 
28765
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

196 
theorems, such as internal position information, or the case names 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

197 
being attached by the attribute @{attribute case_names}. 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

198 

da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

199 
Note that the @{attribute tagged} and @{attribute untagged} 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

200 
attributes provide lowlevel access to the collection of tags 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

201 
associated with a theorem. 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

202 

da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

203 
\item @{ML show_question_marks} controls printing of question marks 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

204 
for schematic variables, such as @{text ?x}. Only the leading 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

205 
question mark is affected, the remaining text is unchanged 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

206 
(including proper markup for schematic variables that might be 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

207 
relevant for user interfaces). 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

208 

da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

209 
\end{description} 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

210 
*} 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

211 

da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

212 

da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

213 
subsection {* Printing limits *} 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

214 

da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

215 
text {* 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

216 
\begin{mldecls} 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

217 
@{index_ML Pretty.setdepth: "int > unit"} \\ 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

218 
@{index_ML Pretty.setmargin: "int > unit"} \\ 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

219 
@{index_ML print_depth: "int > unit"} \\ 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

220 
\end{mldecls} 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

221 

da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

222 
These ML functions set limits for pretty printed text. 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

223 

da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

224 
\begin{description} 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

225 

da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

226 
\item @{ML Pretty.setdepth}~@{text d} tells the pretty printer to 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

227 
limit the printing depth to @{text d}. This affects the display of 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

228 
types, terms, theorems etc. The default value is 0, which permits 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

229 
printing to an arbitrary depth. Other useful values for @{text d} 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

230 
are 10 and 20. 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

231 

da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

232 
\item @{ML Pretty.setmargin}~@{text m} tells the pretty printer to 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

233 
assume a right margin (page width) of @{text m}. The initial margin 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

234 
is 76, but user interfaces might adapt the margin automatically when 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

235 
resizing windows. 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

236 

da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

237 
\item @{ML print_depth}~@{text n} limits the printing depth of the 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

238 
ML toplevel pretty printer; the precise effect depends on the ML 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

239 
compiler and runtime system. Typically @{text n} should be less 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

240 
than 10. Bigger values such as 1001000 are useful for debugging. 
28763
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

241 

b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

242 
\end{description} 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

243 
*} 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

244 

b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

245 

28762  246 
section {* Mixfix annotations *} 
247 

248 
text {* Mixfix annotations specify concrete \emph{inner syntax} of 

28767  249 
Isabelle types and terms. Some commands such as @{command 
250 
"typedecl"} admit infixes only, while @{command "definition"} etc.\ 

251 
support the full range of general mixfixes and binders. Fixed 

252 
parameters in toplevel theorem statements, locale specifications 

253 
also admit mixfix annotations. 

28762  254 

255 
\indexouternonterm{infix}\indexouternonterm{mixfix}\indexouternonterm{structmixfix} 

256 
\begin{rail} 

257 
infix: '(' ('infix'  'infixl'  'infixr') string nat ')' 

258 
; 

259 
mixfix: infix  '(' string prios? nat? ')'  '(' 'binder' string prios? nat ')' 

260 
; 

261 
structmixfix: mixfix  '(' 'structure' ')' 

262 
; 

263 

264 
prios: '[' (nat + ',') ']' 

265 
; 

266 
\end{rail} 

267 

268 
Here the \railtok{string} specifications refer to the actual mixfix 

269 
template, which may include literal text, spacing, blocks, and 

270 
arguments (denoted by ``@{text _}''); the special symbol 

271 
``@{verbatim "\<index>"}'' (printed as ``@{text "\<index>"}'') represents an index 

272 
argument that specifies an implicit structure reference (see also 

273 
\secref{sec:locale}). Infix and binder declarations provide common 

274 
abbreviations for particular mixfix declarations. So in practice, 

275 
mixfix templates mostly degenerate to literal text for concrete 

276 
syntax, such as ``@{verbatim "++"}'' for an infix symbol. 

277 

278 
\medskip In full generality, mixfix declarations work as follows. 

279 
Suppose a constant @{text "c :: \<tau>\<^sub>1 \<Rightarrow> \<dots> \<tau>\<^sub>n \<Rightarrow> \<tau>"} is 

280 
annotated by @{text "(mixfix [p\<^sub>1, \<dots>, p\<^sub>n] p)"}, where @{text 

281 
"mixfix"} is a string @{text "d\<^sub>0 _ d\<^sub>1 _ \<dots> _ d\<^sub>n"} consisting of 

282 
delimiters that surround argument positions as indicated by 

283 
underscores. 

284 

285 
Altogether this determines a production for a contextfree priority 

286 
grammar, where for each argument @{text "i"} the syntactic category 

287 
is determined by @{text "\<tau>\<^sub>i"} (with priority @{text "p\<^sub>i"}), and 

288 
the result category is determined from @{text "\<tau>"} (with 

289 
priority @{text "p"}). Priority specifications are optional, with 

290 
default 0 for arguments and 1000 for the result. 

291 

292 
Since @{text "\<tau>"} may be again a function type, the constant 

293 
type scheme may have more argument positions than the mixfix 

294 
pattern. Printing a nested application @{text "c t\<^sub>1 \<dots> t\<^sub>m"} for 

295 
@{text "m > n"} works by attaching concrete notation only to the 

296 
innermost part, essentially by printing @{text "(c t\<^sub>1 \<dots> t\<^sub>n) \<dots> t\<^sub>m"} 

297 
instead. If a term has fewer arguments than specified in the mixfix 

298 
template, the concrete syntax is ignored. 

299 

300 
\medskip A mixfix template may also contain additional directives 

301 
for pretty printing, notably spaces, blocks, and breaks. The 

302 
general template format is a sequence over any of the following 

303 
entities. 

304 

305 
\begin{itemize} 

306 

307 
\item @{text "\<^bold>d"} is a delimiter, namely a nonempty 

308 
sequence of characters other than the special characters @{text "'"} 

309 
(single quote), @{text "_"} (underscore), @{text "\<index>"} (index 

310 
symbol), @{text "/"} (slash), @{text "("} and @{text ")"} 

311 
(parentheses). 

312 

313 
A single quote escapes the special meaning of these metacharacters, 

314 
producing a literal version of the following character, unless that 

315 
is a blank. A single quote followed by a blank separates 

316 
delimiters, without affecting printing, but input tokens may have 

317 
additional white space here. 

318 

319 
\item @{text "_"} is an argument position, which stands for a 

320 
certain syntactic category in the underlying grammar. 

321 

322 
\item @{text "\<index>"} is an indexed argument position; this is 

323 
the place where implicit structure arguments can be attached. 

324 

325 
\item @{text "\<^bold>s"} is a nonempty sequence of spaces for 

326 
printing. This and the following specifications do not affect 

327 
parsing at all. 

328 

329 
\item @{text "(\<^bold>n"} opens a pretty printing block. The 

330 
optional number specifies how much indentation to add when a line 

331 
break occurs within the block. If the parenthesis is not followed 

332 
by digits, the indentation defaults to 0. A block specified via 

333 
@{text "(00"} is unbreakable. 

334 

335 
\item @{text ")"} closes a pretty printing block. 

336 

337 
\item @{text "//"} forces a line break. 

338 

339 
\item @{text "/\<^bold>s"} allows a line break. Here @{text 

340 
"\<^bold>s"} stands for the string of spaces (zero or more) right 

341 
after the slash. These spaces are printed if the break is 

342 
\emph{not} taken. 

343 

344 
\end{itemize} 

345 

346 
For example, the template @{text "(_ +/ _)"} specifies an infix 

347 
operator. There are two argument positions; the delimiter @{text 

348 
"+"} is preceded by a space and followed by a space or line break; 

349 
the entire phrase is a pretty printing block. 

350 

351 
The general idea of pretty printing with blocks and breaks is also 

352 
described in \cite{paulsonml2}. 

353 
*} 

354 

355 

28766
accab7594b8e
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28765
diff
changeset

356 
section {* Explicit term notation *} 
28762  357 

358 
text {* 

359 
\begin{matharray}{rcll} 

360 
@{command_def "notation"} & : & @{text "local_theory \<rightarrow> local_theory"} \\ 

361 
@{command_def "no_notation"} & : & @{text "local_theory \<rightarrow> local_theory"} \\ 

362 
\end{matharray} 

363 

364 
\begin{rail} 

365 
('notation'  'no\_notation') target? mode? (nameref structmixfix + 'and') 

366 
; 

367 
\end{rail} 

368 

369 
\begin{description} 

370 

371 
\item @{command "notation"}~@{text "c (mx)"} associates mixfix 

372 
syntax with an existing constant or fixed variable. This is a 

373 
robust interface to the underlying @{command "syntax"} primitive 

374 
(\secref{sec:syntrans}). Type declaration and internal syntactic 

375 
representation of the given entity is retrieved from the context. 

376 

377 
\item @{command "no_notation"} is similar to @{command "notation"}, 

378 
but removes the specified syntax annotation from the present 

379 
context. 

380 

381 
\end{description} 

382 
*} 

383 

28769
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

384 
section {* The Pure syntax *} 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

385 

8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

386 
subsection {* Priority grammars *} 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

387 

8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

388 
text {* A contextfree grammar consists of a set of \emph{terminal 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

389 
symbols}, a set of \emph{nonterminal symbols} and a set of 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

390 
\emph{productions}. Productions have the form @{text "A = \<gamma>"}, 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

391 
where @{text A} is a nonterminal and @{text \<gamma>} is a string of 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

392 
terminals and nonterminals. One designated nonterminal is called 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

393 
the \emph{root symbol}. The language defined by the grammar 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

394 
consists of all strings of terminals that can be derived from the 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

395 
root symbol by applying productions as rewrite rules. 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

396 

8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

397 
The standard Isabelle parser for inner syntax uses a \emph{priority 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

398 
grammar}. Each nonterminal is decorated by an integer priority: 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

399 
@{text "A\<^sup>(\<^sup>p\<^sup>)"}. In a derivation, @{text "A\<^sup>(\<^sup>p\<^sup>)"} may be rewritten 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

400 
using a production @{text "A\<^sup>(\<^sup>q\<^sup>) = \<gamma>"} only if @{text "p \<le> q"}. Any 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

401 
priority grammar can be translated into a normal contextfree 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

402 
grammar by introducing new nonterminals and productions. 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

403 

8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

404 
\medskip Formally, a set of context free productions @{text G} 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

405 
induces a derivation relation @{text "\<longrightarrow>\<^sub>G"} as follows. Let @{text 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

406 
\<alpha>} and @{text \<beta>} denote strings of terminal or nonterminal symbols. 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

407 
Then 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

408 
\[ 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

409 
@{text "\<alpha> A\<^sup>(\<^sup>p\<^sup>) \<beta> \<longrightarrow>\<^sub>G \<alpha> \<gamma> \<beta>"} 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

410 
\] 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

411 
if and only if @{text G} contains some production @{text "A\<^sup>(\<^sup>q\<^sup>) = \<gamma>"} 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

412 
for @{text "p \<le> q"}. 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

413 

8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

414 
\medskip The following grammar for arithmetic expressions 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

415 
demonstrates how binding power and associativity of operators can be 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

416 
enforced by priorities. 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

417 

8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

418 
\begin{center} 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

419 
\begin{tabular}{rclr} 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

420 
@{text "A\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)"} & @{text "="} & @{verbatim 0} \\ 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

421 
@{text "A\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)"} & @{text "="} & @{verbatim "("} @{text "A\<^sup>(\<^sup>0\<^sup>)"} @{verbatim ")"} \\ 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

422 
@{text "A\<^sup>(\<^sup>0\<^sup>)"} & @{text "="} & @{text "A\<^sup>(\<^sup>0\<^sup>)"} @{verbatim "+"} @{text "A\<^sup>(\<^sup>1\<^sup>)"} \\ 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

423 
@{text "A\<^sup>(\<^sup>2\<^sup>)"} & @{text "="} & @{text "A\<^sup>(\<^sup>3\<^sup>)"} @{verbatim "*"} @{text "A\<^sup>(\<^sup>2\<^sup>)"} \\ 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

424 
@{text "A\<^sup>(\<^sup>3\<^sup>)"} & @{text "="} & @{verbatim ""} @{text "A\<^sup>(\<^sup>3\<^sup>)"} \\ 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

425 
\end{tabular} 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

426 
\end{center} 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

427 
The choice of priorities determines that @{verbatim ""} binds 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

428 
tighter than @{verbatim "*"}, which binds tighter than @{verbatim 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

429 
"+"}. Furthermore @{verbatim "+"} associates to the left and 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

430 
@{verbatim "*"} to the right. 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

431 

8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

432 
\medskip For clarity, grammars obey these conventions: 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

433 
\begin{itemize} 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

434 

8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

435 
\item All priorities must lie between 0 and 1000. 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

436 

8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

437 
\item Priority 0 on the righthand side and priority 1000 on the 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

438 
lefthand side may be omitted. 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

439 

8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

440 
\item The production @{text "A\<^sup>(\<^sup>p\<^sup>) = \<alpha>"} is written as @{text "A = \<alpha> 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

441 
(p)"}, i.e.\ the priority of the lefthand side actually appears in 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

442 
a column on the far right. 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

443 

8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

444 
\item Alternatives are separated by @{text ""}. 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

445 

8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

446 
\item Repetition is indicated by dots @{text "(\<dots>)"} in an informal 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

447 
but obvious way. 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

448 

8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

449 
\end{itemize} 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

450 

8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

451 
Using these conventions, the example grammar specification above 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

452 
takes the form: 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

453 
\begin{center} 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

454 
\begin{tabular}{rclc} 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

455 
@{text A} & @{text "="} & @{verbatim 0} & \qquad\qquad \\ 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

456 
& @{text ""} & @{verbatim "("} @{text A} @{verbatim ")"} \\ 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

457 
& @{text ""} & @{text A} @{verbatim "+"} @{text "A\<^sup>(\<^sup>1\<^sup>)"} & @{text "(0)"} \\ 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

458 
& @{text ""} & @{text "A\<^sup>(\<^sup>3\<^sup>)"} @{verbatim "*"} @{text "A\<^sup>(\<^sup>2\<^sup>)"} & @{text "(2)"} \\ 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

459 
& @{text ""} & @{verbatim ""} @{text "A\<^sup>(\<^sup>3\<^sup>)"} & @{text "(3)"} \\ 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

460 
\end{tabular} 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

461 
\end{center} 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

462 
*} 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

463 

8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

464 

28770
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

465 
subsection {* The Pure grammar *} 
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

466 

93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

467 
text {* 
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

468 
\begin{figure}[htb]\small 
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

469 
\begin{center} 
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

470 
\begin{tabular}{rclc} 
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

471 

93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

472 
@{text any} & = & @{text "prop  logic"} \\\\ 
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

473 
% FIXME 
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

474 

93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

475 
\end{tabular} 
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

476 
\end{center} 
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

477 
\caption{The Pure grammar}\label{fig:puregrammar} 
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

478 
\end{figure} 
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

479 

93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

480 
The priority grammar of the @{text "Pure"} theory is defined in 
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

481 
\figref{fig:puregrammar}. The following nonterminals are 
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

482 
introduced: 
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

483 

93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

484 
\begin{description} 
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

485 

93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

486 
\item @{text "any"} denotes any term. 
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

487 

93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

488 
\item @{text "prop"} denotes metalevel propositions, which are 
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

489 
terms of type @{typ prop}. The syntax of such formulae of the 
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

490 
metalogic is carefully distinguished from usual conventions for 
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

491 
objectlogics. In particular, plain @{text "\<lambda>"}term 
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

492 
notation is \emph{not} recognized as @{text "prop"}. 
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

493 

93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

494 
\item @{text aprop} denotes atomic propositions, which are embedded 
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

495 
into regular @{typ prop} by means of an explicit @{text "PROP"} 
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

496 
token. 
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

497 

93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

498 
Terms of type @{typ prop} with nonconstant head, e.g.\ a plain 
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

499 
variable, are printed in this form. Constants that yield type @{typ 
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

500 
prop} are expected to provide their own concrete syntax; otherwise 
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

501 
the printed version will appear like @{typ logic} and cannot be 
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

502 
parsed again as @{typ prop}. 
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

503 

93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

504 
\item @{text logic} denotes arbitrary terms of a logical type, 
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

505 
excluding type @{typ prop}. This is the main syntactic category of 
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

506 
objectlogic entities, covering plain @{text \<lambda>}term notation 
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

507 
(variables, abstraction, application), plus anything defined by the 
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

508 
user. 
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

509 

93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

510 
When specifying notation for logical entities, all logical types 
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

511 
(excluding @{typ prop}) are \emph{collapsed} to this single category 
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

512 
of @{typ logic}. 
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

513 

93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

514 
\item @{text idt} denotes identifiers, possibly constrained by 
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

515 
types. 
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

516 

93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

517 
\item @{text idts} denotes a sequence of @{text idt}. This is the 
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

518 
most basic category for variables in iterated binders, such as 
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

519 
@{text "\<lambda>"} or @{text "\<And>"}. 
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

520 

93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

521 
\item @{text pttrn} and @{text pttrns} denote patterns for 
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

522 
abstraction, cases bindings etc. In Pure, these categories start as 
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

523 
a merely copy of @{text idt} and @{text idts}, respectively. 
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

524 
Objectlogics may add additional productions for binding forms. 
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

525 

93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

526 
\item @{text type} denotes types of the metalogic. 
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

527 

93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

528 
\item @{text sort} denotes metalevel sorts. 
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

529 

93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

530 
\end{description} 
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

531 

93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

532 
\begin{warn} 
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

533 
In @{text idts}, note that @{text "x :: nat y"} is parsed as @{text 
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

534 
"x :: (nat y)"}, treating @{text y} like a type constructor applied 
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

535 
to @{text nat}. To avoid this interpretation, write @{text "(x :: 
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

536 
nat) y"} with explicit parentheses. 
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

537 

93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

538 
Similarly, @{text "x :: nat y :: nat"} is parsed as @{text "x :: 
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

539 
(nat y :: nat)"}. The correct form is @{text "(x :: nat) (y :: 
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

540 
nat)"}, or @{text "(x :: nat) y :: nat"} if @{text y} is last in the 
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

541 
sequence of identifiers. 
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

542 
\end{warn} 
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

543 

93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

544 
\begin{warn} 
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

545 
Type constraints for terms bind very weakly. For example, @{text "x 
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

546 
< y :: nat"} is normally parsed as @{text "(x < y) :: nat"}, unless 
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

547 
@{text "<"} has a very low priority, in which case the input is 
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

548 
likely to be ambiguous. The correct form is @{text "x < (y :: nat)"}. 
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

549 
\end{warn} 
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

550 
*} 
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

551 

93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

552 

28762  553 
section {* Syntax and translations \label{sec:syntrans} *} 
554 

555 
text {* 

556 
\begin{matharray}{rcl} 

557 
@{command_def "nonterminals"} & : & @{text "theory \<rightarrow> theory"} \\ 

558 
@{command_def "syntax"} & : & @{text "theory \<rightarrow> theory"} \\ 

559 
@{command_def "no_syntax"} & : & @{text "theory \<rightarrow> theory"} \\ 

560 
@{command_def "translations"} & : & @{text "theory \<rightarrow> theory"} \\ 

561 
@{command_def "no_translations"} & : & @{text "theory \<rightarrow> theory"} \\ 

562 
\end{matharray} 

563 

564 
\begin{rail} 

565 
'nonterminals' (name +) 

566 
; 

567 
('syntax'  'no\_syntax') mode? (constdecl +) 

568 
; 

569 
('translations'  'no\_translations') (transpat ('=='  '=>'  '<='  rightleftharpoons  rightharpoonup  leftharpoondown) transpat +) 

570 
; 

571 

572 
mode: ('(' ( name  'output'  name 'output' ) ')') 

573 
; 

574 
transpat: ('(' nameref ')')? string 

575 
; 

576 
\end{rail} 

577 

578 
\begin{description} 

579 

580 
\item @{command "nonterminals"}~@{text c} declares a type 

581 
constructor @{text c} (without arguments) to act as purely syntactic 

582 
type: a nonterminal symbol of the inner syntax. 

583 

584 
\item @{command "syntax"}~@{text "(mode) decls"} is similar to 

585 
@{command "consts"}~@{text decls}, except that the actual logical 

586 
signature extension is omitted. Thus the context free grammar of 

587 
Isabelle's inner syntax may be augmented in arbitrary ways, 

588 
independently of the logic. The @{text mode} argument refers to the 

589 
print mode that the grammar rules belong; unless the @{keyword_ref 

590 
"output"} indicator is given, all productions are added both to the 

591 
input and output grammar. 

592 

593 
\item @{command "no_syntax"}~@{text "(mode) decls"} removes grammar 

594 
declarations (and translations) resulting from @{text decls}, which 

595 
are interpreted in the same manner as for @{command "syntax"} above. 

596 

597 
\item @{command "translations"}~@{text rules} specifies syntactic 

598 
translation rules (i.e.\ macros): parse~/ print rules (@{text "\<rightleftharpoons>"}), 

599 
parse rules (@{text "\<rightharpoonup>"}), or print rules (@{text "\<leftharpoondown>"}). 

600 
Translation patterns may be prefixed by the syntactic category to be 

601 
used for parsing; the default is @{text logic}. 

602 

603 
\item @{command "no_translations"}~@{text rules} removes syntactic 

604 
translation rules, which are interpreted in the same manner as for 

605 
@{command "translations"} above. 

606 

607 
\end{description} 

608 
*} 

609 

610 

611 
section {* Syntax translation functions *} 

612 

613 
text {* 

614 
\begin{matharray}{rcl} 

615 
@{command_def "parse_ast_translation"} & : & @{text "theory \<rightarrow> theory"} \\ 

616 
@{command_def "parse_translation"} & : & @{text "theory \<rightarrow> theory"} \\ 

617 
@{command_def "print_translation"} & : & @{text "theory \<rightarrow> theory"} \\ 

618 
@{command_def "typed_print_translation"} & : & @{text "theory \<rightarrow> theory"} \\ 

619 
@{command_def "print_ast_translation"} & : & @{text "theory \<rightarrow> theory"} \\ 

620 
\end{matharray} 

621 

622 
\begin{rail} 

623 
( 'parse\_ast\_translation'  'parse\_translation'  'print\_translation'  

624 
'typed\_print\_translation'  'print\_ast\_translation' ) ('(advanced)')? text 

625 
; 

626 
\end{rail} 

627 

628 
Syntax translation functions written in ML admit almost arbitrary 

629 
manipulations of Isabelle's inner syntax. Any of the above commands 

630 
have a single \railqtok{text} argument that refers to an ML 

631 
expression of appropriate type, which are as follows by default: 

632 

633 
%FIXME proper antiquotations 

634 
\begin{ttbox} 

635 
val parse_ast_translation : (string * (ast list > ast)) list 

636 
val parse_translation : (string * (term list > term)) list 

637 
val print_translation : (string * (term list > term)) list 

638 
val typed_print_translation : 

639 
(string * (bool > typ > term list > term)) list 

640 
val print_ast_translation : (string * (ast list > ast)) list 

641 
\end{ttbox} 

642 

643 
If the @{text "(advanced)"} option is given, the corresponding 

644 
translation functions may depend on the current theory or proof 

645 
context. This allows to implement advanced syntax mechanisms, as 

646 
translations functions may refer to specific theory declarations or 

647 
auxiliary proof data. 

648 

649 
See also \cite[\S8]{isabelleref} for more information on the 

650 
general concept of syntax transformations in Isabelle. 

651 

652 
%FIXME proper antiquotations 

653 
\begin{ttbox} 

654 
val parse_ast_translation: 

655 
(string * (Proof.context > ast list > ast)) list 

656 
val parse_translation: 

657 
(string * (Proof.context > term list > term)) list 

658 
val print_translation: 

659 
(string * (Proof.context > term list > term)) list 

660 
val typed_print_translation: 

661 
(string * (Proof.context > bool > typ > term list > term)) list 

662 
val print_ast_translation: 

663 
(string * (Proof.context > ast list > ast)) list 

664 
\end{ttbox} 

665 
*} 

666 

667 
end 