[isabelle-dev] Method parsing, YXML and term construction.

[Makarius]

On Tue, 9 Feb 2010, Thomas Sewell wrote:

> Thanks Makarius, Syntax.parse_term and Syntax.check_term do indeed seem 
> to be my friends.
>
> In fact, I sort of wish I'd known about them earlier. I remember in one 
> of the record package proofs it was annoying me that I had to construct 
> the types explicitly when it felt like I should be able to construct the 
> term skeleton and appeal to the type resolver. Now I know how.
>
> BTW, should I have known this already? Is there some part of the 
> documentation that I should have read, but have overlooked?

I've checked again: you would have had to be a very keen reader of NEWS, 
where it says for Isabelle2007 (not Isabelle2008 as I claimed):

* Pure/Syntax: generic interfaces for parsing (Syntax.parse_term etc.)
and type checking (Syntax.check_term etc.), with common combinations
(Syntax.read_term etc.). These supersede former Sign.read_term etc.
which are considered legacy and await removal.

* Pure/Syntax: generic interfaces for type unchecking
(Syntax.uncheck_terms etc.) and unparsing (Syntax.unparse_term etc.),
with common combinations (Syntax.pretty_term, Syntax.string_of_term
etc.).  Former Sign.pretty_term, Sign.string_of_term etc. are still
available for convenience, but refer to the very same operations using
a mere theory instead of a full context.

The corresponding section in the Isar Implementation manual is this a 
dummy -- I've been close to touching it during my vacation last week.


These issues of parse/check and uncheck/unparse were once very hot in the 
discussion -- a discussion that was somehow too much localized, though.

Both those asking questions and those giving answers should develop a 
habit of making this a bit more public, i.e. on the isabelle-dev mailing 
list.


 	Makarius