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, 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.
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.)
PS: In the attached file I searched for where the inner syntax could
come into Parse.term --- so far without success.
I have had a brief look at the file, but found it very hard to read,
because of its exceedingy long lings, and strange indentation. Standard
line length is 80 chars, at most 100 in extreme situations, never beyond.
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
_______________________________________________
Isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
