188 |
188 |
189 @{ML_response_fake [display,gray] "(!! (fn _ => \"foo\") ($$ \"h\")) (explode \"world\")" |
189 @{ML_response_fake [display,gray] "(!! (fn _ => \"foo\") ($$ \"h\")) (explode \"world\")" |
190 "Exception ABORT raised"} |
190 "Exception ABORT raised"} |
191 |
191 |
192 then the parsing aborts and the error message @{text "foo"} is printed. In order to |
192 then the parsing aborts and the error message @{text "foo"} is printed. In order to |
193 see the error message properly, we need to prefix the parser with the function |
193 see the error message properly, you need to prefix the parser with the function |
194 @{ML "Scan.error"}. For example: |
194 @{ML "Scan.error"}. For example: |
195 |
195 |
196 @{ML_response_fake [display,gray] "Scan.error (!! (fn _ => \"foo\") ($$ \"h\"))" |
196 @{ML_response_fake [display,gray] "Scan.error (!! (fn _ => \"foo\") ($$ \"h\"))" |
197 "Exception Error \"foo\" raised"} |
197 "Exception Error \"foo\" raised"} |
198 |
198 |
597 |
597 |
598 text {* |
598 text {* |
599 (FIXME: why is intro, elim and dest treated differently from bar?) |
599 (FIXME: why is intro, elim and dest treated differently from bar?) |
600 *} |
600 *} |
601 |
601 |
|
602 ML{*val spec_parser = |
|
603 OuterParse.opt_target -- |
|
604 OuterParse.fixes -- |
|
605 OuterParse.for_fixes -- |
|
606 Scan.optional |
|
607 (OuterParse.$$$ "where" |-- |
|
608 OuterParse.!!! |
|
609 (OuterParse.enum1 "|" |
|
610 (SpecParse.opt_thm_name ":" -- OuterParse.prop))) []*} |
|
611 |
602 text {* |
612 text {* |
603 @{ML_response [display,gray] |
613 @{ML_response [display,gray] |
604 "let |
614 "let |
605 val input = filtered_input |
615 val input = filtered_input |
606 (\"even and odd \" ^ |
616 (\"even and odd \" ^ |
607 \"where \" ^ |
617 \"where \" ^ |
608 \" even0[intro]: \\\"even 0\\\" \" ^ |
618 \" even0[intro]: \\\"even 0\\\" \" ^ |
609 \"| evenS[intro]: \\\"odd n \<Longrightarrow> even (Suc n)\\\" \" ^ |
619 \"| evenS[intro]: \\\"odd n \<Longrightarrow> even (Suc n)\\\" \" ^ |
610 \"| oddS[intro]: \\\"even n \<Longrightarrow> odd (Suc n)\\\"\") |
620 \"| oddS[intro]: \\\"even n \<Longrightarrow> odd (Suc n)\\\"\") |
611 |
|
612 val parser = |
|
613 OuterParse.opt_target -- |
|
614 OuterParse.fixes -- |
|
615 OuterParse.for_fixes -- |
|
616 Scan.optional |
|
617 (OuterParse.$$$ \"where\" |-- |
|
618 OuterParse.!!! |
|
619 (OuterParse.enum1 \"|\" |
|
620 (SpecParse.opt_thm_name \":\" -- OuterParse.prop))) [] |
|
621 in |
621 in |
622 parse parser input |
622 parse spec_parser input |
623 end" |
623 end" |
624 "((((NONE, [(even, NONE, NoSyn), (odd, NONE, NoSyn)]), []), |
624 "((((NONE, [(even, NONE, NoSyn), (odd, NONE, NoSyn)]), []), |
625 [((even0,\<dots>), \"\\^E\\^Ftoken\\^Eeven 0\\^E\\^F\\^E\"), |
625 [((even0,\<dots>), \"\\^E\\^Ftoken\\^Eeven 0\\^E\\^F\\^E\"), |
626 ((evenS,\<dots>), \"\\^E\\^Ftoken\\^Eodd n \<Longrightarrow> even (Suc n)\\^E\\^F\\^E\"), |
626 ((evenS,\<dots>), \"\\^E\\^Ftoken\\^Eodd n \<Longrightarrow> even (Suc n)\\^E\\^F\\^E\"), |
627 ((oddS,\<dots>), \"\\^E\\^Ftoken\\^Eeven n \<Longrightarrow> odd (Suc n)\\^E\\^F\\^E\")]), [])"} |
627 ((oddS,\<dots>), \"\\^E\\^Ftoken\\^Eeven n \<Longrightarrow> odd (Suc n)\\^E\\^F\\^E\")]), [])"} |