src/Pure/Thy/term_style.ML
changeset 43277 1fd31f859fc7
parent 42360 da8817d01e7c
child 50592 a39250169636
equal deleted inserted replaced
43276:91bf67e0e755 43277:1fd31f859fc7
    51 val parse = Args.context :|-- (fn ctxt => Scan.lift 
    51 val parse = Args.context :|-- (fn ctxt => Scan.lift 
    52   (Args.parens (parse_single ctxt ::: Scan.repeat (Args.$$$ "," |-- parse_single ctxt))
    52   (Args.parens (parse_single ctxt ::: Scan.repeat (Args.$$$ "," |-- parse_single ctxt))
    53       >> fold I
    53       >> fold I
    54   || Scan.succeed I));
    54   || Scan.succeed I));
    55 
    55 
    56 val parse_bare = Args.context :|-- (fn ctxt => (Output.legacy_feature "Old-style antiquotation style.";
    56 val parse_bare = Args.context :|-- (fn ctxt => (legacy_feature "Old-style antiquotation style.";
    57   Scan.lift Args.liberal_name
    57   Scan.lift Args.liberal_name
    58   >> (fn name => fst (Args.context_syntax "style"
    58   >> (fn name => fst (Args.context_syntax "style"
    59        (Scan.lift (the_style (Proof_Context.theory_of ctxt) name))
    59        (Scan.lift (the_style (Proof_Context.theory_of ctxt) name))
    60           (Args.src (("style", []), Position.none)) ctxt |>> (fn f => f ctxt)))));
    60           (Args.src (("style", []), Position.none)) ctxt |>> (fn f => f ctxt)))));
    61 
    61 
    82   end);
    82   end);
    83 
    83 
    84 fun style_parm_premise i = Scan.succeed (fn ctxt => fn t =>
    84 fun style_parm_premise i = Scan.succeed (fn ctxt => fn t =>
    85   let
    85   let
    86     val i_str = string_of_int i;
    86     val i_str = string_of_int i;
    87     val _ = Output.legacy_feature (quote ("prem" ^ i_str)
    87     val _ = legacy_feature (quote ("prem" ^ i_str)
    88       ^ " term style encountered; use explicit argument syntax "
    88       ^ " term style encountered; use explicit argument syntax "
    89       ^ quote ("prem " ^ i_str) ^ " instead.");
    89       ^ quote ("prem " ^ i_str) ^ " instead.");
    90     val prems = Logic.strip_imp_prems t;
    90     val prems = Logic.strip_imp_prems t;
    91   in
    91   in
    92     if i <= length prems then nth prems (i - 1)
    92     if i <= length prems then nth prems (i - 1)