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

[Makarius]

On Mon, 8 Feb 2010, Thomas Sewell wrote:

> Specifically, f is a polymorphic constant, x is a simple function 
> application generated by our ML code, and y is supplied by the user and 
> must be parsed. So far, our code has simply generated the string 
> expression "f (x) (y)" and passed it to Syntax.read_term. Using the 
> parser to get around type problems seems the ugly way through, however.

Pasting strings together for consumption by the inner syntax engine was 
never robust, and should never be done in production code.  (Likewise is 
it a very bad idea to split output by the pretty printing engine, e.g. the 
result of Syntax.string_of_term.)

In Isabelle2008 we have introduced a clear separation of the raw parsing 
and type-checking phases.  The Syntax.parse_term function is your friend 
-- it will parse legal term fragments to produce a certain "preterm" 
format that can be composed with other preterms and then given to 
Syntax.check_term (or Syntax.check_terms for several simulataneous 
operands).


> In upgrading to Isabelle-2009 everything got broken, because the input 
> for y may be wrapped in YXML code to annotate it with position 
> information, which results in "f (x) (y)" causing a malformed YXML error 
> (it's a forest, not a tree).

When introducing the YXML markup around outer syntax tokens that become 
types/terms later, I was fully aware that any code that manipulates inner 
syntax source will break.  This should be taken as an opportunity to 
remove these things from your code.


 	Makarius