src/Pure/Isar/method.ML
changeset 59981 0d0f9c66ff3f
parent 59953 3d207f8f40dd
child 59982 f402fd001429
     1.1 --- a/src/Pure/Isar/method.ML	Wed Apr 08 23:00:09 2015 +0200
     1.2 +++ b/src/Pure/Isar/method.ML	Thu Apr 09 11:28:00 2015 +0200
     1.3 @@ -77,8 +77,9 @@
     1.4    val position: text_range option -> Position.T
     1.5    val reports_of: text_range -> Position.report list
     1.6    val report: text_range -> unit
     1.7 +  val parser': Proof.context -> int -> text_range parser
     1.8 +  val parser: int -> text_range parser
     1.9    val parse: text_range parser
    1.10 -  val parse_internal: Proof.context -> text_range parser
    1.11  end;
    1.12  
    1.13  structure Method: METHOD =
    1.14 @@ -574,7 +575,7 @@
    1.15  fun is_symid_meth s =
    1.16    s <> "|" andalso s <> "?" andalso s <> "+" andalso Token.ident_or_symbolic s;
    1.17  
    1.18 -fun parser check_ctxt low_pri =
    1.19 +fun gen_parser check_ctxt pri =
    1.20    let
    1.21      val (meth_name, mk_src) =
    1.22        (case check_ctxt of
    1.23 @@ -610,15 +611,17 @@
    1.24      and meth0 x =
    1.25        (Parse.enum1_positions "|" meth1
    1.26          >> (fn ([m], _) => m | (ms, ps) => Combinator (combinator_info ps, Orelse, ms))) x;
    1.27 -  in
    1.28 -    Scan.trace (if low_pri then meth0 else meth4)
    1.29 -      >> (fn (m, toks) => (m, Token.range_of toks))
    1.30 -  end;
    1.31 +
    1.32 +    val meth =
    1.33 +      nth [meth0, meth1, meth2, meth3, meth4, meth5] pri
    1.34 +        handle General.Subscript => raise Fail ("Bad method parser priority " ^ string_of_int pri);
    1.35 +  in Scan.trace meth >> (fn (m, toks) => (m, Token.range_of toks)) end;
    1.36  
    1.37  in
    1.38  
    1.39 -val parse = parser NONE false;
    1.40 -fun parse_internal ctxt = parser (SOME ctxt) true;
    1.41 +val parser' = gen_parser o SOME;
    1.42 +val parser = gen_parser NONE;
    1.43 +val parse = parser 4;
    1.44  
    1.45  end;
    1.46  
    1.47 @@ -672,4 +675,3 @@
    1.48  val SIMPLE_METHOD = Method.SIMPLE_METHOD;
    1.49  val SIMPLE_METHOD' = Method.SIMPLE_METHOD';
    1.50  val SIMPLE_METHOD'' = Method.SIMPLE_METHOD'';
    1.51 -