Re: [isabelle] Syntax.string_of_term changed in Isabelle2013



On 07/21/2013 11:03 AM, Makarius wrote:
On Sat, 20 Jul 2013, Walther Neuper wrote:

In Isabelle2012 the function

  fun term_to_str t = Print_Mode.setmp [] (Syntax.string_of_term
    (Proof_Context.init_global (Thy_Info.get_theory "Isac"))) t;
:
in Isabelle2013 ?

Here is an example that works better:

ML {*
  fun term_to_string ctxt t =
    let
      val ctxt' = Config.put show_markup false ctxt;
    in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;

term_to_string (Proof_Context.init_global @{theory Main}) @{term "a+1::int"}
*}

Note that show_markup is the key thing here. You should also avoid Thy_Info.get_theory, since it only works in certain situations (theory produced TTY or batch mode).

Thanks a lot for the function (we got stuck with Pretty.T) and the note ...

What are you doing with the string output anyway? It is relatively hard to rely on exact behaviour of inner syntax layers, apart from the normal mode of operation as user input / output.

... because a considerable part of our regression tests still uses this function.

We shall narrow the gap to Isabelle standards also in isac's test configuration, but that will take time (and won't start before all tests are running on Isabelle2013 ;-)

Walther




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.