thanks a lot for your detailed reply ...
On 08/14/2010 09:01 PM, Makarius wrote:
On Wed, 11 Aug 2010, Walther Neuper wrote:
text {* should not Parse.term repeat until a non-term token is
reached ? *}
parse Parse.term "xxx +++ 111 end";
parse (Scan.repeat Parse.term) "xxx +++ 111 end";
text {* Parse.term stops at "Keyword" of outer syntax ?!?
Should not be parsed according to inner syntax ? *}
parse Parse.term "xxx + 111 end";
parse Parse.term "xxx +++ (111) end";
I do not fully understand the misunderstanding yet,
The misunderstanding came from that I'd simply lost sight of the quotes
required around terms while digging in the sources ...
but outer syntax parsers cannot know anything about inner syntax --
the context is missing, and even with the inner grammer tables
available, it would be technically very hard to make it work robustly
and efficiently. In fact, the separation of outer vs. inner syntax
allows a great deal of flexibility on both sides: outer commands can
be introduced easily by users later on, and inner parsing can work
with fully general context-free grammars. The price for that are
funny quotes in user input, but the implementation should get simpler
in almost every respect.
... I see. Nice to see this separation of outer syntax and inner syntax
reflected in the scala layer.
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 ...
[...]
Anyway, to understand Parse.term you need to look both "inside" and
"around". Looking inside means brief inspection of 1-3 layers of the
implementation, not more (control-hover-click in Isabelle/jEdit makes
that relatively easy). Looking around means to check some common uses
of the thing in question: e.g. by hypersearch for "Parse.term" in jEdit.
This should give you various examples of Isar command parsers that
pass on the outer token to Syntax.read_term or similar.
Makarius
Walther
_______________________________________________
Isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
