1 

     2 theory Antiquotes

     3 imports Main

     4 begin

     5 

     6 

     7 section {* Two Document Antiquotations *}

     8 

     9 text {*

    10 

    11   For writing documents using Isabelle it is often uesful to use

    12   document antiquotations. Below we give the code for such an 

    13   antiquotation that typesets ML-code and also checks whether

    14   the code is actually correct. In this way one can achieve that the

    15   document is always in sync with code.

    16 

    17   Below we introduce the antiquotation @{text "@{ML_checked \"\<dots>\"}"} which

    18   takes a piece of code as argument. We will check this code by sending 

    19   the ML-expression @{text "val _ = \<dots>"} to the ML-compiler (i.e.~the 

    20   function @{ML "ML_Context.eval_in"}). The code for this antiquotation

    21   is as follows:

    22 *}

    23 

    24 ML {*

    25 fun ml_val txt = "val _ = " ^ txt

    26 

    27 fun output_ml ml src ctxt txt =

    28   (ML_Context.eval_in (SOME ctxt) false Position.none (ml txt);

    29   ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt (space_explode "\n" txt))

    30 

    31 val _ = ThyOutput.add_commands

    32  [("ML_checked", ThyOutput.args (Scan.lift Args.name) (output_ml ml_val))]

    33 *}

    34 

    35 text {*

    36   

    37   Note that the parser @{ML "(Scan.lift Args.name)"} parses a string. If the

    38   code is approved by the compiler, the output function 

    39   @{ML "ThyOutput.output_list (fn _ => fn s => Pretty.str s)"}

    40   pretty prints the code. There are a number of options that are observed

    41   when printing the code (for example @{text "[display]"}; for more information

    42   about the options see \rsccite{sec:antiq}).

    43 

    44   Since we

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

    46   information about the line number where an error might have occurred. We 

    47   can improve this code slightly by writing 

    48 

    49 *}

    50 

    51 ML {*

    52 fun output_ml ml src ctxt (txt,pos) =

    53   (ML_Context.eval_in (SOME ctxt) false pos (ml txt);

    54   ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt (space_explode "\n" txt))

    55 

    56 val _ = ThyOutput.add_commands

    57  [("ML_checked", ThyOutput.args 

    58        (Scan.lift (OuterParse.position Args.name)) (output_ml ml_val))]

    59 *}

    60 

    61 text {*

    62   where the antiquotation can also handle position information.

    63 

    64   (FIXME: say something about OuterParse.position)

    65 

    66 *}

    67 

    68 ML {*

    69 

    70 fun ml_pat (rhs, pat) =

    71   let val pat' = implode (map (fn "\\<dots>" => "_" | s => s) (Symbol.explode pat))

    72   in

    73     "val " ^ pat' ^ " = " ^ rhs

    74   end;

    75 

    76 fun add_response_indicator txt =

    77   map (fn s => "> " ^ s) (space_explode "\n" txt)

    78 

    79 fun output_ml_response ml src ctxt ((lhs,pat),pos) = 

    80   (ML_Context.eval_in (SOME ctxt) false pos (ml (lhs,pat));

    81   let val txt = (space_explode "\n" lhs) @ (add_response_indicator pat)

    82   in ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt txt end)

    83 

    84 *}

    85 

    86 

    87 (*

    88 val _ = ThyOutput.add_commands

    89  [("ML_response", 

    90       ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- Args.name))) 

    91       (output_ml_response ml_pat)]

    92 *)

    93 

    94 

    95 ML {*

    96 

    97 let 

    98   val i = 1 + 2

    99 in

   100   i * i

   101 end

   102 

   103 *}

   104 

   105 (*

   106 A test: 

   107 

   108 @{ML_response [display] "true andalso false" "false"} 

   109 

   110 @{ML_response [display]

   111 "let 

   112   val i = 1 + 2

   113 in

   114   i * i

   115 end" "9"}

   116 *)

   117 

   118 

   119 

   120 end

   121   

   122 

   123 

   124