isabelle-cookbook: comparison ProgTutorial/First

equal deleted inserted replaced

-:886a7c614ced
+:26d2f91608ed
 @{text "\<verbclose>"}\isanewline
 @{text "> 7"}\smallskip
 \end{graybox}
 \end{isabelle}
-Like normal Isabelle scripts, \isacommand{ML}-commands can be evaluated by
+If you work with ProofGeneral then like normal Isabelle scripts
+\isacommand{ML}-commands can be evaluated by
 using the advance and undo buttons of your Isabelle environment. The code
 inside the \isacommand{ML}-command can also contain value and function
 bindings, for example
 *}
 @{text "@{make_string}"}:
 @{ML_response_fake [display,gray] "writeln (@{make_string} 1)" "\"1\""}
 However, @{text "@{makes_tring}"} 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,
+You can print out error messages with the function @{ML_ind error in Library};
-because any output this function generates will be overwritten as soon as an
+for example:
-error is raised. For printing anything more serious and elaborate, the
-function @{ML_ind tracing in Output} is more appropriate. This function writes all
-output into a separate tracing buffer. For example:
-@{ML_response_fake [display,gray] "tracing \"foo\"" "\"foo\""}
-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
 At command \"ML\"."}
 This function raises the exception @{text ERROR}, which will then
 be displayed by the infrastructure. Note that this exception is meant
 for ``user-level'' error messages seen by the ``end-user''.
 For messages where you want to indicate a genuine program error, then
 use the exception @{text Fail}. Here the infrastructure indicates that this
 is a low-level exception, and also prints the source position of the ML
 raise statement.
-\footnote{\bf FIXME Mention how to work with @{ML_ind debug in Toplevel} and
-@{ML_ind profiling in Toplevel}.}
-*}
-(* FIXME*)
-(*
-ML {* reset Toplevel.debug *}
-ML {* fun dodgy_fun () = (raise TYPE ("",[],[]); 1) *}
-ML {* fun innocent () = dodgy_fun () *}
-ML {* exception_trace (fn () => cterm_of @{theory} (Bound 0)) *}
-ML {* exception_trace (fn () => innocent ()) *}
-ML {* Toplevel.program (fn () => cterm_of @{theory} (Bound 0)) *}
-ML {* Toplevel.program (fn () => innocent ()) *}
-*)
-text {*
-%Kernel exceptions TYPE, TERM, THM also have their place in situations
-%where kernel-like operations are involved.  The printing is similar as for
-%Fail, although there is some special treatment when Toplevel.debug is
-%enabled.
 Most often you want to inspect data of Isabelle's basic data structures,
 namely @{ML_type term}, @{ML_type typ}, @{ML_type cterm}, @{ML_type ctyp}
 and @{ML_type thm}. Isabelle contains elaborate pretty-printing functions,
 which we will explain in more detail in Section \ref{sec:pretty}. For now
 In this case we obtain
 *}
 text {*
 @{ML_response_fake [display, gray]
-"pwriteln (pretty_term
+"let
-(Config.put show_all_types true @{context}) @{term \"(1::nat, x)\"})"
+val show_all_types_ctxt = Config.put show_all_types true @{context}
+in
+pwriteln (pretty_term show_all_types_ctxt @{term \"(1::nat, x)\"})
+end"
 "(Pair::nat \<Rightarrow> 'a \<Rightarrow> nat \<times> 'a) (1::nat) (x::'a)"}
-where @{term Pair} is the term-constructor for products.
+where now even @{term Pair} is written with its type (@{term Pair} is the
-Other configuration values that influence printing of terms are
+term-constructor for products). Other configuration values that influence
-@{ML_ind show_brackets in Syntax} and @{ML_ind show_sorts in Syntax}.
+printing of terms are @{ML_ind show_brackets in Syntax} and @{ML_ind
+show_sorts in Syntax}.
 *}
 text {*
 A @{ML_type cterm} can be printed with the following function.
 *}
 @{ML_response_fake [display, gray]
 "pwriteln (pretty_thm @{context} @{thm conjI})"
 "\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q"}
 However, in order to improve the readability when printing theorems, we
-convert these schematic variables into free variables using the function
+can switch off the question marks as follows:
-@{ML_ind  import in Variable}. This is similar to statements like @{text
+*}
-"conjI[no_vars]"} on Isabelle's user-level.
-*}
+ML{*fun pretty_thm_no_vars ctxt thm =
+let
-ML{*fun no_vars ctxt thm =
+val ctxt' = Config.put show_question_marks false ctxt
-let
-val ((_, [thm']), _) = Variable.import true [thm] ctxt
 in
-thm'
+pretty_term ctxt' (prop_of thm)
-end
+end*}
-fun pretty_thm_no_vars ctxt thm =
-pretty_term ctxt (prop_of (no_vars ctxt thm))*}
 text {*
 With this function, theorem @{thm [source] conjI} is now printed as follows:
 @{ML_response_fake [display, gray]
 @{ML "#>"}.\footnote{give example}
 The remaining combinators we describe in this section add convenience for the
 ``waterfall method'' of writing functions. The combinator @{ML_ind tap in
 Basics} allows you to get hold of an intermediate result (to do some
-side-calculations for instance). The function
+side-calculations or print out an intermediate result, for instance). The function
 *}
 ML %linenosgray{*fun inc_by_three x =
 x |> (fn x => x + 1)
-|> tap (fn x => tracing (PolyML.makestring x))
+|> tap (fn x => writeln (@{make_string} x))
 |> (fn x => x + 2)*}
 text {*
 increments the argument first by @{text "1"} and then by @{text "2"}. In the
 middle (Line 3), however, it uses @{ML tap} for printing the ``plus-one''

changeset 466	26d2f91608ed
parent 462	1d1e795bc3ad
child 467	e11fe0de19a5