equal
deleted
inserted
replaced
796 Scan.option (Scan.ahead (OuterParse.name || |
796 Scan.option (Scan.ahead (OuterParse.name || |
797 OuterParse.$$$ "[") -- |
797 OuterParse.$$$ "[") -- |
798 OuterParse.!!! (OuterParse.$$$ "|"))))) [] *} |
798 OuterParse.!!! (OuterParse.$$$ "|"))))) [] *} |
799 text_raw {* |
799 text_raw {* |
800 \end{isabelle} |
800 \end{isabelle} |
801 Both parsers accept the same input, but if you look closely, you can notice |
801 Both parsers accept the same input% that's not true: |
|
802 % spec_parser accepts input that is refuted by spec_parser' |
|
803 , but if you look closely, you can notice |
802 an additional ``tail'' (Lines 8 to 10) in @{ML spec_parser'}. What is the purpose of |
804 an additional ``tail'' (Lines 8 to 10) in @{ML spec_parser'}. What is the purpose of |
803 this additional ``tail''? |
805 this additional ``tail''? |
804 \end{exercise} |
806 \end{exercise} |
805 *} |
807 *} |
806 |
808 |