Args/Attrib syntax: Context.generic;
authorwenzelm
Fri Feb 10 02:22:16 2006 +0100 (2006-02-10)
changeset 18988d6e5fa2ba8b8
parent 18987 61c7875a58b8
child 18989 a5c3bc6fd6b6
Args/Attrib syntax: Context.generic;
src/HOL/Tools/datatype_package.ML
src/Provers/eqsubst.ML
src/Provers/induct_method.ML
src/Provers/splitter.ML
src/Pure/Isar/isar_output.ML
src/Pure/simplifier.ML
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Fri Feb 10 02:22:13 2006 +0100
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Fri Feb 10 02:22:16 2006 +0100
     1.3 @@ -262,7 +262,7 @@
     1.4  local
     1.5  
     1.6  val rule_spec = Scan.lift (Args.$$$ "rule" -- Args.$$$ ":");
     1.7 -val opt_rule = Scan.option (rule_spec |-- Attrib.local_thm);
     1.8 +val opt_rule = Scan.option (rule_spec |-- Attrib.thm);
     1.9  
    1.10  val varss =
    1.11    Args.and_list (Scan.repeat (Scan.unless rule_spec (Scan.lift (Args.maybe Args.name))));
     2.1 --- a/src/Provers/eqsubst.ML	Fri Feb 10 02:22:13 2006 +0100
     2.2 +++ b/src/Provers/eqsubst.ML	Fri Feb 10 02:22:16 2006 +0100
     2.3 @@ -331,7 +331,7 @@
     2.4  should be done to an assumption, false = apply to the conclusion of
     2.5  the goal) as well as the theorems to use *)
     2.6  fun subst_meth src =
     2.7 -  Method.syntax ((Scan.lift options_syntax) -- (Scan.lift ith_syntax) -- Attrib.local_thms) src
     2.8 +  Method.syntax ((Scan.lift options_syntax) -- (Scan.lift ith_syntax) -- Attrib.thms) src
     2.9    #> (fn (ctxt, ((asmflag, occL), inthms)) =>
    2.10      (if asmflag then eqsubst_asm_meth else eqsubst_meth) ctxt occL inthms);
    2.11  
     3.1 --- a/src/Provers/induct_method.ML	Fri Feb 10 02:22:13 2006 +0100
     3.2 +++ b/src/Provers/induct_method.ML	Fri Feb 10 02:22:16 2006 +0100
     3.3 @@ -491,29 +491,29 @@
     3.4  
     3.5  fun named_rule k arg get =
     3.6    Scan.lift (Args.$$$ k -- Args.colon) |-- Scan.repeat arg :--
     3.7 -    (fn names => Scan.peek (fn ctxt => Scan.succeed (names |> map (fn name =>
     3.8 -      (case get ctxt name of SOME x => x
     3.9 +    (fn names => Scan.peek (fn context => Scan.succeed (names |> map (fn name =>
    3.10 +      (case get (Context.proof_of context) name of SOME x => x
    3.11        | NONE => error ("No rule for " ^ k ^ " " ^ quote name)))))) >> #2;
    3.12  
    3.13  fun rule get_type get_set =
    3.14 -  named_rule InductAttrib.typeN Args.local_tyname get_type ||
    3.15 -  named_rule InductAttrib.setN Args.local_const get_set ||
    3.16 -  Scan.lift (Args.$$$ ruleN -- Args.colon) |-- Attrib.local_thmss;
    3.17 +  named_rule InductAttrib.typeN Args.tyname get_type ||
    3.18 +  named_rule InductAttrib.setN Args.const get_set ||
    3.19 +  Scan.lift (Args.$$$ ruleN -- Args.colon) |-- Attrib.thms;
    3.20  
    3.21  val cases_rule = rule InductAttrib.lookup_casesT InductAttrib.lookup_casesS >> single_rule;
    3.22  val induct_rule = rule InductAttrib.lookup_inductT InductAttrib.lookup_inductS;
    3.23  val coinduct_rule =
    3.24    rule InductAttrib.lookup_coinductT InductAttrib.lookup_coinductS >> single_rule;
    3.25  
    3.26 -val inst = Scan.lift (Args.$$$ "_") >> K NONE || Args.local_term >> SOME;
    3.27 +val inst = Scan.lift (Args.$$$ "_") >> K NONE || Args.term >> SOME;
    3.28  
    3.29  val def_inst =
    3.30    ((Scan.lift (Args.name --| (Args.$$$ "\\<equiv>" || Args.$$$ "==")) >> SOME)
    3.31 -      -- Args.local_term) >> SOME ||
    3.32 +      -- Args.term) >> SOME ||
    3.33      inst >> Option.map (pair NONE);
    3.34  
    3.35 -val free = Scan.state -- Args.local_term >> (fn (_, Free v) => v | (ctxt, t) =>
    3.36 -  error ("Bad free variable: " ^ ProofContext.string_of_term ctxt t));
    3.37 +val free = Scan.state -- Args.term >> (fn (_, Free v) => v | (context, t) =>
    3.38 +  error ("Bad free variable: " ^ ProofContext.string_of_term (Context.proof_of context) t));
    3.39  
    3.40  fun unless_more_args scan = Scan.unless (Scan.lift
    3.41    ((Args.$$$ fixingN || Args.$$$ takingN || Args.$$$ InductAttrib.typeN ||
     4.1 --- a/src/Provers/splitter.ML	Fri Feb 10 02:22:13 2006 +0100
     4.2 +++ b/src/Provers/splitter.ML	Fri Feb 10 02:22:16 2006 +0100
     4.3 @@ -448,7 +448,7 @@
     4.4    Args.$$$ splitN -- Args.del -- Args.colon >> K (I, split_del)];
     4.5  
     4.6  fun split_meth src =
     4.7 -  Method.syntax Attrib.local_thms src
     4.8 +  Method.syntax Attrib.thms src
     4.9    #> (fn (_, ths) => Method.SIMPLE_METHOD' HEADGOAL (CHANGED_PROP o gen_split_tac ths));
    4.10  
    4.11  
     5.1 --- a/src/Pure/Isar/isar_output.ML	Fri Feb 10 02:22:13 2006 +0100
     5.2 +++ b/src/Pure/Isar/isar_output.ML	Fri Feb 10 02:22:16 2006 +0100
     5.3 @@ -16,7 +16,7 @@
     5.4    val print_antiquotations: unit -> unit
     5.5    val boolean: string -> bool
     5.6    val integer: string -> int
     5.7 -  val args: (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list)) ->
     5.8 +  val args: (Context.generic * Args.T list -> 'a * (Context.generic * Args.T list)) ->
     5.9      (Args.src -> Proof.context -> 'a -> string) -> Args.src -> Toplevel.state -> string
    5.10    datatype markup = Markup | MarkupEnv | Verbatim
    5.11    val modes: string list ref
    5.12 @@ -110,8 +110,7 @@
    5.13  
    5.14  (* args syntax *)
    5.15  
    5.16 -fun syntax (scan: (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list))) =
    5.17 -  Args.syntax "antiquotation" scan;
    5.18 +fun syntax scan = Args.context_syntax "antiquotation" scan;
    5.19  
    5.20  fun args scan f src state : string =
    5.21    let
    5.22 @@ -505,20 +504,20 @@
    5.23  (* commands *)
    5.24  
    5.25  val _ = add_commands
    5.26 - [("thm", args Attrib.local_thmss (output_list pretty_thm)),
    5.27 -  ("thm_style", args (Scan.lift Args.liberal_name -- Attrib.local_thm) (output pretty_thm_style)),
    5.28 -  ("prop", args Args.local_prop (output pretty_term)),
    5.29 -  ("term", args Args.local_term (output pretty_term)),
    5.30 -  ("term_style", args (Scan.lift Args.liberal_name -- Args.local_term) (output pretty_term_style)),
    5.31 -  ("term_type", args Args.local_term (output pretty_term_typ)),
    5.32 -  ("typeof", args Args.local_term (output pretty_term_typeof)),
    5.33 -  ("const", args Args.local_term (output pretty_term_const)),
    5.34 -  ("typ", args Args.local_typ_abbrev (output ProofContext.pretty_typ)),
    5.35 + [("thm", args Attrib.thms (output_list pretty_thm)),
    5.36 +  ("thm_style", args (Scan.lift Args.liberal_name -- Attrib.thm) (output pretty_thm_style)),
    5.37 +  ("prop", args Args.prop (output pretty_term)),
    5.38 +  ("term", args Args.term (output pretty_term)),
    5.39 +  ("term_style", args (Scan.lift Args.liberal_name -- Args.term) (output pretty_term_style)),
    5.40 +  ("term_type", args Args.term (output pretty_term_typ)),
    5.41 +  ("typeof", args Args.term (output pretty_term_typeof)),
    5.42 +  ("const", args Args.term (output pretty_term_const)),
    5.43 +  ("typ", args Args.typ_abbrev (output ProofContext.pretty_typ)),
    5.44    ("text", args (Scan.lift Args.name) (output (K pretty_text))),
    5.45    ("goals", output_goals true),
    5.46    ("subgoals", output_goals false),
    5.47 -  ("prf", args Attrib.local_thmss (output (pretty_prf false))),
    5.48 -  ("full_prf", args Attrib.local_thmss (output (pretty_prf true))),
    5.49 +  ("prf", args Attrib.thms (output (pretty_prf false))),
    5.50 +  ("full_prf", args Attrib.thms (output (pretty_prf true))),
    5.51    ("ML", args (Scan.lift Args.name) (output_ml ml_val)),
    5.52    ("ML_type", args (Scan.lift Args.name) (output_ml ml_type)),
    5.53    ("ML_struct", args (Scan.lift Args.name) (output_ml ml_struct))];
     6.1 --- a/src/Pure/simplifier.ML	Fri Feb 10 02:22:13 2006 +0100
     6.2 +++ b/src/Pure/simplifier.ML	Fri Feb 10 02:22:16 2006 +0100
     6.3 @@ -251,7 +251,7 @@
     6.4  in
     6.5  
     6.6  val simplified =
     6.7 -  Attrib.syntax (conv_mode -- Attrib.thmss >> (fn (f, ths) => Thm.rule_attribute (fn x =>
     6.8 +  Attrib.syntax (conv_mode -- Attrib.thms >> (fn (f, ths) => Thm.rule_attribute (fn x =>
     6.9      f ((if null ths then I else MetaSimplifier.clear_ss) (get_ss x) addsimps ths))));
    6.10  
    6.11  end;