isabelle-cookbook: comparison ProgTutorial/FirstSteps.thy

equal deleted inserted replaced

-:b1a458a03a8e
+:74ba778b09c9
 section {* Printing and Debugging\label{sec:printing} *}
 text {*
 During development you might find it necessary to inspect some data in your
 code. This can be done in a ``quick-and-dirty'' fashion using the function
-@{ML_ind  "writeln"}. For example
+@{ML_ind writeln in Output}. For example
 @{ML_response_eq [display,gray] "writeln \"any string\"" "\"any string\"" with "(op =)"}
 will print out @{text [quotes] "any string"} inside the response buffer of
 Isabelle.  This function expects a string as argument. If you develop under
 PolyML, then there is a convenient, though again ``quick-and-dirty'', method
 for converting values into strings, namely the function
-@{ML_ind  makestring in PolyML}:
+@{ML_ind makestring in PolyML}:
 @{ML_response_eq [display,gray] "writeln (PolyML.makestring 1)" "\"1\"" with "(op =)"}
 However, @{ML makestring in PolyML} only works if the type of what
 is converted is monomorphic and not a function.
 The function @{ML "writeln"} should only be used for testing purposes,
 because any output this function generates will be overwritten as soon as an
 error is raised. For printing anything more serious and elaborate, the
-function @{ML_ind  tracing} is more appropriate. This function writes all
+function @{ML_ind tracing in Output} is more appropriate. This function writes all
 output into a separate tracing buffer. For example:
 @{ML_response_eq [display,gray] "tracing \"foo\"" "\"foo\"" with "(op =)"}
 It is also possible to redirect the ``channel'' where the string @{text
 @{ML [display,gray] "redirect_tracing (TextIO.openOut \"foo.bar\")"}
 will cause that all tracing information is printed into the file @{text "foo.bar"}.
-You can print out error messages with the function @{ML_ind  error}; for
+You can print out error messages with the function @{ML_ind error in Library}; for
 example:
 @{ML_response_fake [display,gray]
 "if 0=1 then true else (error \"foo\")"
 "Exception- ERROR \"foo\" raised
 This function raises the exception @{text ERROR}, which will then
 be displayed by the infrastructure.
-\footnote{\bf FIXME Mention how to work with @{ML_ind  debug in Toplevel} and
+\footnote{\bf FIXME Mention how to work with @{ML_ind debug in Toplevel} and
-@{ML_ind  profiling in Toplevel}.}
+@{ML_ind profiling in Toplevel}.}
 *}
 (* FIXME
 ML {* reset Toplevel.debug *}
 "string_of_term @{context} @{term \"1::nat\"}"
 "\"\\^E\\^Fterm\\^E\\^E\\^Fconst\\^Fname=HOL.one_class.one\\^E1\\^E\\^F\\^E\\^E\\^F\\^E\""}
 We obtain a string corrsponding to the term @{term [show_types] "1::nat"} with some
 additional information encoded in it. The string can be properly printed by
-using either the function @{ML_ind  writeln} or @{ML_ind  tracing}:
+using either the function @{ML  writeln} or @{ML  tracing}:
 @{ML_response_fake [display,gray]
 "writeln (string_of_term @{context} @{term \"1::nat\"})"
 "\"1\""}
 @{ML_response_fake [display,gray]
 "tracing (string_of_term @{context} @{term \"1::nat\"})"
 "\"1\""}
 If there are more than one term to be printed, you can use the
-function @{ML_ind  commas} to separate them.
+function @{ML_ind commas in Library} to separate them.
 *}
 ML{*fun string_of_terms ctxt ts =
 commas (map (string_of_term ctxt) ts)*}
 ML{*fun string_of_cterm ctxt ct =
 string_of_term ctxt (term_of ct)*}
 text {*
-In this example the function @{ML_ind term_of} extracts the @{ML_type
+In this example the function @{ML_ind term_of in Thm} extracts the @{ML_type
 term} from a @{ML_type cterm}.  More than one @{ML_type cterm}s can again be
-printed with @{ML_ind commas}.
+printed with @{ML commas}.
 *}
 ML{*fun string_of_cterms ctxt cts =
 commas (map (string_of_cterm ctxt) cts)*}
 text {*
 The easiest way to get the string of a theorem is to transform it
-into a @{ML_type term} using the function @{ML_ind prop_of}.
+into a @{ML_type term} using the function @{ML_ind prop_of in Thm}.
 *}
 ML{*fun string_of_thm ctxt thm =
 string_of_term ctxt (prop_of thm)*}
 "tracing (\"First half,\" ^ \"\\n\" ^ \"and second half.\")"
 "First half,
 and second half."}
 To ease this kind of string manipulations, there are a number
-of library functions. For example,  the function @{ML_ind  cat_lines}
+of library functions. For example,  the function @{ML_ind cat_lines in Library}
 concatenates a list of strings and inserts newlines.
 @{ML_response [display, gray]
 "cat_lines [\"foo\", \"bar\"]"
 "\"foo\\nbar\""}
 defined on the logical level of Isabelle. By this we mean definitions,
 theorems, terms and so on. This kind of reference is realised in Isabelle
 with ML-antiquotations, often just called antiquotations.\footnote{There are
 two kinds of antiquotations in Isabelle, which have very different purposes
 and infrastructures. The first kind, described in this section, are
-\emph{\index*{ML-antiquotations}}. They are used to refer to entities (like terms,
+\emph{\index*{ML-antiquotation}}. They are used to refer to entities (like terms,
 types etc) from Isabelle's logic layer inside ML-code. The other kind of
-antiquotations are \emph{document}\index{document antiquotationa} antiquotations.
+antiquotations are \emph{document}\index{document antiquotation} antiquotations.
 They are used only in the
 text parts of Isabelle and their purpose is to print logical entities inside
 \LaTeX-documents. Document antiquotations are part of the user level and
 therefore we are not interested in them in this Tutorial, except in Appendix
 \ref{rec:docantiquotations} where we show how to implement your own document

changeset 369	74ba778b09c9
parent 361	8ba963a3e039
child 370	2494b5b7a85d