syntax: Context.generic;
authorwenzelm
Fri Feb 10 02:22:43 2006 +0100 (2006-02-10)
changeset 18999e0eb9cb97db0
parent 18998 10c251f29847
child 19000 1f73a35743f4
syntax: Context.generic;
src/Pure/Isar/method.ML
     1.1 --- a/src/Pure/Isar/method.ML	Fri Feb 10 02:22:41 2006 +0100
     1.2 +++ b/src/Pure/Isar/method.ML	Fri Feb 10 02:22:43 2006 +0100
     1.3 @@ -76,15 +76,14 @@
     1.4    val add_method: bstring * (src -> ProofContext.context -> method) * string
     1.5      -> theory -> theory
     1.6    val method_setup: bstring * string * string -> theory -> theory
     1.7 -  val syntax: (ProofContext.context * Args.T list -> 'a * (ProofContext.context * Args.T list))
     1.8 +  val syntax: (Context.generic * Args.T list -> 'a * (Context.generic * Args.T list))
     1.9      -> src -> ProofContext.context -> ProofContext.context * 'a
    1.10    val simple_args: (Args.T list -> 'a * Args.T list)
    1.11      -> ('a -> ProofContext.context -> method) -> src -> ProofContext.context -> method
    1.12    val ctxt_args: (ProofContext.context -> method) -> src -> ProofContext.context -> method
    1.13    val no_args: method -> src -> ProofContext.context -> method
    1.14    type modifier
    1.15 -  val sectioned_args: (ProofContext.context * Args.T list ->
    1.16 -      'a * (ProofContext.context * Args.T list)) ->
    1.17 +  val sectioned_args: (Context.generic * Args.T list -> 'a * (Context.generic * Args.T list)) ->
    1.18      (Args.T list -> modifier * Args.T list) list ->
    1.19      ('a -> ProofContext.context -> 'b) -> src -> ProofContext.context -> 'b
    1.20    val bang_sectioned_args:
    1.21 @@ -92,7 +91,7 @@
    1.22      (thm list -> ProofContext.context -> 'a) -> src -> ProofContext.context -> 'a
    1.23    val bang_sectioned_args':
    1.24      (Args.T list -> modifier * Args.T list) list ->
    1.25 -    (ProofContext.context * Args.T list -> 'a * (ProofContext.context * Args.T list)) ->
    1.26 +    (Context.generic * Args.T list -> 'a * (Context.generic * Args.T list)) ->
    1.27      ('a -> thm list -> ProofContext.context -> 'b) -> src -> ProofContext.context -> 'b
    1.28    val only_sectioned_args:
    1.29      (Args.T list -> modifier * Args.T list) list ->
    1.30 @@ -103,13 +102,11 @@
    1.31    val thm_args: (thm -> 'a) -> src -> ProofContext.context -> 'a
    1.32    val goal_args: (Args.T list -> 'a * Args.T list) -> ('a -> int -> tactic)
    1.33      -> src -> ProofContext.context -> method
    1.34 -  val goal_args': (ProofContext.context * Args.T list ->
    1.35 -      'a * (ProofContext.context * Args.T list))
    1.36 +  val goal_args': (Context.generic * Args.T list -> 'a * (Context.generic * Args.T list))
    1.37      -> ('a -> int -> tactic) -> src -> ProofContext.context -> method
    1.38    val goal_args_ctxt: (Args.T list -> 'a * Args.T list) ->
    1.39      (ProofContext.context -> 'a -> int -> tactic) -> src -> ProofContext.context -> method
    1.40 -  val goal_args_ctxt': (ProofContext.context * Args.T list ->
    1.41 -    'a * (ProofContext.context * Args.T list)) ->
    1.42 +  val goal_args_ctxt': (Context.generic * Args.T list -> 'a * (Context.generic * Args.T list)) ->
    1.43      (ProofContext.context -> 'a -> int -> tactic) -> src -> ProofContext.context -> method
    1.44  end;
    1.45  
    1.46 @@ -602,9 +599,7 @@
    1.47  
    1.48  (* basic *)
    1.49  
    1.50 -fun syntax (scan:
    1.51 -    (ProofContext.context * Args.T list -> 'a * (ProofContext.context * Args.T list))) =
    1.52 -  Args.syntax "method" scan;
    1.53 +fun syntax scan = Args.context_syntax "method" scan;
    1.54  
    1.55  fun simple_args scan f src ctxt : method =
    1.56    #2 (syntax (Scan.lift (scan >> (fn x => f x ctxt))) src ctxt);
    1.57 @@ -622,13 +617,12 @@
    1.58  local
    1.59  
    1.60  fun sect ss = Scan.first (map Scan.lift ss);
    1.61 -fun thms ss = Scan.unless (sect ss) Attrib.local_thms;
    1.62 -fun thmss ss = Scan.repeat (thms ss) >> List.concat;
    1.63 +fun thms ss = Scan.repeat (Scan.unless (sect ss) Attrib.multi_thm) >> List.concat;
    1.64  
    1.65 -fun apply (f, att) (ctxt, ths) = foldl_map (Thm.proof_attributes [att]) (f ctxt, ths);
    1.66 +fun apply (f, att) (context, ths) = foldl_map att (Context.map_proof f context, ths);
    1.67  
    1.68 -fun section ss = (sect ss -- thmss ss) :-- (fn (m, ths) => Scan.depend (fn ctxt =>
    1.69 -  Scan.succeed (apply m (ctxt, ths)))) >> #2;
    1.70 +fun section ss = (sect ss -- thms ss) :-- (fn (m, ths) => Scan.depend (fn context =>
    1.71 +  Scan.succeed (apply m (context, ths)))) >> #2;
    1.72  
    1.73  fun sectioned args ss = args -- Scan.repeat (section ss);
    1.74  
    1.75 @@ -643,7 +637,7 @@
    1.76    sectioned_args (Args.bang_facts -- scan >> swap) ss (uncurry f);
    1.77  fun only_sectioned_args ss f = sectioned_args (Scan.succeed ()) ss (fn () => f);
    1.78  
    1.79 -fun thms_ctxt_args f = sectioned_args (thmss []) [] f;
    1.80 +fun thms_ctxt_args f = sectioned_args (thms []) [] f;
    1.81  fun thms_args f = thms_ctxt_args (K o f);
    1.82  fun thm_args f = thms_args (fn [thm] => f thm | _ => error "Single theorem expected");
    1.83  
    1.84 @@ -686,19 +680,19 @@
    1.85  (* tactic syntax *)
    1.86  
    1.87  fun nat_thms_args f = uncurry f oo
    1.88 -  (#2 oo syntax (Scan.lift (Scan.optional (Args.parens Args.nat) 0) -- Attrib.local_thmss));
    1.89 +  (#2 oo syntax (Scan.lift (Scan.optional (Args.parens Args.nat) 0) -- Attrib.thms));
    1.90  
    1.91  val insts =
    1.92    Scan.optional
    1.93      (Args.enum1 "and" (Scan.lift (Args.name -- (Args.$$$ "=" |-- Args.!!! Args.name))) --|
    1.94 -      Scan.lift (Args.$$$ "in")) [] -- Attrib.local_thmss;
    1.95 +      Scan.lift (Args.$$$ "in")) [] -- Attrib.thms;
    1.96  
    1.97  fun inst_args f src ctxt = f ctxt (#2 (syntax (Args.goal_spec HEADGOAL -- insts) src ctxt));
    1.98  
    1.99  val insts_var =
   1.100    Scan.optional
   1.101      (Args.enum1 "and" (Scan.lift (Args.var -- (Args.$$$ "=" |-- Args.!!! Args.name))) --|
   1.102 -      Scan.lift (Args.$$$ "in")) [] -- Attrib.local_thmss;
   1.103 +      Scan.lift (Args.$$$ "in")) [] -- Attrib.thms;
   1.104  
   1.105  fun inst_args_var f src ctxt =
   1.106    f ctxt (#2 (syntax (Args.goal_spec HEADGOAL -- insts_var) src ctxt));