diff -r 6e2479089226 -r cecd7a941885 ProgTutorial/Recipes/Antiquotes.thy --- a/ProgTutorial/Recipes/Antiquotes.thy Tue May 14 16:59:53 2019 +0200 +++ b/ProgTutorial/Recipes/Antiquotes.thy Tue May 14 17:10:47 2019 +0200 @@ -3,9 +3,9 @@ imports "../Appendix" begin -section {* Useful Document Antiquotations\label{rec:docantiquotations} *} +section \Useful Document Antiquotations\label{rec:docantiquotations}\ -text {* +text \ {\bf Problem:} How to keep your ML-code inside a document synchronised with the actual code?\smallskip @@ -14,11 +14,11 @@ Document antiquotations can be used for ensuring consistent type-setting of various entities in a document. They can also be used for sophisticated \LaTeX-hacking. If you type on the Isabelle level -*} +\ print_antiquotations -text {* +text \ you obtain a list of all currently available document antiquotations and their options. @@ -29,7 +29,7 @@ and also allows you to keep documents in sync with other code, for example Isabelle. - We first describe the antiquotation @{text "ML_checked"} with the syntax: + We first describe the antiquotation \ML_checked\ with the syntax: @{text [display] "@{ML_checked \"a_piece_of_code\"}"} @@ -38,12 +38,12 @@ "ML_Context.eval_source_in"} in Line 7 below). The complete code of the document antiquotation is as follows: -*} +\ ML \Input.pos_of\ -ML%linenosgray{*fun ml_enclose bg en source = - ML_Lex.read bg @ ML_Lex.read_source false source @ ML_Lex.read en;*} +ML%linenosgray\fun ml_enclose bg en source = + ML_Lex.read bg @ ML_Lex.read_source false source @ ML_Lex.read en;\ -ML%linenosgray{*fun ml_val code_txt = (ml_enclose "val _ = " "" code_txt) +ML%linenosgray\fun ml_val code_txt = (ml_enclose "val _ = " "" code_txt) fun output_ml ctxt code_txt = let @@ -52,12 +52,12 @@ Pretty.str (Input.source_content code_txt) end -val ml_checked_setup = Thy_Output.antiquotation_pretty_source @{binding "ML_checked"} (Scan.lift Args.text_input) output_ml*} +val ml_checked_setup = Thy_Output.antiquotation_pretty_source @{binding "ML_checked"} (Scan.lift Args.text_input) output_ml\ -setup {* ml_checked_setup *} +setup \ml_checked_setup\ -text {* +text \ The parser @{ML "(Scan.lift Args.name)"} in Line 7 parses a string, in this case the code, and then calls the function @{ML output_ml}. As mentioned before, the parsed code is sent to the ML-compiler in Line 4 using the @@ -69,8 +69,8 @@ line in the output. Therefore the use of @{ML "(space_explode \"\\n\" txt)" for txt} which produces such a list according to linebreaks. There are a number of options for antiquotations that are observed by the function - @{ML "output" in Document_Antiquotation} when printing the code (including @{text "[display]"} - and @{text "[quotes]"}). The function @{ML "antiquotation_raw" in Thy_Output} in + @{ML "output" in Document_Antiquotation} when printing the code (including \[display]\ + and \[quotes]\). The function @{ML "antiquotation_raw" in Thy_Output} in Line 7 sets up the new document antiquotation. \begin{readmore} @@ -80,7 +80,7 @@ Since we used the argument @{ML "Position.none"}, the compiler cannot give specific information about the line number, in case an error is detected. We can improve the code above slightly by writing -*} +\ (* FIXME: remove ML%linenosgray{*fun output_ml ctxt (code_txt, pos) = let @@ -100,12 +100,12 @@ setup {* ml_checked_setup2 *} *) -text {* +text \ where in Lines 1 and 2 the positional information is properly treated. The parser @{ML Parse.position} encodes the positional information in the result. - We can now write @{text "@{ML_checked2 \"2 + 3\"}"} in a document in order to + We can now write \@{ML_checked2 "2 + 3"}\ in a document in order to obtain @{ML_checked "2 + 3"} and be sure that this code compiles until somebody changes the definition of addition. @@ -119,18 +119,18 @@ @{text [display] "@{ML_resp \"a_piece_of_code\" \"a_pattern\"}"} To add some convenience and also to deal with large outputs, the user can - give a partial specification by using ellipses. For example @{text "(\, \)"} + give a partial specification by using ellipses. For example \(\, \)\ for specifying a pair. In order to check consistency between the pattern and the output of the code, we have to change the ML-expression that is sent - to the compiler: in @{text "ML_checked2"} we sent the expression @{text [quotes] - "val _ = a_piece_of_code"} to the compiler; now the wildcard @{text "_"} + to the compiler: in \ML_checked2\ we sent the expression @{text [quotes] + "val _ = a_piece_of_code"} to the compiler; now the wildcard \_\ must be be replaced by the given pattern. However, we have to remove all ellipses from it and replace them by @{text [quotes] "_"}. The following function will do this: -*} +\ -ML%linenosgray{*fun ml_pat pat code = - ML_Lex.read "val" @ ML_Lex.read_source false pat @ ML_Lex.read " = " @ ML_Lex.read_source false code*} +ML%linenosgray\fun ml_pat pat code = + ML_Lex.read "val" @ ML_Lex.read_source false pat @ ML_Lex.read " = " @ ML_Lex.read_source false code\ (* ML %grayML{*fun ml_pat code_txt pat = @@ -140,16 +140,16 @@ ml_enclose ("val " ^ pat' ^ " = ") "" code_txt end*} *) -text {* +text \ Next we add a response indicator to the result using: -*} +\ -ML %grayML{*fun add_resp pat = map (fn s => "> " ^ s) pat*} +ML %grayML\fun add_resp pat = map (fn s => "> " ^ s) pat\ -text {* - The rest of the code of @{text "ML_resp"} is: -*} +text \ + The rest of the code of \ML_resp\ is: +\ ML %linenosgray\ fun output_ml_resp ctxt (code_txt, pat) = @@ -184,11 +184,11 @@ (Scan.lift (Parse.position (Args.text_input -- Args.text_input))) output_ml_resp*} *) -setup {* ml_response_setup *} +setup \ml_response_setup\ (* FIXME *) -text {* - In comparison with @{text "ML_checked"}, we only changed the line about +text \ + In comparison with \ML_checked\, we only changed the line about the compiler (Line~2), the lines about the output (Lines 4 to 7) and the parser in the setup (Line 11). Now you can write @@ -212,5 +212,5 @@ pattern can only be given for values that can be constructed. This excludes values that are abstract datatypes, like @{ML_type thm}s and @{ML_type cterm}s. -*} +\ end