37   a_piece_of_code"} to the ML-compiler (i.e.~the function @{ML

    37   a_piece_of_code"} to the ML-compiler (i.e.~the function @{ML

    38   "ML_Context.eval_source_in"} in Line 7 below). The complete code of the

    38   "ML_Context.eval_source_in"} in Line 7 below). The complete code of the

    39   document antiquotation is as follows:

    39   document antiquotation is as follows:

    40 

    40 

    41 *}

    41 *}

    46 let

    49 let

    54 

    56 

    55 setup {* ml_checked_setup *}

    57 setup {* ml_checked_setup *}

    56 

    59 

    57 text {*

    60 text {*

    58   The parser @{ML "(Scan.lift Args.name)"} in Line 7 parses a string, in this

    61   The parser @{ML "(Scan.lift Args.name)"} in Line 7 parses a string, in this

    59   case the code, and then calls the function @{ML output_ml}. As mentioned

    62   case the code, and then calls the function @{ML output_ml}. As mentioned

    60   before, the parsed code is sent to the ML-compiler in Line 4 using the

    63   before, the parsed code is sent to the ML-compiler in Line 4 using the

    61   function @{ML ml_val}, which constructs the appropriate ML-expression, and

    64   function @{ML ml_val}, which constructs the appropriate ML-expression, and

    62   using @{ML "eval_in" in ML_Context}, which calls the compiler.  If the code is

    65   using @{ML "eval_in" in ML_Context}, which calls the compiler.  If the code is

    63   ``approved'' by the compiler, then the output function @{ML "output" in

    66   ``approved'' by the compiler, then the output function @{ML "output" in

    65   that the code is a list of (pretty)strings where each string correspond to a

    68   that the code is a list of (pretty)strings where each string correspond to a

    66   line in the output. Therefore the use of @{ML "(space_explode \"\\n\" txt)"

    69   line in the output. Therefore the use of @{ML "(space_explode \"\\n\" txt)"

    67   for txt} which produces such a list according to linebreaks.  There are a

    70   for txt} which produces such a list according to linebreaks.  There are a

    68   number of options for antiquotations that are observed by the function 

    71   number of options for antiquotations that are observed by the function 

    71   Line 7 sets up the new document antiquotation.

    74   Line 7 sets up the new document antiquotation.

    72 

    75 

    73   \begin{readmore}

    76   \begin{readmore}

    74   For more information about options of document antiquotations see \rsccite{sec:antiq}).

    77   For more information about options of document antiquotations see \rsccite{sec:antiq}).

    75   \end{readmore}

    78   \end{readmore}

    76 

    79 

    77   Since we used the argument @{ML "Position.none"}, the compiler cannot give specific 

    80   Since we used the argument @{ML "Position.none"}, the compiler cannot give specific 

    78   information about the line number, in case an error is detected. We 

    81   information about the line number, in case an error is detected. We 

    79   can improve the code above slightly by writing 

    82   can improve the code above slightly by writing 

    80 *}

    83 *}

    83 let

    86 let

    84   val srcpos = {delimited = false, pos = pos, text = ml_val code_txt}

    87   val srcpos = {delimited = false, pos = pos, text = ml_val code_txt}

    85 in

    88 in

    86   (ML_Context.eval_source_in (SOME ctxt) ML_Compiler.flags srcpos;

    89   (ML_Context.eval_source_in (SOME ctxt) ML_Compiler.flags srcpos;

    88 end

    96 end

    89 

    97 

    90 val ml_checked_setup2 = Thy_Output.antiquotation @{binding "ML_checked2"}

    98 val ml_checked_setup2 = Thy_Output.antiquotation @{binding "ML_checked2"}

    91          (Scan.lift (Parse.position Args.name)) output_ml *}

    99          (Scan.lift (Parse.position Args.name)) output_ml *}

    92 

   100 

    93 setup {* ml_checked_setup2 *}

   101 setup {* ml_checked_setup2 *}

    95 text {*

   103 text {*

    96   where in Lines 1 and 2 the positional information is properly treated. The

   104   where in Lines 1 and 2 the positional information is properly treated. The

    97   parser @{ML Parse.position} encodes the positional information in the 

   105   parser @{ML Parse.position} encodes the positional information in the 

    98   result.

   106   result.

    99 

   107 

   100   We can now write @{text "@{ML_checked2 \"2 + 3\"}"} in a document in order to

   108   We can now write @{text "@{ML_checked2 \"2 + 3\"}"} in a document in order to

   102   somebody changes the definition of addition.

   110   somebody changes the definition of addition.

   103 

   111 

   104 

   112 

   105   The second document antiquotation we describe extends the first by a pattern

   113   The second document antiquotation we describe extends the first by a pattern

   106   that specifies what the result of the ML-code should be and checks the

   114   that specifies what the result of the ML-code should be and checks the

   119   must be be replaced by the given pattern. However, we have to remove all

   127   must be be replaced by the given pattern. However, we have to remove all

   120   ellipses from it and replace them by @{text [quotes] "_"}. The following 

   128   ellipses from it and replace them by @{text [quotes] "_"}. The following 

   121   function will do this:

   129   function will do this:

   122 *}

   130 *}

   123 

   131 

   125 let val pat' = 

   137 let val pat' = 

   126          implode (map (fn "\<dots>" => "_" | s => s) (Symbol.explode pat))

   138          implode (map (fn "\<dots>" => "_" | s => s) (Symbol.explode pat))

   127 in 

   139 in 

   129 end*}

   141 end*}

   131 text {* 

   143 text {* 

   132   Next we add a response indicator to the result using:

   144   Next we add a response indicator to the result using:

   133 *}

   145 *}

   134 

   146 

   135 

   147 

   137 

   149 

   138 text {* 

   150 text {* 

   139   The rest of the code of @{text "ML_resp"} is: 

   151   The rest of the code of @{text "ML_resp"} is: 

   140 *}

   152 *}

   141 

   153 

   142 ML %linenosgray{*fun output_ml_resp {context = ctxt, ...} ((code_txt, pat), pos) = 

   169 ML %linenosgray{*fun output_ml_resp {context = ctxt, ...} ((code_txt, pat), pos) = 

   143   (let

   170   (let

   144      val srcpos = {delimited = false, text = ml_pat (code_txt, pat), pos = pos}

   171      val srcpos = {delimited = false, text = ml_pat (code_txt, pat), pos = pos}

   145    in

   172    in

   146      ML_Context.eval_source_in (SOME ctxt) ML_Compiler.flags srcpos 

   173      ML_Context.eval_source_in (SOME ctxt) ML_Compiler.flags srcpos 

   152      Thy_Output.output ctxt (map Pretty.str (code_output @ resp_output)) 

   179      Thy_Output.output ctxt (map Pretty.str (code_output @ resp_output)) 

   153    end)

   180    end)

   154 

   181 

   155 

   182 

   156 val ml_resp_setup = Thy_Output.antiquotation @{binding "ML_resp"} 

   183 val ml_resp_setup = Thy_Output.antiquotation @{binding "ML_resp"} 

   158              output_ml_resp*}

   185              output_ml_resp*}

   164   the compiler (Line~2), the lines about

   192   the compiler (Line~2), the lines about

   165   the output (Lines 4 to 7) and the parser in the setup (Line 11). Now 

   193   the output (Lines 4 to 7) and the parser in the setup (Line 11). Now 

   166   you can write

   194   you can write

   167  

   195  

   168   @{text [display] "@{ML_resp [display] \"true andalso false\" \"false\"}"}

   196   @{text [display] "@{ML_resp [display] \"true andalso false\" \"false\"}"}

   175 

   203 

   176   @{text [display] "@{ML_resp [display] \"let val i = 3 in (i * i, \"foo\") end\" \"(9, \<dots>)\"}"}

   204   @{text [display] "@{ML_resp [display] \"let val i = 3 in (i * i, \"foo\") end\" \"(9, \<dots>)\"}"}

   177   

   205   

   178   to obtain

   206   to obtain

   179 

   207 

   181 

   209 

   182   In both cases, the check by the compiler ensures that code and result

   210   In both cases, the check by the compiler ensures that code and result

   183   match. A limitation of this document antiquotation, however, is that the

   211   match. A limitation of this document antiquotation, however, is that the

   184   pattern can only be given for values that can be constructed. This excludes

   212   pattern can only be given for values that can be constructed. This excludes

   185   values that are abstract datatypes, like @{ML_type thm}s and @{ML_type cterm}s.

   213   values that are abstract datatypes, like @{ML_type thm}s and @{ML_type cterm}s.