1.1 --- a/doc-src/antiquote_setup.ML Sat Aug 09 12:28:13 2008 +0200
1.2 +++ b/doc-src/antiquote_setup.ML Sat Aug 09 22:43:46 2008 +0200
1.3 @@ -30,7 +30,7 @@
1.4 | clean_name "}" = "braceright"
1.5 | clean_name s = s |> translate_string (fn "_" => "-" | c => c);
1.6
1.7 -val str_of_source = space_implode " " o map Args.string_of o #2 o #1 o Args.dest_src;
1.8 +val str_of_source = space_implode " " o map OuterLex.unparse o #2 o #1 o Args.dest_src;
1.9
1.10 fun tweak_line s =
1.11 if ! O.display then s else Symbol.strip_blanks s;
2.1 --- a/src/FOL/ex/IffOracle.thy Sat Aug 09 12:28:13 2008 +0200
2.2 +++ b/src/FOL/ex/IffOracle.thy Sat Aug 09 22:43:46 2008 +0200
2.3 @@ -53,7 +53,7 @@
2.4 subsection {* Oracle as proof method *}
2.5
2.6 method_setup iff = {*
2.7 - Method.simple_args Args.nat (fn n => fn ctxt =>
2.8 + Method.simple_args OuterParse.nat (fn n => fn ctxt =>
2.9 Method.SIMPLE_METHOD
2.10 (HEADGOAL (Tactic.rtac (iff_oracle (ProofContext.theory_of ctxt) n))
2.11 handle Fail _ => no_tac))
3.1 --- a/src/HOL/Nominal/nominal_induct.ML Sat Aug 09 12:28:13 2008 +0200
3.2 +++ b/src/HOL/Nominal/nominal_induct.ML Sat Aug 09 22:43:46 2008 +0200
3.3 @@ -123,6 +123,8 @@
3.4
3.5 local
3.6
3.7 +structure P = OuterParse;
3.8 +
3.9 val avoidingN = "avoiding";
3.10 val fixingN = "arbitrary"; (* to be consistent with induct; hopefully this changes again *)
3.11 val ruleN = "rule";
3.12 @@ -145,7 +147,7 @@
3.13 Scan.repeat (unless_more_args free)) [];
3.14
3.15 val fixing = Scan.optional (Scan.lift (Args.$$$ fixingN -- Args.colon) |--
3.16 - Args.and_list (Scan.repeat (unless_more_args free))) [];
3.17 + P.and_list' (Scan.repeat (unless_more_args free))) [];
3.18
3.19 val rule_spec = Scan.lift (Args.$$$ "rule" -- Args.colon) |-- Attrib.thms;
3.20
3.21 @@ -153,7 +155,7 @@
3.22
3.23 fun nominal_induct_method src =
3.24 Method.syntax
3.25 - (Args.and_list (Scan.repeat (unless_more_args def_inst)) --
3.26 + (P.and_list' (Scan.repeat (unless_more_args def_inst)) --
3.27 avoiding -- fixing -- rule_spec) src
3.28 #> (fn ((((x, y), z), w), ctxt) =>
3.29 Method.RAW_METHOD_CASES (fn facts =>
4.1 --- a/src/HOL/Tools/inductive_codegen.ML Sat Aug 09 12:28:13 2008 +0200
4.2 +++ b/src/HOL/Tools/inductive_codegen.ML Sat Aug 09 22:43:46 2008 +0200
4.3 @@ -697,6 +697,6 @@
4.4 val setup =
4.5 add_codegen "inductive" inductive_codegen #>
4.6 Code.add_attribute ("ind", Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) --
4.7 - Scan.option (Args.$$$ "params" |-- Args.colon |-- Args.nat) >> uncurry add);
4.8 + Scan.option (Args.$$$ "params" |-- Args.colon |-- OuterParse.nat) >> uncurry add);
4.9
4.10 end;
5.1 --- a/src/HOL/Tools/recdef_package.ML Sat Aug 09 12:28:13 2008 +0200
5.2 +++ b/src/HOL/Tools/recdef_package.ML Sat Aug 09 22:43:46 2008 +0200
5.3 @@ -295,7 +295,7 @@
5.4 val _ = List.app OuterKeyword.keyword ["permissive", "congs", "hints"];
5.5
5.6 val hints =
5.7 - P.$$$ "(" |-- P.!!! (P.position (P.$$$ "hints" -- P.arguments) --| P.$$$ ")") >> Args.src;
5.8 + P.$$$ "(" |-- P.!!! (P.position (P.$$$ "hints" -- Args.parse) --| P.$$$ ")") >> Args.src;
5.9
5.10 val recdef_decl =
5.11 Scan.optional (P.$$$ "(" -- P.!!! (P.$$$ "permissive" -- P.$$$ ")") >> K false) true --
6.1 --- a/src/HOL/Tools/res_axioms.ML Sat Aug 09 12:28:13 2008 +0200
6.2 +++ b/src/HOL/Tools/res_axioms.ML Sat Aug 09 22:43:46 2008 +0200
6.3 @@ -557,7 +557,7 @@
6.4
6.5 (** Attribute for converting a theorem into clauses **)
6.6
6.7 -val clausify = Attrib.syntax (Scan.lift Args.nat
6.8 +val clausify = Attrib.syntax (Scan.lift OuterParse.nat
6.9 >> (fn i => Thm.rule_attribute (fn context => fn th =>
6.10 Meson.make_meta_clause (nth (cnf_axiom (Context.theory_of context) th) i))));
6.11
7.1 --- a/src/HOL/Tools/split_rule.ML Sat Aug 09 12:28:13 2008 +0200
7.2 +++ b/src/HOL/Tools/split_rule.ML Sat Aug 09 22:43:46 2008 +0200
7.3 @@ -146,12 +146,11 @@
7.4
7.5 (* FIXME dynamically scoped due to Args.name/pair_tac *)
7.6
7.7 -val split_format = Attrib.syntax
7.8 - (Scan.lift (Args.parens (Args.$$$ "complete"))
7.9 - >> K (Thm.rule_attribute (K complete_split_rule)) ||
7.10 - Args.and_list1 (Scan.lift (Scan.repeat Args.name))
7.11 +val split_format = Attrib.syntax (Scan.lift
7.12 + (Args.parens (Args.$$$ "complete") >> K (Thm.rule_attribute (K complete_split_rule)) ||
7.13 + OuterParse.and_list1 (Scan.repeat Args.name)
7.14 >> (fn xss => Thm.rule_attribute (fn context =>
7.15 - split_rule_goal (Context.proof_of context) xss)));
7.16 + split_rule_goal (Context.proof_of context) xss))));
7.17
7.18 val setup =
7.19 Attrib.add_attributes
8.1 --- a/src/Provers/blast.ML Sat Aug 09 12:28:13 2008 +0200
8.2 +++ b/src/Provers/blast.ML Sat Aug 09 22:43:46 2008 +0200
8.3 @@ -1307,7 +1307,7 @@
8.4 (** method setup **)
8.5
8.6 val blast_method =
8.7 - Method.bang_sectioned_args' Data.cla_modifiers (Scan.lift (Scan.option Args.nat))
8.8 + Method.bang_sectioned_args' Data.cla_modifiers (Scan.lift (Scan.option OuterParse.nat))
8.9 (fn NONE => Data.cla_meth' blast_tac
8.10 | SOME lim => Data.cla_meth' (fn cs => depth_tac cs lim));
8.11
9.1 --- a/src/Provers/clasimp.ML Sat Aug 09 12:28:13 2008 +0200
9.2 +++ b/src/Provers/clasimp.ML Sat Aug 09 22:43:46 2008 +0200
9.3 @@ -302,7 +302,8 @@
9.4
9.5
9.6 fun auto_args m =
9.7 - Method.bang_sectioned_args' clasimp_modifiers (Scan.lift (Scan.option (Args.nat -- Args.nat))) m;
9.8 + Method.bang_sectioned_args' clasimp_modifiers
9.9 + (Scan.lift (Scan.option (OuterParse.nat -- OuterParse.nat))) m;
9.10
9.11 fun auto_meth NONE = clasimp_meth (CHANGED_PROP o auto_tac)
9.12 | auto_meth (SOME (m, n)) = clasimp_meth (CHANGED_PROP o (fn css => mk_auto_tac css m n));
10.1 --- a/src/Provers/eqsubst.ML Sat Aug 09 12:28:13 2008 +0200
10.2 +++ b/src/Provers/eqsubst.ML Sat Aug 09 22:43:46 2008 +0200
10.3 @@ -559,8 +559,7 @@
10.4 (Scan.succeed false);
10.5
10.6 val ith_syntax =
10.7 - (Args.parens (Scan.repeat Args.nat))
10.8 - || (Scan.succeed [0]);
10.9 + Scan.optional (Args.parens (Scan.repeat OuterParse.nat)) [0];
10.10
10.11 (* combination method that takes a flag (true indicates that subst
10.12 should be done to an assumption, false = apply to the conclusion of
11.1 --- a/src/Pure/Isar/context_rules.ML Sat Aug 09 12:28:13 2008 +0200
11.2 +++ b/src/Pure/Isar/context_rules.ML Sat Aug 09 22:43:46 2008 +0200
11.3 @@ -205,8 +205,8 @@
11.4 (* concrete syntax *)
11.5
11.6 fun add_args a b c = Attrib.syntax
11.7 - (Scan.lift ((Args.bang >> K a || Args.query >> K c || Scan.succeed b) -- Scan.option Args.nat)
11.8 - >> (fn (f, n) => f n));
11.9 + (Scan.lift ((Args.bang >> K a || Args.query >> K c || Scan.succeed b) --
11.10 + Scan.option OuterParse.nat) >> (fn (f, n) => f n));
11.11
11.12 val rule_atts =
11.13 [("intro", add_args intro_bang intro intro_query, "declaration of introduction rule"),
12.1 --- a/src/Pure/Isar/rule_insts.ML Sat Aug 09 12:28:13 2008 +0200
12.2 +++ b/src/Pure/Isar/rule_insts.ML Sat Aug 09 22:43:46 2008 +0200
12.3 @@ -28,6 +28,9 @@
12.4 structure RuleInsts: RULE_INSTS =
12.5 struct
12.6
12.7 +structure T = OuterLex;
12.8 +structure P = OuterParse;
12.9 +
12.10
12.11 (** reading instantiations **)
12.12
12.13 @@ -97,11 +100,11 @@
12.14
12.15 val (type_insts, term_insts) = List.partition (is_tvar o fst) mixed_insts;
12.16 val internal_insts = term_insts |> map_filter
12.17 - (fn (xi, Args.Term t) => SOME (xi, t)
12.18 - | (_, Args.Text _) => NONE
12.19 + (fn (xi, T.Term t) => SOME (xi, t)
12.20 + | (_, T.Text _) => NONE
12.21 | (xi, _) => error_var "Term argument expected for " xi);
12.22 val external_insts = term_insts |> map_filter
12.23 - (fn (xi, Args.Text s) => SOME (xi, s) | _ => NONE);
12.24 + (fn (xi, T.Text s) => SOME (xi, s) | _ => NONE);
12.25
12.26
12.27 (* mixed type instantiations *)
12.28 @@ -111,8 +114,8 @@
12.29 val S = the_sort tvars xi;
12.30 val T =
12.31 (case arg of
12.32 - Args.Text s => Syntax.read_typ ctxt s
12.33 - | Args.Typ T => T
12.34 + T.Text s => Syntax.read_typ ctxt s
12.35 + | T.Typ T => T
12.36 | _ => error_var "Type argument expected for " xi);
12.37 in
12.38 if Sign.of_sort thy (T, S) then ((xi, S), T)
12.39 @@ -169,9 +172,9 @@
12.40 val _ = (*assign internalized values*)
12.41 mixed_insts |> List.app (fn (arg, (xi, _)) =>
12.42 if is_tvar xi then
12.43 - Args.assign (SOME (Args.Typ (the (AList.lookup (op =) type_insts xi)))) arg
12.44 + T.assign (SOME (T.Typ (the (AList.lookup (op =) type_insts xi)))) arg
12.45 else
12.46 - Args.assign (SOME (Args.Term (the (AList.lookup (op =) term_insts xi)))) arg);
12.47 + T.assign (SOME (T.Term (the (AList.lookup (op =) term_insts xi)))) arg);
12.48 in
12.49 Drule.instantiate insts thm |> RuleCases.save thm
12.50 end;
12.51 @@ -194,7 +197,7 @@
12.52
12.53 fun read_instantiate ctxt args thm =
12.54 read_instantiate_mixed (ctxt |> ProofContext.set_mode ProofContext.mode_schematic) (* FIXME !? *)
12.55 - (map (fn (x, y) => (Args.eof, (x, Args.Text y))) args) thm;
12.56 + (map (fn (x, y) => (T.eof, (x, T.Text y))) args) thm;
12.57
12.58 fun instantiate_tac ctxt args = PRIMITIVE (read_instantiate ctxt args);
12.59
12.60 @@ -207,16 +210,16 @@
12.61 local
12.62
12.63 val value =
12.64 - Args.internal_typ >> Args.Typ ||
12.65 - Args.internal_term >> Args.Term ||
12.66 - Args.name >> Args.Text;
12.67 + Args.internal_typ >> T.Typ ||
12.68 + Args.internal_term >> T.Term ||
12.69 + Args.name >> T.Text;
12.70
12.71 -val inst = Args.var -- (Args.$$$ "=" |-- Args.ahead -- value)
12.72 +val inst = Args.var -- (Args.$$$ "=" |-- Scan.ahead P.not_eof -- value)
12.73 >> (fn (xi, (a, v)) => (a, (xi, v)));
12.74
12.75 in
12.76
12.77 -val where_att = Attrib.syntax (Args.and_list (Scan.lift inst) >> (fn args =>
12.78 +val where_att = Attrib.syntax (Scan.lift (P.and_list inst) >> (fn args =>
12.79 Thm.rule_attribute (fn context => read_instantiate_mixed (Context.proof_of context) args)));
12.80
12.81 end;
12.82 @@ -227,10 +230,10 @@
12.83 local
12.84
12.85 val value =
12.86 - Args.internal_term >> Args.Term ||
12.87 - Args.name >> Args.Text;
12.88 + Args.internal_term >> T.Term ||
12.89 + Args.name >> T.Text;
12.90
12.91 -val inst = Args.ahead -- Args.maybe value;
12.92 +val inst = Scan.ahead P.not_eof -- Args.maybe value;
12.93 val concl = Args.$$$ "concl" -- Args.colon;
12.94
12.95 val insts =
12.96 @@ -406,16 +409,16 @@
12.97
12.98 val insts =
12.99 Scan.optional
12.100 - (Args.and_list1 (Scan.lift (Args.name -- (Args.$$$ "=" |-- Args.!!! Args.name))) --|
12.101 - Scan.lift (Args.$$$ "in")) [] -- Attrib.thms;
12.102 + (Scan.lift (P.and_list1 (Args.name -- (Args.$$$ "=" |-- P.!!! Args.name)) --| Args.$$$ "in")) []
12.103 + -- Attrib.thms;
12.104
12.105 fun inst_args f src ctxt =
12.106 f ctxt (fst (Method.syntax (Args.goal_spec HEADGOAL -- insts) src ctxt));
12.107
12.108 val insts_var =
12.109 Scan.optional
12.110 - (Args.and_list1 (Scan.lift (Args.var -- (Args.$$$ "=" |-- Args.!!! Args.name))) --|
12.111 - Scan.lift (Args.$$$ "in")) [] -- Attrib.thms;
12.112 + (Scan.lift (P.and_list1 (Args.var -- (Args.$$$ "=" |-- P.!!! Args.name)) --| Args.$$$ "in")) []
12.113 + -- Attrib.thms;
12.114
12.115 fun inst_args_var f src ctxt =
12.116 f ctxt (fst (Method.syntax (Args.goal_spec HEADGOAL -- insts_var) src ctxt));
13.1 --- a/src/Pure/ML/ml_antiquote.ML Sat Aug 09 12:28:13 2008 +0200
13.2 +++ b/src/Pure/ML/ml_antiquote.ML Sat Aug 09 22:43:46 2008 +0200
13.3 @@ -62,6 +62,9 @@
13.4
13.5 (** concrete antiquotations **)
13.6
13.7 +structure P = OuterParse;
13.8 +
13.9 +
13.10 (* misc *)
13.11
13.12 val _ = value "theory"
13.13 @@ -83,11 +86,11 @@
13.14 val _ = inline "prop" (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term));
13.15
13.16 val _ = macro "let" (Args.context --
13.17 - Args.and_list1 (Args.and_list1 (Scan.lift Args.name) -- Scan.lift (Args.$$$ "=" |-- Args.name))
13.18 + Scan.lift (P.and_list1 (P.and_list1 Args.name -- (Args.$$$ "=" |-- Args.name)))
13.19 >> (fn (ctxt, args) => #2 (ProofContext.match_bind true args ctxt)));
13.20
13.21 val _ = macro "note" (Args.context :|-- (fn ctxt =>
13.22 - Args.and_list1 (Scan.lift (Args.opt_thm_name I "=") -- Attrib.thms >> (fn ((a, srcs), ths) =>
13.23 + P.and_list1' (Scan.lift (Args.opt_thm_name I "=") -- Attrib.thms >> (fn ((a, srcs), ths) =>
13.24 ((a, map (Attrib.attribute (ProofContext.theory_of ctxt)) srcs), [(ths, [])])))
13.25 >> (fn args => #2 (ProofContext.note_thmss_i "" args ctxt))));
13.26
13.27 @@ -123,8 +126,8 @@
13.28 val _ = inline "const_syntax" (const true);
13.29
13.30 val _ = inline "const"
13.31 - (Args.context -- Scan.lift Args.name --
13.32 - Scan.optional (Scan.lift (Args.$$$ "(") |-- Args.enum1 "," Args.typ --| Scan.lift (Args.$$$ ")")) []
13.33 + (Args.context -- Scan.lift Args.name -- Scan.optional
13.34 + (Scan.lift (Args.$$$ "(") |-- OuterParse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) []
13.35 >> (fn ((ctxt, c), Ts) =>
13.36 let val (c, _) = Term.dest_Const (ProofContext.read_const_proper ctxt c)
13.37 in ML_Syntax.atomic (ML_Syntax.print_term (ProofContext.mk_const ctxt (c, Ts))) end));
14.1 --- a/src/Pure/ML/ml_context.ML Sat Aug 09 12:28:13 2008 +0200
14.2 +++ b/src/Pure/ML/ml_context.ML Sat Aug 09 22:43:46 2008 +0200
14.3 @@ -118,7 +118,7 @@
14.4 structure P = OuterParse;
14.5
14.6 val antiq =
14.7 - P.!!! (P.position P.xname -- P.arguments --| Scan.ahead P.eof)
14.8 + P.!!! (P.position P.xname -- Args.parse --| Scan.ahead P.eof)
14.9 >> (fn ((x, pos), y) => Args.src ((x, y), pos));
14.10
14.11 fun eval_antiquotes struct_name (txt, pos) opt_ctxt =
15.1 --- a/src/Pure/ML/ml_thms.ML Sat Aug 09 12:28:13 2008 +0200
15.2 +++ b/src/Pure/ML/ml_thms.ML Sat Aug 09 22:43:46 2008 +0200
15.3 @@ -49,12 +49,12 @@
15.4
15.5 (* ad-hoc goals *)
15.6
15.7 -fun by x = Scan.lift (Args.$$$ "by") x;
15.8 -val goal = Scan.unless by Args.prop;
15.9 +val by = Args.$$$ "by";
15.10 +val goal = Scan.unless (Scan.lift by) Args.prop;
15.11
15.12 val _ = ML_Context.add_antiq "lemma"
15.13 - ((Args.context -- Args.mode "open" -- Scan.repeat1 goal --
15.14 - (by |-- Scan.lift Method.parse_args -- Scan.option (Scan.lift Method.parse_args))) >>
15.15 + (Args.context -- Args.mode "open" -- Scan.repeat1 goal --
15.16 + Scan.lift (by |-- Method.parse -- Scan.option Method.parse) >>
15.17 (fn (((ctxt, is_open), props), methods) => fn {struct_name, background} =>
15.18 let
15.19 val i = serial ();
16.1 --- a/src/Pure/Thy/latex.ML Sat Aug 09 12:28:13 2008 +0200
16.2 +++ b/src/Pure/Thy/latex.ML Sat Aug 09 22:43:46 2008 +0200
16.3 @@ -107,7 +107,7 @@
16.4 val invisible_token = T.keyword_with (equal ";") orf T.is_kind T.Comment;
16.5
16.6 fun output_basic tok =
16.7 - let val s = T.val_of tok in
16.8 + let val s = T.content_of tok in
16.9 if invisible_token tok then ""
16.10 else if T.is_kind T.Command tok then
16.11 "\\isacommand{" ^ output_syms s ^ "}"
17.1 --- a/src/Pure/Thy/thy_output.ML Sat Aug 09 12:28:13 2008 +0200
17.2 +++ b/src/Pure/Thy/thy_output.ML Sat Aug 09 22:43:46 2008 +0200
17.3 @@ -135,7 +135,7 @@
17.4
17.5 in
17.6
17.7 -val antiq = P.!!! (P.position P.xname -- properties -- P.arguments --| Scan.ahead P.eof)
17.8 +val antiq = P.!!! (P.position P.xname -- properties -- Args.parse --| Scan.ahead P.eof)
17.9 >> (fn (((x, pos), y), z) => (y, Args.src ((x, z), pos)));
17.10
17.11 end;
17.12 @@ -332,18 +332,18 @@
17.13 >> (fn d => (NONE, (NoToken, ("", d))));
17.14
17.15 fun markup mark mk flag = Scan.peek (fn d =>
17.16 - improper |-- P.position (Scan.one (T.is_kind T.Command andf is_markup mark o T.val_of)) --
17.17 + improper |-- P.position (Scan.one (T.is_kind T.Command andf is_markup mark o T.content_of)) --
17.18 Scan.repeat tag --
17.19 P.!!!! ((improper -- locale -- improper) |-- P.position P.text --| improper_end)
17.20 >> (fn (((tok, pos), tags), txt) =>
17.21 - let val name = T.val_of tok
17.22 + let val name = T.content_of tok
17.23 in (SOME (name, pos, tags), (mk (name, txt), (flag, d))) end));
17.24
17.25 val command = Scan.peek (fn d =>
17.26 P.position (Scan.one (T.is_kind T.Command)) --
17.27 Scan.repeat tag
17.28 >> (fn ((tok, pos), tags) =>
17.29 - let val name = T.val_of tok
17.30 + let val name = T.content_of tok
17.31 in (SOME (name, pos, tags), (BasicToken tok, (Latex.markup_false, d))) end));
17.32
17.33 val cmt = Scan.peek (fn d =>
17.34 @@ -428,7 +428,7 @@
17.35
17.36 (* basic pretty printing *)
17.37
17.38 -val str_of_source = space_implode " " o map Args.string_of o #2 o #1 o Args.dest_src;
17.39 +val str_of_source = space_implode " " o map T.unparse o #2 o #1 o Args.dest_src;
17.40
17.41 fun tweak_line s =
17.42 if ! display then s else Symbol.strip_blanks s;
17.43 @@ -527,7 +527,7 @@
17.44 in pretty_term ctxt prop end;
17.45
17.46 val embedded_lemma =
17.47 - args (Args.prop -- Scan.lift (Args.$$$ "by" |-- Method.parse_args -- Scan.option Method.parse_args))
17.48 + args (Args.prop -- Scan.lift (Args.$$$ "by" |-- Method.parse -- Scan.option Method.parse))
17.49 (output pretty_lemma o (fn ((a, arg :: _), p) => (Args.src ((a, [arg]), p))) o Args.dest_src);
17.50
17.51
17.52 @@ -553,8 +553,8 @@
17.53 ("prf", args Attrib.thms (output (pretty_prf false))),
17.54 ("full_prf", args Attrib.thms (output (pretty_prf true))),
17.55 ("theory", args (Scan.lift Args.name) (output pretty_theory)),
17.56 - ("ML", args (Scan.lift (Args.position Args.name)) (output_ml ml_val)),
17.57 - ("ML_type", args (Scan.lift (Args.position Args.name)) (output_ml ml_type)),
17.58 - ("ML_struct", args (Scan.lift (Args.position Args.name)) (output_ml ml_struct))];
17.59 + ("ML", args (Scan.lift (P.position Args.name)) (output_ml ml_val)),
17.60 + ("ML_type", args (Scan.lift (P.position Args.name)) (output_ml ml_type)),
17.61 + ("ML_struct", args (Scan.lift (P.position Args.name)) (output_ml ml_struct))];
17.62
17.63 end;
18.1 --- a/src/Tools/code/code_target.ML Sat Aug 09 12:28:13 2008 +0200
18.2 +++ b/src/Tools/code/code_target.ML Sat Aug 09 22:43:46 2008 +0200
18.3 @@ -318,7 +318,7 @@
18.4 fun serialize thy = mount_serializer thy NONE;
18.5
18.6 fun parse_args f args =
18.7 - case Scan.read Args.stopper f args
18.8 + case Scan.read OuterLex.stopper f args
18.9 of SOME x => x
18.10 | NONE => error "Bad serializer arguments";
18.11
18.12 @@ -2243,7 +2243,7 @@
18.13 -- Scan.repeat (P.$$$ inK |-- P.name
18.14 -- Scan.option (P.$$$ module_nameK |-- P.name)
18.15 -- Scan.option (P.$$$ fileK |-- P.name)
18.16 - -- Scan.optional (P.$$$ "(" |-- P.arguments --| P.$$$ ")") []
18.17 + -- Scan.optional (P.$$$ "(" |-- Args.parse --| P.$$$ ")") []
18.18 ) >> (fn (raw_cs, seris) => cmd raw_cs seris));
18.19
18.20 val _ = List.app OuterKeyword.keyword [infixK, infixlK, infixrK, inK, module_nameK, fileK];
19.1 --- a/src/Tools/induct.ML Sat Aug 09 12:28:13 2008 +0200
19.2 +++ b/src/Tools/induct.ML Sat Aug 09 22:43:46 2008 +0200
19.3 @@ -686,6 +686,8 @@
19.4
19.5 (** concrete syntax **)
19.6
19.7 +structure P = OuterParse;
19.8 +
19.9 val arbitraryN = "arbitrary";
19.10 val takingN = "taking";
19.11 val ruleN = "rule";
19.12 @@ -726,7 +728,7 @@
19.13 Args.$$$ predN || Args.$$$ setN || Args.$$$ ruleN) -- Args.colon)) scan;
19.14
19.15 val arbitrary = Scan.optional (Scan.lift (Args.$$$ arbitraryN -- Args.colon) |--
19.16 - Args.and_list1 (Scan.repeat (unless_more_args free))) [];
19.17 + P.and_list1' (Scan.repeat (unless_more_args free))) [];
19.18
19.19 val taking = Scan.optional (Scan.lift (Args.$$$ takingN -- Args.colon) |--
19.20 Scan.repeat1 (unless_more_args inst)) [];
19.21 @@ -734,13 +736,13 @@
19.22 in
19.23
19.24 fun cases_meth src =
19.25 - Method.syntax (Args.and_list (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule) src
19.26 + Method.syntax (P.and_list' (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule) src
19.27 #> (fn ((insts, opt_rule), ctxt) =>
19.28 Method.METHOD_CASES (fn facts =>
19.29 Seq.DETERM (HEADGOAL (cases_tac ctxt insts opt_rule facts))));
19.30
19.31 fun induct_meth src =
19.32 - Method.syntax (Args.and_list (Scan.repeat (unless_more_args def_inst)) --
19.33 + Method.syntax (P.and_list' (Scan.repeat (unless_more_args def_inst)) --
19.34 (arbitrary -- taking -- Scan.option induct_rule)) src
19.35 #> (fn ((insts, ((arbitrary, taking), opt_rule)), ctxt) =>
19.36 Method.RAW_METHOD_CASES (fn facts =>
20.1 --- a/src/Tools/induct_tacs.ML Sat Aug 09 12:28:13 2008 +0200
20.2 +++ b/src/Tools/induct_tacs.ML Sat Aug 09 22:43:46 2008 +0200
20.3 @@ -117,7 +117,7 @@
20.4 val opt_rules = Scan.option (rule_spec |-- Attrib.thms);
20.5
20.6 val varss =
20.7 - Args.and_list (Scan.repeat (Scan.unless rule_spec (Scan.lift (Args.maybe Args.name))));
20.8 + OuterParse.and_list' (Scan.repeat (Scan.unless rule_spec (Scan.lift (Args.maybe Args.name))));
20.9
20.10 in
20.11