--- a/doc-src/antiquote_setup.ML Sat Aug 09 12:28:13 2008 +0200
+++ b/doc-src/antiquote_setup.ML Sat Aug 09 22:43:46 2008 +0200
@@ -30,7 +30,7 @@
| clean_name "}" = "braceright"
| clean_name s = s |> translate_string (fn "_" => "-" | c => c);
-val str_of_source = space_implode " " o map Args.string_of o #2 o #1 o Args.dest_src;
+val str_of_source = space_implode " " o map OuterLex.unparse o #2 o #1 o Args.dest_src;
fun tweak_line s =
if ! O.display then s else Symbol.strip_blanks s;
--- a/src/FOL/ex/IffOracle.thy Sat Aug 09 12:28:13 2008 +0200
+++ b/src/FOL/ex/IffOracle.thy Sat Aug 09 22:43:46 2008 +0200
@@ -53,7 +53,7 @@
subsection {* Oracle as proof method *}
method_setup iff = {*
- Method.simple_args Args.nat (fn n => fn ctxt =>
+ Method.simple_args OuterParse.nat (fn n => fn ctxt =>
Method.SIMPLE_METHOD
(HEADGOAL (Tactic.rtac (iff_oracle (ProofContext.theory_of ctxt) n))
handle Fail _ => no_tac))
--- a/src/HOL/Nominal/nominal_induct.ML Sat Aug 09 12:28:13 2008 +0200
+++ b/src/HOL/Nominal/nominal_induct.ML Sat Aug 09 22:43:46 2008 +0200
@@ -123,6 +123,8 @@
local
+structure P = OuterParse;
+
val avoidingN = "avoiding";
val fixingN = "arbitrary"; (* to be consistent with induct; hopefully this changes again *)
val ruleN = "rule";
@@ -145,7 +147,7 @@
Scan.repeat (unless_more_args free)) [];
val fixing = Scan.optional (Scan.lift (Args.$$$ fixingN -- Args.colon) |--
- Args.and_list (Scan.repeat (unless_more_args free))) [];
+ P.and_list' (Scan.repeat (unless_more_args free))) [];
val rule_spec = Scan.lift (Args.$$$ "rule" -- Args.colon) |-- Attrib.thms;
@@ -153,7 +155,7 @@
fun nominal_induct_method src =
Method.syntax
- (Args.and_list (Scan.repeat (unless_more_args def_inst)) --
+ (P.and_list' (Scan.repeat (unless_more_args def_inst)) --
avoiding -- fixing -- rule_spec) src
#> (fn ((((x, y), z), w), ctxt) =>
Method.RAW_METHOD_CASES (fn facts =>
--- a/src/HOL/Tools/inductive_codegen.ML Sat Aug 09 12:28:13 2008 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML Sat Aug 09 22:43:46 2008 +0200
@@ -697,6 +697,6 @@
val setup =
add_codegen "inductive" inductive_codegen #>
Code.add_attribute ("ind", Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) --
- Scan.option (Args.$$$ "params" |-- Args.colon |-- Args.nat) >> uncurry add);
+ Scan.option (Args.$$$ "params" |-- Args.colon |-- OuterParse.nat) >> uncurry add);
end;
--- a/src/HOL/Tools/recdef_package.ML Sat Aug 09 12:28:13 2008 +0200
+++ b/src/HOL/Tools/recdef_package.ML Sat Aug 09 22:43:46 2008 +0200
@@ -295,7 +295,7 @@
val _ = List.app OuterKeyword.keyword ["permissive", "congs", "hints"];
val hints =
- P.$$$ "(" |-- P.!!! (P.position (P.$$$ "hints" -- P.arguments) --| P.$$$ ")") >> Args.src;
+ P.$$$ "(" |-- P.!!! (P.position (P.$$$ "hints" -- Args.parse) --| P.$$$ ")") >> Args.src;
val recdef_decl =
Scan.optional (P.$$$ "(" -- P.!!! (P.$$$ "permissive" -- P.$$$ ")") >> K false) true --
--- a/src/HOL/Tools/res_axioms.ML Sat Aug 09 12:28:13 2008 +0200
+++ b/src/HOL/Tools/res_axioms.ML Sat Aug 09 22:43:46 2008 +0200
@@ -557,7 +557,7 @@
(** Attribute for converting a theorem into clauses **)
-val clausify = Attrib.syntax (Scan.lift Args.nat
+val clausify = Attrib.syntax (Scan.lift OuterParse.nat
>> (fn i => Thm.rule_attribute (fn context => fn th =>
Meson.make_meta_clause (nth (cnf_axiom (Context.theory_of context) th) i))));
--- a/src/HOL/Tools/split_rule.ML Sat Aug 09 12:28:13 2008 +0200
+++ b/src/HOL/Tools/split_rule.ML Sat Aug 09 22:43:46 2008 +0200
@@ -146,12 +146,11 @@
(* FIXME dynamically scoped due to Args.name/pair_tac *)
-val split_format = Attrib.syntax
- (Scan.lift (Args.parens (Args.$$$ "complete"))
- >> K (Thm.rule_attribute (K complete_split_rule)) ||
- Args.and_list1 (Scan.lift (Scan.repeat Args.name))
+val split_format = Attrib.syntax (Scan.lift
+ (Args.parens (Args.$$$ "complete") >> K (Thm.rule_attribute (K complete_split_rule)) ||
+ OuterParse.and_list1 (Scan.repeat Args.name)
>> (fn xss => Thm.rule_attribute (fn context =>
- split_rule_goal (Context.proof_of context) xss)));
+ split_rule_goal (Context.proof_of context) xss))));
val setup =
Attrib.add_attributes
--- a/src/Provers/blast.ML Sat Aug 09 12:28:13 2008 +0200
+++ b/src/Provers/blast.ML Sat Aug 09 22:43:46 2008 +0200
@@ -1307,7 +1307,7 @@
(** method setup **)
val blast_method =
- Method.bang_sectioned_args' Data.cla_modifiers (Scan.lift (Scan.option Args.nat))
+ Method.bang_sectioned_args' Data.cla_modifiers (Scan.lift (Scan.option OuterParse.nat))
(fn NONE => Data.cla_meth' blast_tac
| SOME lim => Data.cla_meth' (fn cs => depth_tac cs lim));
--- a/src/Provers/clasimp.ML Sat Aug 09 12:28:13 2008 +0200
+++ b/src/Provers/clasimp.ML Sat Aug 09 22:43:46 2008 +0200
@@ -302,7 +302,8 @@
fun auto_args m =
- Method.bang_sectioned_args' clasimp_modifiers (Scan.lift (Scan.option (Args.nat -- Args.nat))) m;
+ Method.bang_sectioned_args' clasimp_modifiers
+ (Scan.lift (Scan.option (OuterParse.nat -- OuterParse.nat))) m;
fun auto_meth NONE = clasimp_meth (CHANGED_PROP o auto_tac)
| auto_meth (SOME (m, n)) = clasimp_meth (CHANGED_PROP o (fn css => mk_auto_tac css m n));
--- a/src/Provers/eqsubst.ML Sat Aug 09 12:28:13 2008 +0200
+++ b/src/Provers/eqsubst.ML Sat Aug 09 22:43:46 2008 +0200
@@ -559,8 +559,7 @@
(Scan.succeed false);
val ith_syntax =
- (Args.parens (Scan.repeat Args.nat))
- || (Scan.succeed [0]);
+ Scan.optional (Args.parens (Scan.repeat OuterParse.nat)) [0];
(* combination method that takes a flag (true indicates that subst
should be done to an assumption, false = apply to the conclusion of
--- a/src/Pure/Isar/context_rules.ML Sat Aug 09 12:28:13 2008 +0200
+++ b/src/Pure/Isar/context_rules.ML Sat Aug 09 22:43:46 2008 +0200
@@ -205,8 +205,8 @@
(* concrete syntax *)
fun add_args a b c = Attrib.syntax
- (Scan.lift ((Args.bang >> K a || Args.query >> K c || Scan.succeed b) -- Scan.option Args.nat)
- >> (fn (f, n) => f n));
+ (Scan.lift ((Args.bang >> K a || Args.query >> K c || Scan.succeed b) --
+ Scan.option OuterParse.nat) >> (fn (f, n) => f n));
val rule_atts =
[("intro", add_args intro_bang intro intro_query, "declaration of introduction rule"),
--- a/src/Pure/Isar/rule_insts.ML Sat Aug 09 12:28:13 2008 +0200
+++ b/src/Pure/Isar/rule_insts.ML Sat Aug 09 22:43:46 2008 +0200
@@ -28,6 +28,9 @@
structure RuleInsts: RULE_INSTS =
struct
+structure T = OuterLex;
+structure P = OuterParse;
+
(** reading instantiations **)
@@ -97,11 +100,11 @@
val (type_insts, term_insts) = List.partition (is_tvar o fst) mixed_insts;
val internal_insts = term_insts |> map_filter
- (fn (xi, Args.Term t) => SOME (xi, t)
- | (_, Args.Text _) => NONE
+ (fn (xi, T.Term t) => SOME (xi, t)
+ | (_, T.Text _) => NONE
| (xi, _) => error_var "Term argument expected for " xi);
val external_insts = term_insts |> map_filter
- (fn (xi, Args.Text s) => SOME (xi, s) | _ => NONE);
+ (fn (xi, T.Text s) => SOME (xi, s) | _ => NONE);
(* mixed type instantiations *)
@@ -111,8 +114,8 @@
val S = the_sort tvars xi;
val T =
(case arg of
- Args.Text s => Syntax.read_typ ctxt s
- | Args.Typ T => T
+ T.Text s => Syntax.read_typ ctxt s
+ | T.Typ T => T
| _ => error_var "Type argument expected for " xi);
in
if Sign.of_sort thy (T, S) then ((xi, S), T)
@@ -169,9 +172,9 @@
val _ = (*assign internalized values*)
mixed_insts |> List.app (fn (arg, (xi, _)) =>
if is_tvar xi then
- Args.assign (SOME (Args.Typ (the (AList.lookup (op =) type_insts xi)))) arg
+ T.assign (SOME (T.Typ (the (AList.lookup (op =) type_insts xi)))) arg
else
- Args.assign (SOME (Args.Term (the (AList.lookup (op =) term_insts xi)))) arg);
+ T.assign (SOME (T.Term (the (AList.lookup (op =) term_insts xi)))) arg);
in
Drule.instantiate insts thm |> RuleCases.save thm
end;
@@ -194,7 +197,7 @@
fun read_instantiate ctxt args thm =
read_instantiate_mixed (ctxt |> ProofContext.set_mode ProofContext.mode_schematic) (* FIXME !? *)
- (map (fn (x, y) => (Args.eof, (x, Args.Text y))) args) thm;
+ (map (fn (x, y) => (T.eof, (x, T.Text y))) args) thm;
fun instantiate_tac ctxt args = PRIMITIVE (read_instantiate ctxt args);
@@ -207,16 +210,16 @@
local
val value =
- Args.internal_typ >> Args.Typ ||
- Args.internal_term >> Args.Term ||
- Args.name >> Args.Text;
+ Args.internal_typ >> T.Typ ||
+ Args.internal_term >> T.Term ||
+ Args.name >> T.Text;
-val inst = Args.var -- (Args.$$$ "=" |-- Args.ahead -- value)
+val inst = Args.var -- (Args.$$$ "=" |-- Scan.ahead P.not_eof -- value)
>> (fn (xi, (a, v)) => (a, (xi, v)));
in
-val where_att = Attrib.syntax (Args.and_list (Scan.lift inst) >> (fn args =>
+val where_att = Attrib.syntax (Scan.lift (P.and_list inst) >> (fn args =>
Thm.rule_attribute (fn context => read_instantiate_mixed (Context.proof_of context) args)));
end;
@@ -227,10 +230,10 @@
local
val value =
- Args.internal_term >> Args.Term ||
- Args.name >> Args.Text;
+ Args.internal_term >> T.Term ||
+ Args.name >> T.Text;
-val inst = Args.ahead -- Args.maybe value;
+val inst = Scan.ahead P.not_eof -- Args.maybe value;
val concl = Args.$$$ "concl" -- Args.colon;
val insts =
@@ -406,16 +409,16 @@
val insts =
Scan.optional
- (Args.and_list1 (Scan.lift (Args.name -- (Args.$$$ "=" |-- Args.!!! Args.name))) --|
- Scan.lift (Args.$$$ "in")) [] -- Attrib.thms;
+ (Scan.lift (P.and_list1 (Args.name -- (Args.$$$ "=" |-- P.!!! Args.name)) --| Args.$$$ "in")) []
+ -- Attrib.thms;
fun inst_args f src ctxt =
f ctxt (fst (Method.syntax (Args.goal_spec HEADGOAL -- insts) src ctxt));
val insts_var =
Scan.optional
- (Args.and_list1 (Scan.lift (Args.var -- (Args.$$$ "=" |-- Args.!!! Args.name))) --|
- Scan.lift (Args.$$$ "in")) [] -- Attrib.thms;
+ (Scan.lift (P.and_list1 (Args.var -- (Args.$$$ "=" |-- P.!!! Args.name)) --| Args.$$$ "in")) []
+ -- Attrib.thms;
fun inst_args_var f src ctxt =
f ctxt (fst (Method.syntax (Args.goal_spec HEADGOAL -- insts_var) src ctxt));
--- a/src/Pure/ML/ml_antiquote.ML Sat Aug 09 12:28:13 2008 +0200
+++ b/src/Pure/ML/ml_antiquote.ML Sat Aug 09 22:43:46 2008 +0200
@@ -62,6 +62,9 @@
(** concrete antiquotations **)
+structure P = OuterParse;
+
+
(* misc *)
val _ = value "theory"
@@ -83,11 +86,11 @@
val _ = inline "prop" (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term));
val _ = macro "let" (Args.context --
- Args.and_list1 (Args.and_list1 (Scan.lift Args.name) -- Scan.lift (Args.$$$ "=" |-- Args.name))
+ Scan.lift (P.and_list1 (P.and_list1 Args.name -- (Args.$$$ "=" |-- Args.name)))
>> (fn (ctxt, args) => #2 (ProofContext.match_bind true args ctxt)));
val _ = macro "note" (Args.context :|-- (fn ctxt =>
- Args.and_list1 (Scan.lift (Args.opt_thm_name I "=") -- Attrib.thms >> (fn ((a, srcs), ths) =>
+ P.and_list1' (Scan.lift (Args.opt_thm_name I "=") -- Attrib.thms >> (fn ((a, srcs), ths) =>
((a, map (Attrib.attribute (ProofContext.theory_of ctxt)) srcs), [(ths, [])])))
>> (fn args => #2 (ProofContext.note_thmss_i "" args ctxt))));
@@ -123,8 +126,8 @@
val _ = inline "const_syntax" (const true);
val _ = inline "const"
- (Args.context -- Scan.lift Args.name --
- Scan.optional (Scan.lift (Args.$$$ "(") |-- Args.enum1 "," Args.typ --| Scan.lift (Args.$$$ ")")) []
+ (Args.context -- Scan.lift Args.name -- Scan.optional
+ (Scan.lift (Args.$$$ "(") |-- OuterParse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) []
>> (fn ((ctxt, c), Ts) =>
let val (c, _) = Term.dest_Const (ProofContext.read_const_proper ctxt c)
in ML_Syntax.atomic (ML_Syntax.print_term (ProofContext.mk_const ctxt (c, Ts))) end));
--- a/src/Pure/ML/ml_context.ML Sat Aug 09 12:28:13 2008 +0200
+++ b/src/Pure/ML/ml_context.ML Sat Aug 09 22:43:46 2008 +0200
@@ -118,7 +118,7 @@
structure P = OuterParse;
val antiq =
- P.!!! (P.position P.xname -- P.arguments --| Scan.ahead P.eof)
+ P.!!! (P.position P.xname -- Args.parse --| Scan.ahead P.eof)
>> (fn ((x, pos), y) => Args.src ((x, y), pos));
fun eval_antiquotes struct_name (txt, pos) opt_ctxt =
--- a/src/Pure/ML/ml_thms.ML Sat Aug 09 12:28:13 2008 +0200
+++ b/src/Pure/ML/ml_thms.ML Sat Aug 09 22:43:46 2008 +0200
@@ -49,12 +49,12 @@
(* ad-hoc goals *)
-fun by x = Scan.lift (Args.$$$ "by") x;
-val goal = Scan.unless by Args.prop;
+val by = Args.$$$ "by";
+val goal = Scan.unless (Scan.lift by) Args.prop;
val _ = ML_Context.add_antiq "lemma"
- ((Args.context -- Args.mode "open" -- Scan.repeat1 goal --
- (by |-- Scan.lift Method.parse_args -- Scan.option (Scan.lift Method.parse_args))) >>
+ (Args.context -- Args.mode "open" -- Scan.repeat1 goal --
+ Scan.lift (by |-- Method.parse -- Scan.option Method.parse) >>
(fn (((ctxt, is_open), props), methods) => fn {struct_name, background} =>
let
val i = serial ();
--- a/src/Pure/Thy/latex.ML Sat Aug 09 12:28:13 2008 +0200
+++ b/src/Pure/Thy/latex.ML Sat Aug 09 22:43:46 2008 +0200
@@ -107,7 +107,7 @@
val invisible_token = T.keyword_with (equal ";") orf T.is_kind T.Comment;
fun output_basic tok =
- let val s = T.val_of tok in
+ let val s = T.content_of tok in
if invisible_token tok then ""
else if T.is_kind T.Command tok then
"\\isacommand{" ^ output_syms s ^ "}"
--- a/src/Pure/Thy/thy_output.ML Sat Aug 09 12:28:13 2008 +0200
+++ b/src/Pure/Thy/thy_output.ML Sat Aug 09 22:43:46 2008 +0200
@@ -135,7 +135,7 @@
in
-val antiq = P.!!! (P.position P.xname -- properties -- P.arguments --| Scan.ahead P.eof)
+val antiq = P.!!! (P.position P.xname -- properties -- Args.parse --| Scan.ahead P.eof)
>> (fn (((x, pos), y), z) => (y, Args.src ((x, z), pos)));
end;
@@ -332,18 +332,18 @@
>> (fn d => (NONE, (NoToken, ("", d))));
fun markup mark mk flag = Scan.peek (fn d =>
- improper |-- P.position (Scan.one (T.is_kind T.Command andf is_markup mark o T.val_of)) --
+ improper |-- P.position (Scan.one (T.is_kind T.Command andf is_markup mark o T.content_of)) --
Scan.repeat tag --
P.!!!! ((improper -- locale -- improper) |-- P.position P.text --| improper_end)
>> (fn (((tok, pos), tags), txt) =>
- let val name = T.val_of tok
+ let val name = T.content_of tok
in (SOME (name, pos, tags), (mk (name, txt), (flag, d))) end));
val command = Scan.peek (fn d =>
P.position (Scan.one (T.is_kind T.Command)) --
Scan.repeat tag
>> (fn ((tok, pos), tags) =>
- let val name = T.val_of tok
+ let val name = T.content_of tok
in (SOME (name, pos, tags), (BasicToken tok, (Latex.markup_false, d))) end));
val cmt = Scan.peek (fn d =>
@@ -428,7 +428,7 @@
(* basic pretty printing *)
-val str_of_source = space_implode " " o map Args.string_of o #2 o #1 o Args.dest_src;
+val str_of_source = space_implode " " o map T.unparse o #2 o #1 o Args.dest_src;
fun tweak_line s =
if ! display then s else Symbol.strip_blanks s;
@@ -527,7 +527,7 @@
in pretty_term ctxt prop end;
val embedded_lemma =
- args (Args.prop -- Scan.lift (Args.$$$ "by" |-- Method.parse_args -- Scan.option Method.parse_args))
+ args (Args.prop -- Scan.lift (Args.$$$ "by" |-- Method.parse -- Scan.option Method.parse))
(output pretty_lemma o (fn ((a, arg :: _), p) => (Args.src ((a, [arg]), p))) o Args.dest_src);
@@ -553,8 +553,8 @@
("prf", args Attrib.thms (output (pretty_prf false))),
("full_prf", args Attrib.thms (output (pretty_prf true))),
("theory", args (Scan.lift Args.name) (output pretty_theory)),
- ("ML", args (Scan.lift (Args.position Args.name)) (output_ml ml_val)),
- ("ML_type", args (Scan.lift (Args.position Args.name)) (output_ml ml_type)),
- ("ML_struct", args (Scan.lift (Args.position Args.name)) (output_ml ml_struct))];
+ ("ML", args (Scan.lift (P.position Args.name)) (output_ml ml_val)),
+ ("ML_type", args (Scan.lift (P.position Args.name)) (output_ml ml_type)),
+ ("ML_struct", args (Scan.lift (P.position Args.name)) (output_ml ml_struct))];
end;
--- a/src/Tools/code/code_target.ML Sat Aug 09 12:28:13 2008 +0200
+++ b/src/Tools/code/code_target.ML Sat Aug 09 22:43:46 2008 +0200
@@ -318,7 +318,7 @@
fun serialize thy = mount_serializer thy NONE;
fun parse_args f args =
- case Scan.read Args.stopper f args
+ case Scan.read OuterLex.stopper f args
of SOME x => x
| NONE => error "Bad serializer arguments";
@@ -2243,7 +2243,7 @@
-- Scan.repeat (P.$$$ inK |-- P.name
-- Scan.option (P.$$$ module_nameK |-- P.name)
-- Scan.option (P.$$$ fileK |-- P.name)
- -- Scan.optional (P.$$$ "(" |-- P.arguments --| P.$$$ ")") []
+ -- Scan.optional (P.$$$ "(" |-- Args.parse --| P.$$$ ")") []
) >> (fn (raw_cs, seris) => cmd raw_cs seris));
val _ = List.app OuterKeyword.keyword [infixK, infixlK, infixrK, inK, module_nameK, fileK];
--- a/src/Tools/induct.ML Sat Aug 09 12:28:13 2008 +0200
+++ b/src/Tools/induct.ML Sat Aug 09 22:43:46 2008 +0200
@@ -686,6 +686,8 @@
(** concrete syntax **)
+structure P = OuterParse;
+
val arbitraryN = "arbitrary";
val takingN = "taking";
val ruleN = "rule";
@@ -726,7 +728,7 @@
Args.$$$ predN || Args.$$$ setN || Args.$$$ ruleN) -- Args.colon)) scan;
val arbitrary = Scan.optional (Scan.lift (Args.$$$ arbitraryN -- Args.colon) |--
- Args.and_list1 (Scan.repeat (unless_more_args free))) [];
+ P.and_list1' (Scan.repeat (unless_more_args free))) [];
val taking = Scan.optional (Scan.lift (Args.$$$ takingN -- Args.colon) |--
Scan.repeat1 (unless_more_args inst)) [];
@@ -734,13 +736,13 @@
in
fun cases_meth src =
- Method.syntax (Args.and_list (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule) src
+ Method.syntax (P.and_list' (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule) src
#> (fn ((insts, opt_rule), ctxt) =>
Method.METHOD_CASES (fn facts =>
Seq.DETERM (HEADGOAL (cases_tac ctxt insts opt_rule facts))));
fun induct_meth src =
- Method.syntax (Args.and_list (Scan.repeat (unless_more_args def_inst)) --
+ Method.syntax (P.and_list' (Scan.repeat (unless_more_args def_inst)) --
(arbitrary -- taking -- Scan.option induct_rule)) src
#> (fn ((insts, ((arbitrary, taking), opt_rule)), ctxt) =>
Method.RAW_METHOD_CASES (fn facts =>
--- a/src/Tools/induct_tacs.ML Sat Aug 09 12:28:13 2008 +0200
+++ b/src/Tools/induct_tacs.ML Sat Aug 09 22:43:46 2008 +0200
@@ -117,7 +117,7 @@
val opt_rules = Scan.option (rule_spec |-- Attrib.thms);
val varss =
- Args.and_list (Scan.repeat (Scan.unless rule_spec (Scan.lift (Args.maybe Args.name))));
+ OuterParse.and_list' (Scan.repeat (Scan.unless rule_spec (Scan.lift (Args.maybe Args.name))));
in