diff -r de49d5780f57 -r 74f0a06f751f ProgTutorial/FirstSteps.thy --- a/ProgTutorial/FirstSteps.thy Thu Aug 20 14:19:39 2009 +0200 +++ b/ProgTutorial/FirstSteps.thy Thu Aug 20 22:30:20 2009 +0200 @@ -3,8 +3,6 @@ uses "FirstSteps.ML" begin - - chapter {* First Steps *} text {* @@ -115,7 +113,7 @@ 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 [index] "writeln"}. For example + @{ML_ind "writeln"}. For example @{ML_response_fake [display,gray] "writeln \"any string\"" "\"any string\""} @@ -123,7 +121,7 @@ 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 [index] makestring in PolyML}: + @{ML_ind makestring in PolyML}: @{ML_response_fake [display,gray] "writeln (PolyML.makestring 1)" "\"1\""} @@ -133,7 +131,7 @@ 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 [index] tracing} is more appropriate. This function writes all + function @{ML_ind tracing} is more appropriate. This function writes all output into a separate tracing buffer. For example: @{ML_response_fake [display,gray] "tracing \"foo\"" "\"foo\""} @@ -166,7 +164,7 @@ 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 [index] error}; for + You can print out error messages with the function @{ML_ind error}; for example: @{ML_response_fake [display,gray] "if 0=1 then true else (error \"foo\")" @@ -177,8 +175,8 @@ be displayed by the infrastructure. - (FIXME Mention how to work with @{ML_ind [index] debug in Toplevel} and - @{ML_ind [index] profiling in Toplevel}.) + (FIXME Mention how to work with @{ML_ind debug in Toplevel} and + @{ML_ind profiling in Toplevel}.) *} (* @@ -201,7 +199,7 @@ thm}. Isabelle contains elaborate pretty-printing functions for printing them (see Section \ref{sec:pretty}), but for quick-and-dirty solutions they are a bit unwieldy. One way to transform a term into a string is to use the - function @{ML_ind [index] string_of_term in Syntax} in structure @{ML_struct + function @{ML_ind string_of_term in Syntax} in structure @{ML_struct Syntax}, which we bind for more convenience to the toplevel. *} @@ -216,7 +214,7 @@ This produces 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 [index] writeln} or @{ML_ind [index] tracing}: + using either the function @{ML_ind writeln} or @{ML_ind tracing}: @{ML_response_fake [display,gray] "writeln (string_of_term @{context} @{term \"1::nat\"})" @@ -229,7 +227,7 @@ "\"1\""} If there are more than one @{ML_type term}s to be printed, you can use the - function @{ML_ind [index] commas} to separate them. + function @{ML_ind commas} to separate them. *} ML{*fun string_of_terms ctxt ts = @@ -243,9 +241,9 @@ string_of_term ctxt (term_of ct)*} text {* - In this example the function @{ML_ind [index] term_of} extracts the @{ML_type + In this example the function @{ML_ind term_of} extracts the @{ML_type term} from a @{ML_type cterm}. More than one @{ML_type cterm}s can again be - printed with @{ML_ind [index] commas}. + printed with @{ML_ind commas}. *} ML{*fun string_of_cterms ctxt cts = @@ -253,7 +251,7 @@ text {* The easiest way to get the string of a theorem is to transform it - into a @{ML_type cterm} using the function @{ML_ind [index] crep_thm}. + into a @{ML_type cterm} using the function @{ML_ind crep_thm}. *} ML{*fun string_of_thm ctxt thm = @@ -272,7 +270,7 @@ However, in order to improve the readability when printing theorems, we convert these schematic variables into free variables using the function - @{ML_ind [index] import in Variable}. This is similar to statements like @{text + @{ML_ind import in Variable}. This is similar to statements like @{text "conjI[no_vars]"} from Isabelle's user-level. *} @@ -322,7 +320,7 @@ and second half."} To ease this kind of string manipulations, there are a number - of library functions. For example, the function @{ML_ind [index] cat_lines} + of library functions. For example, the function @{ML_ind cat_lines} concatenates a list of strings and inserts newlines. @{ML_response [display, gray] @@ -342,21 +340,21 @@ comprehension of the code, but after getting familiar with them, they actually ease the understanding and also the programming. - The simplest combinator is @{ML_ind [index] I}, which is just the identity function defined as + The simplest combinator is @{ML_ind I}, which is just the identity function defined as *} ML{*fun I x = x*} -text {* Another simple combinator is @{ML_ind [index] K}, defined as *} +text {* Another simple combinator is @{ML_ind K}, defined as *} ML{*fun K x = fn _ => x*} text {* - @{ML_ind [index] K} ``wraps'' a function around the argument @{text "x"}. However, this + @{ML_ind K} ``wraps'' a function around the argument @{text "x"}. However, this function ignores its argument. As a result, @{ML K} defines a constant function always returning @{text x}. - The next combinator is reverse application, @{ML_ind [index] "|>"}, defined as: + The next combinator is reverse application, @{ML_ind "|>"}, defined as: *} ML{*fun x |> f = f x*} @@ -434,15 +432,15 @@ "P z za zb"} You can read off this behaviour from how @{ML apply_fresh_args} is - coded: in Line 2, the function @{ML_ind [index] fastype_of} calculates the type of the - term; @{ML_ind [index] binder_types} in the next line produces the list of argument + coded: in Line 2, the function @{ML_ind fastype_of} calculates the type of the + term; @{ML_ind binder_types} in the next line produces the list of argument types (in the case above the list @{text "[nat, int, unit]"}); Line 4 pairs up each type with the string @{text "z"}; the - function @{ML_ind [index] variant_frees in Variable} generates for each @{text "z"} a + function @{ML_ind variant_frees in Variable} generates for each @{text "z"} a unique name avoiding the given @{text f}; the list of name-type pairs is turned into a list of variable terms in Line 6, which in the last line is applied - by the function @{ML_ind [index] list_comb} to the term. In this last step we have to - use the function @{ML_ind [index] curry}, because @{ML_ind [index] list_comb} expects the + by the function @{ML_ind list_comb} to the term. In this last step we have to + use the function @{ML_ind curry}, because @{ML_ind list_comb} expects the function and the variables list as a pair. This kind of functions is often needed when constructing terms with fresh variables. The infrastructure helps tremendously to avoid any name clashes. Consider for example: @@ -460,7 +458,7 @@ where the @{text "za"} is correctly avoided. - The combinator @{ML_ind [index] "#>"} is the reverse function composition. It can be + The combinator @{ML_ind "#>"} is the reverse function composition. It can be used to define the following function *} @@ -475,7 +473,7 @@ composition allows you to read the code top-down. The remaining combinators described in this section add convenience for the - ``waterfall method'' of writing functions. The combinator @{ML_ind [index] tap} allows + ``waterfall method'' of writing functions. The combinator @{ML_ind tap} allows you to get hold of an intermediate result (to do some side-calculations for instance). The function @@ -488,13 +486,13 @@ text {* increments the argument first by @{text "1"} and then by @{text "2"}. In the - middle (Line 3), however, it uses @{ML_ind [index] tap} for printing the ``plus-one'' - intermediate result inside the tracing buffer. The function @{ML_ind [index] tap} can + middle (Line 3), however, it uses @{ML_ind tap} for printing the ``plus-one'' + intermediate result inside the tracing buffer. The function @{ML_ind tap} can only be used for side-calculations, because any value that is computed cannot be merged back into the ``main waterfall''. To do this, you can use the next combinator. - The combinator @{ML_ind [index] "`"} (a backtick) is similar to @{ML tap}, but applies a + The combinator @{ML_ind "`"} (a backtick) is similar to @{ML tap}, but applies a function to the value and returns the result together with the value (as a pair). For example the function *} @@ -509,7 +507,7 @@ for x}. After that, the function increments the right-hand component of the pair. So finally the result will be @{ML "(x + 1, x + 1)" for x}. - The combinators @{ML_ind [index] "|>>"} and @{ML_ind [index] "||>"} are defined for + The combinators @{ML_ind "|>>"} and @{ML_ind "||>"} are defined for functions manipulating pairs. The first applies the function to the first component of the pair, defined as *} @@ -556,7 +554,7 @@ conciseness is only small, in more complicated situations the benefit of avoiding @{text "lets"} can be substantial. - With the combinator @{ML_ind [index] "|->"} you can re-combine the elements from a pair. + With the combinator @{ML_ind "|->"} you can re-combine the elements from a pair. This combinator is defined as *} @@ -572,10 +570,10 @@ |-> (fn x => fn y => x + y)*} text {* - The combinator @{ML_ind [index] ||>>} plays a central rôle whenever your task is to update a + The combinator @{ML_ind ||>>} plays a central rôle whenever your task is to update a theory and the update also produces a side-result (for example a theorem). Functions for such tasks return a pair whose second component is the theory and the fist - component is the side-result. Using @{ML_ind [index] ||>>}, you can do conveniently the update + component is the side-result. Using @{ML_ind ||>>}, you can do conveniently the update and also accumulate the side-results. Consider the following simple function. *} @@ -587,7 +585,7 @@ text {* The purpose of Line 2 is to just pair up the argument with a dummy value (since - @{ML_ind [index] "||>>"} operates on pairs). Each of the next three lines just increment + @{ML_ind "||>>"} operates on pairs). Each of the next three lines just increment the value by one, but also nest the intermediate results to the left. For example @{ML_response [display,gray] @@ -604,14 +602,14 @@ *} text {* - Recall that @{ML_ind [index] "|>"} is the reverse function application. Recall also that + Recall that @{ML_ind "|>"} is the reverse function application. Recall also that the related - reverse function composition is @{ML_ind [index] "#>"}. In fact all the combinators - @{ML_ind [index] "|->"}, @{ML_ind [index] "|>>"} , @{ML_ind [index] "||>"} and @{ML_ind [index] + reverse function composition is @{ML_ind "#>"}. In fact all the combinators + @{ML_ind "|->"}, @{ML_ind "|>>"} , @{ML_ind "||>"} and @{ML_ind "||>>"} described above have related combinators for - function composition, namely @{ML_ind [index] "#->"}, @{ML_ind [index] "#>>"}, - @{ML_ind [index] "##>"} and @{ML_ind [index] "##>>"}. - Using @{ML_ind [index] "#->"}, for example, the function @{text double} can also be written as: + function composition, namely @{ML_ind "#->"}, @{ML_ind "#>>"}, + @{ML_ind "##>"} and @{ML_ind "##>>"}. + Using @{ML_ind "#->"}, for example, the function @{text double} can also be written as: *} ML{*val double = @@ -627,7 +625,7 @@ list_comb} that works over pairs to fit with the combinator @{ML "|>"}. Such plumbing is also needed in situations where a functions operate over lists, but one calculates only with a single entity. An example is the function - @{ML_ind [index] check_terms in Syntax}, whose purpose is to type-check a list + @{ML_ind check_terms in Syntax}, whose purpose is to type-check a list of terms. @{ML_response_fake [display, gray] @@ -690,7 +688,7 @@ where @{text "@{theory}"} is an antiquotation that is substituted with the current theory (remember that we assumed we are inside the theory @{text FirstSteps}). The name of this theory can be extracted using - the function @{ML_ind [index] theory_name in Context}. + the function @{ML_ind theory_name in Context}. Note, however, that antiquotations are statically linked, that is their value is determined at ``compile-time'', not ``run-time''. For example the function @@ -738,7 +736,7 @@ end*} text {* - The function @{ML_ind [index] dest_ss in MetaSimplifier} returns a record containing all + The function @{ML_ind dest_ss in MetaSimplifier} returns a record containing all information stored in the simpset, but we are only interested in the names of the simp-rules. Now you can feed in the current simpset into this function. The current simpset can be referred to using the antiquotation @{text "@{simpset}"}. @@ -761,7 +759,7 @@ "name"} An example where a qualified name is needed is the function - @{ML_ind [index] define in LocalTheory}. This function is used below to define + @{ML_ind define in LocalTheory}. This function is used below to define the constant @{term "TrueConj"} as the conjunction @{term "True \ True"}. *} @@ -788,7 +786,7 @@ antiquotation @{text "@{term \}"} can be used to construct terms. A restriction of this antiquotation is that it does not allow you to use schematic variables. If you want to have an antiquotation that does not have - this restriction, you can implement your own using the function @{ML_ind [index] + this restriction, you can implement your own using the function @{ML_ind ML_Antiquote.inline}. The code is as follows. *} @@ -801,7 +799,7 @@ text {* The parser in Line 2 provides us with a context and a string; this string is - transformed into a term using the function @{ML_ind [index] read_term_pattern in + transformed into a term using the function @{ML_ind read_term_pattern in ProofContext} (Line 4); the next two lines print the term so that the ML-system can understand them. An example of this antiquotation is as follows. @@ -845,7 +843,7 @@ (Const (\"HOL.plus_class.plus\", \) $ \ $ \) $ \"} will show the term @{term "(a::nat) + b = c"}, but printed using the internal - representation corresponding to the datatype @{ML_type [index] "term"} defined as follows: + representation corresponding to the datatype @{ML_type "term"} defined as follows: *} ML_val %linenosgray{*datatype term = @@ -1045,7 +1043,7 @@ (Const \ $ (Free (\"Q\",\) $ \)))"} There are a number of handy functions that are frequently used for - constructing terms. One is the function @{ML_ind [index] list_comb}, which takes a term + constructing terms. One is the function @{ML_ind list_comb}, which takes a term and a list of terms as arguments, and produces as output the term list applied to the term. For example @@ -1058,7 +1056,7 @@ end" "Free (\"P\", \"nat\") $ Const (\"True\", \"bool\") $ Const (\"False\", \"bool\")"} - Another handy function is @{ML_ind [index] lambda}, which abstracts a variable + Another handy function is @{ML_ind lambda}, which abstracts a variable in a term. For example @{ML_response_fake [display,gray] @@ -1091,7 +1089,7 @@ of Church-style typing, where variables with the same name still differ, if they have different type. - There is also the function @{ML_ind [index] subst_free} with which terms can be + There is also the function @{ML_ind subst_free} with which terms can be replaced by other terms. For example below, we will replace in @{term "(f::nat \ nat \ nat) 0 x"} the subterm @{term "(f::nat \ nat \ nat) 0"} by @{term y}, and @{term x} by @{term True}. @@ -1118,7 +1116,7 @@ end" "Free (\"x\", \"nat\")"} - Similarly the function @{ML_ind [index] subst_bounds}, replaces lose bound + Similarly the function @{ML_ind subst_bounds}, replaces lose bound variables with terms. To see how this function works, let us implement a function that strips off the outermost quantifiers in a term. *} @@ -1137,7 +1135,7 @@ Const (\"op =\", \) $ Bound 1 $ Bound 0)"} After calling @{ML strip_alls}, you obtain a term with lose bound variables. With - the function @{ML subst_bounds}, you can replace these lose @{ML_ind [index] + the function @{ML subst_bounds}, you can replace these lose @{ML_ind Bound}s with the stripped off variables. @{ML_response_fake [display, gray, linenos] @@ -1156,7 +1154,7 @@ and so on. There are many convenient functions that construct specific HOL-terms. For - example @{ML_ind [index] mk_eq in HOLogic} constructs an equality out of two terms. + example @{ML_ind mk_eq in HOLogic} constructs an equality out of two terms. The types needed in this equality are calculated from the type of the arguments. For example @@ -1270,8 +1268,8 @@ (FIXME: Explain the following better.) Occasionally you have to calculate what the ``base'' name of a given - constant is. For this you can use the function @{ML_ind [index] "Sign.extern_const"} or - @{ML_ind [index] Long_Name.base_name}. For example: + constant is. For this you can use the function @{ML_ind "Sign.extern_const"} or + @{ML_ind Long_Name.base_name}. For example: @{ML_response [display,gray] "Sign.extern_const @{theory} \"List.list.Nil\"" "\"Nil\""} @@ -1293,19 +1291,19 @@ ML{*fun make_fun_type ty1 ty2 = Type ("fun", [ty1, ty2]) *} -text {* This can be equally written with the combinator @{ML_ind [index] "-->"} as: *} +text {* This can be equally written with the combinator @{ML_ind "-->"} as: *} ML{*fun make_fun_type ty1 ty2 = ty1 --> ty2 *} text {* If you want to construct a function type with more than one argument - type, then you can use @{ML_ind [index] "--->"}. + type, then you can use @{ML_ind "--->"}. *} ML{*fun make_fun_types tys ty = tys ---> ty *} text {* - A handy function for manipulating terms is @{ML_ind [index] map_types}: it takes a + A handy function for manipulating terms is @{ML_ind map_types}: it takes a function and applies it to every type in a term. You can, for example, change every @{typ nat} in a term into an @{typ int} using the function: *} @@ -1325,8 +1323,8 @@ $ Free (\"a\", \"int\") $ Const (\"HOL.one_class.one\", \"int\")"} If you want to obtain the list of free type-variables of a term, you - can use the function @{ML_ind [index] add_tfrees in Term} - (similarly @{ML_ind [index] add_tvars in Term} for the schematic type-variables). + can use the function @{ML_ind add_tfrees in Term} + (similarly @{ML_ind add_tvars in Term} for the schematic type-variables). One would expect that such functions take a term as input and return a list of types. But their type is actually @@ -1395,8 +1393,8 @@ You can freely construct and manipulate @{ML_type "term"}s and @{ML_type typ}es, since they are just arbitrary unchecked trees. However, you eventually want to see if a term is well-formed, or type-checks, relative to - a theory. Type-checking is done via the function @{ML_ind [index] cterm_of}, which - converts a @{ML_type [index] term} into a @{ML_type [index] cterm}, a \emph{certified} + a theory. Type-checking is done via the function @{ML_ind cterm_of}, which + converts a @{ML_type term} into a @{ML_type cterm}, a \emph{certified} term. Unlike @{ML_type term}s, which are just trees, @{ML_type "cterm"}s are abstract objects that are guaranteed to be type-correct, and they can only be constructed via ``official interfaces''. @@ -1450,7 +1448,7 @@ Remember Isabelle follows the Church-style typing for terms, i.e., a term contains enough typing information (constants, free variables and abstractions all have typing information) so that it is always clear what the type of a term is. - Given a well-typed term, the function @{ML_ind [index] type_of} returns the + Given a well-typed term, the function @{ML_ind type_of} returns the type of a term. Consider for example: @{ML_response [display,gray] @@ -1465,7 +1463,7 @@ "*** Exception- TYPE (\"type_of: type mismatch in application\" \"} Since the complete traversal might sometimes be too costly and - not necessary, there is the function @{ML_ind [index] fastype_of}, which + not necessary, there is the function @{ML_ind fastype_of}, which also returns the type of a term. @{ML_response [display,gray] @@ -1482,7 +1480,7 @@ Sometimes it is a bit inconvenient to construct a term with complete typing annotations, especially in cases where the typing information is redundant. A short-cut is to use the ``place-holder'' - type @{ML_ind [index] dummyT} and then let type-inference figure out the + type @{ML_ind dummyT} and then let type-inference figure out the complete type. An example is as follows: @{ML_response_fake [display,gray] @@ -1579,7 +1577,7 @@ @{ML_file "Pure/thm.ML"}. \end{readmore} - (FIXME: handy functions working on theorems, like @{ML_ind [index] rulify in ObjectLogic} and so on) + (FIXME: handy functions working on theorems, like @{ML_ind rulify in ObjectLogic} and so on) (FIXME: how to add case-names to goal states - maybe in the next section) @@ -1623,7 +1621,7 @@ This is a fundamental principle in Isabelle. A similar situation occurs for example with declaring constants. The function that declares a - constant on the ML-level is @{ML_ind [index] add_consts_i in Sign}. + constant on the ML-level is @{ML_ind add_consts_i in Sign}. If you write\footnote{Recall that ML-code needs to be enclosed in \isacommand{ML}~@{text "\ \ \"}.} *} @@ -1701,11 +1699,11 @@ ML{*val my_symmetric = Thm.rule_attribute (fn _ => fn thm => thm RS @{thm sym})*} text {* - where the function @{ML_ind [index] rule_attribute in Thm} expects a function taking a + where the function @{ML_ind rule_attribute in Thm} expects a function taking a context (which we ignore in the code above) and a theorem (@{text thm}), and returns another theorem (namely @{text thm} resolved with the theorem - @{thm [source] sym}: @{thm sym[no_vars]}).\footnote{The function @{ML_ind [index] "RS"} - is explained in Section~\ref{sec:simpletacs}.} The function + @{thm [source] sym}: @{thm sym[no_vars]}; the function @{ML_ind "RS"} + is explained in Section~\ref{sec:simpletacs}). The function @{ML rule_attribute in Thm} then returns an attribute. Before we can use the attribute, we need to set it up. This can be done @@ -1741,7 +1739,7 @@ @{text "> "}~@{thm test[my_sym]} \end{isabelle} - An alternative for setting up an attribute is the function @{ML_ind [index] setup in Attrib}. + An alternative for setting up an attribute is the function @{ML_ind setup in Attrib}. So instead of using \isacommand{attribute\_setup}, you can also set up the attribute as follows: *} @@ -1806,10 +1804,10 @@ you get an exception indicating that the theorem @{thm [source] sym} does not resolve with meta-equations. - The purpose of @{ML_ind [index] rule_attribute in Thm} is to directly manipulate theorems. + The purpose of @{ML_ind rule_attribute in Thm} is to directly manipulate theorems. Another usage of theorem attributes is to add and delete theorems from stored data. For example the theorem attribute @{text "[simp]"} adds or deletes a theorem from the - current simpset. For these applications, you can use @{ML_ind [index] declaration_attribute in Thm}. + current simpset. For these applications, you can use @{ML_ind declaration_attribute in Thm}. To illustrate this function, let us introduce a reference containing a list of theorems. *} @@ -1838,9 +1836,9 @@ These functions take a theorem and a context and, for what we are explaining here it is sufficient that they just return the context unchanged. They change however the reference @{ML my_thms}, whereby the function - @{ML_ind [index] add_thm in Thm} adds a theorem if it is not already included in - the list, and @{ML_ind [index] del_thm in Thm} deletes one (both functions use the - predicate @{ML_ind [index] eq_thm_prop in Thm}, which compares theorems according to + @{ML_ind add_thm in Thm} adds a theorem if it is not already included in + the list, and @{ML_ind del_thm in Thm} deletes one (both functions use the + predicate @{ML_ind eq_thm_prop in Thm}, which compares theorems according to their proved propositions modulo alpha-equivalence). You can turn functions @{ML my_thm_add} and @{ML my_thm_del} into @@ -1858,7 +1856,7 @@ "maintaining a list of my_thms - rough test only!" text {* - The parser @{ML_ind [index] add_del in Attrib} is a predefined parser for + The parser @{ML_ind add_del in Attrib} is a predefined parser for adding and deleting lemmas. Now if you prove the next lemma and attach to it the attribute @{text "[my_thms]"} *} @@ -1886,7 +1884,7 @@ "[\"True\", \"Suc (Suc 0) = 2\"]"} The theorem @{thm [source] trueI_2} only appears once, since the - function @{ML_ind [index] add_thm in Thm} tests for duplicates, before extending + function @{ML_ind add_thm in Thm} tests for duplicates, before extending the list. Deletion from the list works as follows: *} @@ -1898,7 +1896,7 @@ "!my_thms" "[\"True\"]"} - We used in this example two functions declared as @{ML_ind [index] declaration_attribute in Thm}, + We used in this example two functions declared as @{ML_ind declaration_attribute in Thm}, but there can be any number of them. We just have to change the parser for reading the arguments accordingly. @@ -2127,7 +2125,7 @@ section {* Storing Theorems\label{sec:storing} (TBD) *} -text {* @{ML_ind [index] add_thms_dynamic in PureThy} *} +text {* @{ML_ind add_thms_dynamic in PureThy} *} local_setup %gray {* LocalTheory.note Thm.theoremK @@ -2173,7 +2171,7 @@ its functions do not operate on @{ML_type string}s, but on instances of the type: - @{ML_type [display, gray, index] "Pretty.T"} + @{ML_type_ind [display, gray] "Pretty.T"} The function @{ML str in Pretty} transforms a (plain) string into such a pretty type. For example @@ -2186,7 +2184,7 @@ occur in case the text wraps over a line, or with how much indentation a text should be printed. However, if you want to actually output the formatted text, you have to transform the pretty type back into a @{ML_type - string}. This can be done with the function @{ML_ind [index] string_of in Pretty}. In what + string}. This can be done with the function @{ML_ind string_of in Pretty}. In what follows we will use the following wrapper function for printing a pretty type: *} @@ -2231,10 +2229,10 @@ However by using pretty types you have the ability to indicate a possible line break for example at each space. You can achieve this with the function - @{ML_ind [index] breaks in Pretty}, which expects a list of pretty types and inserts a + @{ML_ind breaks in Pretty}, which expects a list of pretty types and inserts a possible line break in between every two elements in this list. To print this list of pretty types as a single string, we concatenate them - with the function @{ML_ind [index] blk in Pretty} as follows: + with the function @{ML_ind blk in Pretty} as follows: @{ML_response_fake [display,gray] @@ -2249,7 +2247,7 @@ fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar"} Here the layout of @{ML test_str} is much more pleasing to the - eye. The @{ML "0"} in @{ML_ind [index] blk in Pretty} stands for no indentation + eye. The @{ML "0"} in @{ML_ind blk in Pretty} stands for no indentation of the printed string. You can increase the indentation and obtain @{ML_response_fake [display,gray] @@ -2265,7 +2263,7 @@ where starting from the second line the indent is 3. If you want that every line starts with the same indent, you can use the - function @{ML_ind [index] indent in Pretty} as follows: + function @{ML_ind indent in Pretty} as follows: @{ML_response_fake [display,gray] "let @@ -2280,7 +2278,7 @@ If you want to print out a list of items separated by commas and have the linebreaks handled properly, you can use the function - @{ML_ind [index] commas in Pretty}. For example + @{ML_ind commas in Pretty}. For example @{ML_response_fake [display,gray] "let @@ -2295,7 +2293,7 @@ where @{ML upto} generates a list of integers. You can print out this list as a ``set'', that means enclosed inside @{text [quotes] "{"} and @{text [quotes] "}"}, and separated by commas using the function - @{ML_ind [index] enum in Pretty}. For example + @{ML_ind enum in Pretty}. For example *} text {* @@ -2366,8 +2364,8 @@ text {* In Line 3 we define a function that inserts possible linebreaks in places where a space is. In Lines 4 and 5 we pretty-print the term and its type - using the functions @{ML_ind [index] pretty_term in Syntax} and @{ML_ind [index] - pretty_typ in Syntax}. We also use the function @{ML_ind [index] quote in + using the functions @{ML_ind pretty_term in Syntax} and @{ML_ind + pretty_typ in Syntax}. We also use the function @{ML_ind quote in Pretty} in order to enclose the term and type inside quotation marks. In Line 9 we add a period right after the type without the possibility of a line break, because we do not want that a line break occurs there.