[isabelle-dev] Parse.term

[Walther Neuper]

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