[isabelle-dev] Parse.term

[Makarius]

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