Re: [isabelle] Syntax.string_of_term changed in Isabelle2013



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;

  term_to_string @{term "a+1::int"}

delivered

  "a+1": string

which we need for checks in our test suite.

In Isabelle2013 the respective functions in "Syntax" deliver strings apparently for the fontend ( "<markup> ..."). Where do we get a (combination of) function(s) with signature

  : _ -> term -> string

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).


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.


	Makarius





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