113 text {*

   113 text {*

   114   During development you might find it necessary to inspect some data in your

   114   During development you might find it necessary to inspect some data in your

   115   code. This can be done in a ``quick-and-dirty'' fashion using the function

   115   code. This can be done in a ``quick-and-dirty'' fashion using the function

   116   @{ML_ind  "writeln"}. For example

   116   @{ML_ind  "writeln"}. For example

   117 

   117 

   119 

   119 

   120   will print out @{text [quotes] "any string"} inside the response buffer of

   120   will print out @{text [quotes] "any string"} inside the response buffer of

   121   Isabelle.  This function expects a string as argument. If you develop under

   121   Isabelle.  This function expects a string as argument. If you develop under

   122   PolyML, then there is a convenient, though again ``quick-and-dirty'', method

   122   PolyML, then there is a convenient, though again ``quick-and-dirty'', method

   123   for converting values into strings, namely the function 

   123   for converting values into strings, namely the function 

   124   @{ML_ind  makestring in PolyML}:

   124   @{ML_ind  makestring in PolyML}:

   125 

   125 

   127 

   127 

   128   However, @{ML makestring in PolyML} only works if the type of what

   128   However, @{ML makestring in PolyML} only works if the type of what

   129   is converted is monomorphic and not a function.

   129   is converted is monomorphic and not a function.

   130 

   130 

   131   The function @{ML "writeln"} should only be used for testing purposes,

   131   The function @{ML "writeln"} should only be used for testing purposes,

   132   because any output this function generates will be overwritten as soon as an

   132   because any output this function generates will be overwritten as soon as an

   133   error is raised. For printing anything more serious and elaborate, the

   133   error is raised. For printing anything more serious and elaborate, the

   134   function @{ML_ind  tracing} is more appropriate. This function writes all

   134   function @{ML_ind  tracing} is more appropriate. This function writes all

   135   output into a separate tracing buffer. For example:

   135   output into a separate tracing buffer. For example:

   136 

   136 

   138 

   138 

   139   It is also possible to redirect the ``channel'' where the string @{text

   139   It is also possible to redirect the ``channel'' where the string @{text

   140   "foo"} is printed to a separate file, e.g., to prevent ProofGeneral from

   140   "foo"} is printed to a separate file, e.g., to prevent ProofGeneral from

   141   choking on massive amounts of trace output. This redirection can be achieved

   141   choking on massive amounts of trace output. This redirection can be achieved

   142   with the code:

   142   with the code:

   208 text {*

   208 text {*

   209   It can now be used as follows

   209   It can now be used as follows

   210 

   210 

   211   @{ML_response_fake [display,gray]

   211   @{ML_response_fake [display,gray]

   212   "string_of_term @{context} @{term \"1::nat\"}"

   212   "string_of_term @{context} @{term \"1::nat\"}"

   214 

   214 

   215   This produces a string corrsponding to the term @{term [show_types] "1::nat"} with some

   215   This produces a string corrsponding to the term @{term [show_types] "1::nat"} with some

   216   additional information encoded in it. The string can be properly printed by

   216   additional information encoded in it. The string can be properly printed by

   217   using either the function @{ML_ind  writeln} or @{ML_ind  tracing}:

   217   using either the function @{ML_ind  writeln} or @{ML_ind  tracing}:

   218 

   218