[isabelle-dev] fun : term -> string

[Walther Neuper]

Hi Jasmin,

following your hint this works fine:

	fun term2str trm = Print_Mode.setmp (Print_Mode.input ::

  	       filter (curry (op =) Symbol.xsymbolsN) (print_mode_value ()))

  	       (Syntax.string_of_term @{context}) trm;


Thank you very much,
Walther


On 09/23/2010 12:12 PM, Jasmin Christian Blanchette wrote:
> Hi Walther,
>
>    
>> we have hundreds of tests on very old code relying on a function
>>
>>     term2str = fn : term ->  string, with: term2str @{term "str"} = "str"
>>
>> i.e., the string _without_ markup.
>>
>> My actual study of Isabelle code got stuck at 'structure Buffer' (via 'writeln') and at 'markup' --- where can I proceed ?
>>      
> I found a couple of ad hoc solutions to this problem. One way is to set the print mode to "input":
>
>      Print_Mode.setmp (Print_Mode.input ::
>          filter (curry (op =) Symbol.xsymbolsN) (print_mode_value ()))
>          (Syntax.string_of_term ctxt) @{term "str"}
>
> (The business with filter is there to respect the user's "xsymbols" preference. You probably don't need it.) You might need to follow this with
>
>      String.translate (fn c =>  if Char.isPrint c then str c else "")
>
> which I have in my code. Also, you might get several spaces in a row, which you might want to simplify.
>
> The other solution is to strip away the YXML tags, using the following function:
>
>      val unyxml = XML.content_of o YXML.parse_body
>
> These are the solutions I found in those rare cases where I needed this. There might exist better solutions. I hope this helps nonetheless.
>
> Regards,
>
> Jasmin