668 text \<open> |
668 text \<open> |
669 where we pretend the parsed string starts on line 7. An example is |
669 where we pretend the parsed string starts on line 7. An example is |
670 |
670 |
671 @{ML_response [display,gray] |
671 @{ML_response [display,gray] |
672 \<open>filtered_input' "foo \n bar"\<close> |
672 \<open>filtered_input' "foo \n bar"\<close> |
673 \<open>[Token (("foo", ({line=7, offset=1, end_offset=4}, {line=7, offset=4})), (Ident, "foo"),\<dots>), |
673 \<open>[Token (("foo", ({line=7, offset=1, end_offset=4}, |
674 Token (("bar", ({line=8, offset=7, end_offset=10}, {line=8, offset=10})), (Ident, "bar"),\<dots>)]\<close>} |
674 {line=7, offset=4})), (Ident, "foo"),\<dots>), |
|
675 Token (("bar", ({line=8, offset=7, end_offset=10}, |
|
676 {line=8, offset=10})), (Ident, "bar"),\<dots>)]\<close>} |
675 |
677 |
676 in which the @{text [quotes] "\\n"} causes the second token to be in |
678 in which the @{text [quotes] "\\n"} causes the second token to be in |
677 line 8. |
679 line 8. |
678 |
680 |
679 By using the parser @{ML position in Parse} you can access the token |
681 By using the parser @{ML position in Parse} you can access the token |
1325 |
1327 |
1326 An example of a very simple method is: |
1328 An example of a very simple method is: |
1327 \<close> |
1329 \<close> |
1328 |
1330 |
1329 method_setup %gray foo = |
1331 method_setup %gray foo = |
1330 \<open>Scan.succeed |
1332 \<open>Scan.succeed (fn ctxt => |
1331 (fn ctxt => (SIMPLE_METHOD ((eresolve_tac ctxt [@{thm conjE}] THEN' resolve_tac ctxt [@{thm conjI}]) 1)))\<close> |
1333 (SIMPLE_METHOD ((eresolve_tac ctxt [@{thm conjE}] THEN' |
1332 "foo method for conjE and conjI" |
1334 resolve_tac ctxt [@{thm conjI}]) 1)))\<close> |
|
1335 "foo method for conjE and conjI" |
1333 |
1336 |
1334 text \<open> |
1337 text \<open> |
1335 It defines the method \<open>foo\<close>, which takes no arguments (therefore the |
1338 It defines the method \<open>foo\<close>, which takes no arguments (therefore the |
1336 parser @{ML Scan.succeed}) and only applies a single tactic, namely the tactic which |
1339 parser @{ML Scan.succeed}) and only applies a single tactic, namely the tactic which |
1337 applies @{thm [source] conjE} and then @{thm [source] conjI}. The function |
1340 applies @{thm [source] conjE} and then @{thm [source] conjI}. The function |