--- a/src/Pure/Isar/method.ML Wed Apr 08 23:00:09 2015 +0200
+++ b/src/Pure/Isar/method.ML Thu Apr 09 11:28:00 2015 +0200
@@ -77,8 +77,9 @@
val position: text_range option -> Position.T
val reports_of: text_range -> Position.report list
val report: text_range -> unit
+ val parser': Proof.context -> int -> text_range parser
+ val parser: int -> text_range parser
val parse: text_range parser
- val parse_internal: Proof.context -> text_range parser
end;
structure Method: METHOD =
@@ -574,7 +575,7 @@
fun is_symid_meth s =
s <> "|" andalso s <> "?" andalso s <> "+" andalso Token.ident_or_symbolic s;
-fun parser check_ctxt low_pri =
+fun gen_parser check_ctxt pri =
let
val (meth_name, mk_src) =
(case check_ctxt of
@@ -610,15 +611,17 @@
and meth0 x =
(Parse.enum1_positions "|" meth1
>> (fn ([m], _) => m | (ms, ps) => Combinator (combinator_info ps, Orelse, ms))) x;
- in
- Scan.trace (if low_pri then meth0 else meth4)
- >> (fn (m, toks) => (m, Token.range_of toks))
- end;
+
+ val meth =
+ nth [meth0, meth1, meth2, meth3, meth4, meth5] pri
+ handle General.Subscript => raise Fail ("Bad method parser priority " ^ string_of_int pri);
+ in Scan.trace meth >> (fn (m, toks) => (m, Token.range_of toks)) end;
in
-val parse = parser NONE false;
-fun parse_internal ctxt = parser (SOME ctxt) true;
+val parser' = gen_parser o SOME;
+val parser = gen_parser NONE;
+val parse = parser 4;
end;
@@ -672,4 +675,3 @@
val SIMPLE_METHOD = Method.SIMPLE_METHOD;
val SIMPLE_METHOD' = Method.SIMPLE_METHOD';
val SIMPLE_METHOD'' = Method.SIMPLE_METHOD'';
-