[isabelle-dev] Parse.term

[Makarius]

On Mon, 16 Aug 2010, Walther Neuper wrote:

>> Since any "inner" syntactic entities need to be presented as atomic 
>> token at the outer layer, Parse.term merely takes some identifier or 
>> quoted string.  The result still needs to be passed on to 
>> Syntax.read_term or similar internally.  (It also adds some funny 
>> markup to the "token" to allow the system detailed reporting of error 
>> positions etc.)
>
> Studying the markup will be postponed after having succeeded with 
> following these hints ...

In fact, you do not need to look into these implementation details to use 
the parser library.  I have mainly mentioned the at all, since there is a 
general tendency in the Urban tutorial to dissect the system down to the 
tiny bits and pieces in order to try understanding it.

Basically, the strings passed in and out of the inner syntax engine are to 
be treated as abstract datatypes that happen to have a visible 
representation for historical reasons (and simplicity).  When using 
Parse.term at the outer syntax layer, it gives you some abstract entity 
that the inner Syntax.read_term will analyse accordingly (you should not 
try to analyse it yourself).

Similarly for Syntax.pretty_term: it produces certain abstract markup that 
the Isabelle "message channel" functions writeln, warning, error etc. will 
treat accordingly.  This is particularly noticable with the Isabelle/Scala 
layer, because it really delivers the full markup to the front-end as 
XML.Tree, taking intermediate string representation again as an historical 
artifact of the old TTY days.


 	Makarius