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
_______________________________________________
Isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
