--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Aug 19 18:21:29 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Aug 19 23:17:51 2014 +0200
@@ -21,17 +21,17 @@
val nesting_bnfs: Proof.context -> typ list list list -> typ list -> BNF_Def.bnf list
type lfp_sugar_thms =
- (thm list * thm * Args.src list) * (thm list list * Args.src list)
+ (thm list * thm * Token.src list) * (thm list list * Token.src list)
val morph_lfp_sugar_thms: morphism -> lfp_sugar_thms -> lfp_sugar_thms
val transfer_lfp_sugar_thms: Proof.context -> lfp_sugar_thms -> lfp_sugar_thms
type gfp_sugar_thms =
- ((thm list * thm) list * (Args.src list * Args.src list))
+ ((thm list * thm) list * (Token.src list * Token.src list))
* thm list list
* thm list list
- * (thm list list * Args.src list)
- * (thm list list list * Args.src list)
+ * (thm list list * Token.src list)
+ * (thm list list list * Token.src list)
val morph_gfp_sugar_thms: morphism -> gfp_sugar_thms -> gfp_sugar_thms
val transfer_gfp_sugar_thms: Proof.context -> gfp_sugar_thms -> gfp_sugar_thms
@@ -304,7 +304,7 @@
fun indexify proj xs f p = f (find_index (curry (op =) (proj p)) xs) p;
type lfp_sugar_thms =
- (thm list * thm * Args.src list) * (thm list list * Args.src list);
+ (thm list * thm * Token.src list) * (thm list list * Token.src list);
fun morph_lfp_sugar_thms phi ((inducts, induct, induct_attrs), (recss, rec_attrs)) =
((map (Morphism.thm phi) inducts, Morphism.thm phi induct, induct_attrs),
@@ -315,11 +315,11 @@
morph_lfp_sugar_thms o Morphism.transfer_morphism o Proof_Context.theory_of;
type gfp_sugar_thms =
- ((thm list * thm) list * (Args.src list * Args.src list))
+ ((thm list * thm) list * (Token.src list * Token.src list))
* thm list list
* thm list list
- * (thm list list * Args.src list)
- * (thm list list list * Args.src list);
+ * (thm list list * Token.src list)
+ * (thm list list list * Token.src list);
fun morph_gfp_sugar_thms phi ((coinducts_pairs, coinduct_attrs_pair),
corecss, corec_discss, (corec_disc_iffss, corec_disc_iff_attrs),
--- a/src/HOL/Tools/Function/function_common.ML Tue Aug 19 18:21:29 2014 +0200
+++ b/src/HOL/Tools/Function/function_common.ML Tue Aug 19 23:17:51 2014 +0200
@@ -12,7 +12,7 @@
defname : string,
(* contains no logical entities: invariant under morphisms: *)
add_simps : (binding -> binding) -> string -> (binding -> binding) ->
- Attrib.src list -> thm list -> local_theory -> thm list * local_theory,
+ Token.src list -> thm list -> local_theory -> thm list * local_theory,
fnames : string list,
case_names : string list,
fs : term list,
@@ -37,7 +37,7 @@
defname : string,
(* contains no logical entities: invariant under morphisms: *)
add_simps : (binding -> binding) -> string -> (binding -> binding) ->
- Attrib.src list -> thm list -> local_theory -> thm list * local_theory,
+ Token.src list -> thm list -> local_theory -> thm list * local_theory,
fnames : string list,
case_names : string list,
fs : term list,
--- a/src/HOL/Tools/Lifting/lifting_def.ML Tue Aug 19 18:21:29 2014 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML Tue Aug 19 23:17:51 2014 +0200
@@ -13,7 +13,8 @@
(binding * mixfix) -> typ -> term -> thm -> thm list -> local_theory -> local_theory
val lift_def_cmd:
- (binding * string option * mixfix) * string * (Facts.ref * Args.src list) list -> local_theory -> Proof.state
+ (binding * string option * mixfix) * string * (Facts.ref * Token.src list) list ->
+ local_theory -> Proof.state
val can_generate_code_cert: thm -> bool
end
--- a/src/HOL/Tools/Lifting/lifting_setup.ML Tue Aug 19 18:21:29 2014 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML Tue Aug 19 23:17:51 2014 +0200
@@ -223,7 +223,7 @@
val dummy_thm = Thm.transfer thy Drule.dummy_thm
val pointer = Outer_Syntax.scan (Keyword.get_lexicons ()) Position.none bundle_name
val restore_lifting_att =
- ([dummy_thm], [Args.src ("Lifting.lifting_restore_internal", Position.none) pointer])
+ ([dummy_thm], [Token.src ("Lifting.lifting_restore_internal", Position.none) pointer])
in
lthy
|> Local_Theory.declaration {syntax = false, pervasive = true}
@@ -969,7 +969,7 @@
case bundle of
[(_, [arg_src])] =>
let
- val (name, _) = Args.syntax (Scan.lift Args.name) arg_src ctxt
+ val (name, _) = Token.syntax (Scan.lift Args.name) arg_src ctxt
handle ERROR _ => error "The provided bundle is not a lifting bundle."
in name end
| _ => error "The provided bundle is not a lifting bundle."
--- a/src/HOL/Tools/Quotient/quotient_type.ML Tue Aug 19 18:21:29 2014 +0200
+++ b/src/HOL/Tools/Quotient/quotient_type.ML Tue Aug 19 23:17:51 2014 +0200
@@ -13,7 +13,7 @@
((binding * binding) option * bool * thm option) -> Proof.context -> Proof.state
val quotient_type_cmd: ((((((bool * string list) * binding) * mixfix) * string) * (bool * string)) *
- (binding * binding) option) * (Facts.ref * Args.src list) option -> Proof.context -> Proof.state
+ (binding * binding) option) * (Facts.ref * Token.src list) option -> Proof.context -> Proof.state
end;
structure Quotient_Type: QUOTIENT_TYPE =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Tue Aug 19 18:21:29 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Tue Aug 19 23:17:51 2014 +0200
@@ -14,15 +14,15 @@
type fact = (string * stature) * thm
type fact_override =
- {add : (Facts.ref * Attrib.src list) list,
- del : (Facts.ref * Attrib.src list) list,
+ {add : (Facts.ref * Token.src list) list,
+ del : (Facts.ref * Token.src list) list,
only : bool}
val instantiate_inducts : bool Config.T
val no_fact_override : fact_override
val fact_of_ref : Proof.context -> unit Symtab.table -> thm list -> status Termtab.table ->
- Facts.ref * Attrib.src list -> ((string * stature) * thm) list
+ Facts.ref * Token.src list -> ((string * stature) * thm) list
val backquote_thm : Proof.context -> thm -> string
val is_blacklisted_or_something : Proof.context -> bool -> string -> bool
val clasimpset_rule_table_of : Proof.context -> status Termtab.table
@@ -50,8 +50,8 @@
type fact = (string * stature) * thm
type fact_override =
- {add : (Facts.ref * Attrib.src list) list,
- del : (Facts.ref * Attrib.src list) list,
+ {add : (Facts.ref * Token.src list) list,
+ del : (Facts.ref * Token.src list) list,
only : bool}
(* gracefully handle huge background theories *)
@@ -159,7 +159,7 @@
fun fact_of_ref ctxt reserved chained css (xthm as (xref, args)) =
let
val ths = Attrib.eval_thms ctxt [xthm]
- val bracket = implode (map (enclose "[" "]" o Pretty.str_of o Args.pretty_src ctxt) args)
+ val bracket = implode (map (enclose "[" "]" o Pretty.str_of o Token.pretty_src ctxt) args)
fun nth_name j =
(case xref of
--- a/src/HOL/Tools/inductive.ML Tue Aug 19 18:21:29 2014 +0200
+++ b/src/HOL/Tools/inductive.ML Tue Aug 19 23:17:51 2014 +0200
@@ -53,7 +53,7 @@
(binding * string option * mixfix) list ->
(binding * string option * mixfix) list ->
(Attrib.binding * string) list ->
- (Facts.ref * Attrib.src list) list ->
+ (Facts.ref * Token.src list) list ->
local_theory -> inductive_result * local_theory
val add_inductive_global: inductive_flags ->
((binding * typ) * mixfix) list -> (string * typ) list -> (Attrib.binding * term) list ->
@@ -76,7 +76,7 @@
term list -> (binding * mixfix) list ->
local_theory -> inductive_result * local_theory
val declare_rules: binding -> bool -> bool -> string list -> term list ->
- thm list -> binding list -> Attrib.src list list -> (thm * string list * int) list ->
+ thm list -> binding list -> Token.src list list -> (thm * string list * int) list ->
thm list -> thm -> local_theory -> thm list * thm list * thm list * thm * thm list * local_theory
val add_ind_def: add_ind_def
val gen_add_inductive_i: add_ind_def -> inductive_flags ->
@@ -85,7 +85,7 @@
val gen_add_inductive: add_ind_def -> bool -> bool ->
(binding * string option * mixfix) list ->
(binding * string option * mixfix) list ->
- (Attrib.binding * string) list -> (Facts.ref * Attrib.src list) list ->
+ (Attrib.binding * string) list -> (Facts.ref * Token.src list) list ->
local_theory -> inductive_result * local_theory
val gen_ind_decl: add_ind_def -> bool -> (local_theory -> local_theory) parser
end;
--- a/src/HOL/Tools/inductive_set.ML Tue Aug 19 18:21:29 2014 +0200
+++ b/src/HOL/Tools/inductive_set.ML Tue Aug 19 23:17:51 2014 +0200
@@ -20,7 +20,7 @@
val add_inductive: bool -> bool ->
(binding * string option * mixfix) list ->
(binding * string option * mixfix) list ->
- (Attrib.binding * string) list -> (Facts.ref * Attrib.src list) list ->
+ (Attrib.binding * string) list -> (Facts.ref * Token.src list) list ->
local_theory -> Inductive.inductive_result * local_theory
val mono_add: attribute
val mono_del: attribute
--- a/src/HOL/Tools/recdef.ML Tue Aug 19 18:21:29 2014 +0200
+++ b/src/HOL/Tools/recdef.ML Tue Aug 19 23:17:51 2014 +0200
@@ -15,17 +15,17 @@
val cong_del: attribute
val wf_add: attribute
val wf_del: attribute
- val add_recdef: bool -> xstring -> string -> ((binding * string) * Attrib.src list) list ->
- Attrib.src option -> theory -> theory
+ val add_recdef: bool -> xstring -> string -> ((binding * string) * Token.src list) list ->
+ Token.src option -> theory -> theory
* {lhs: term, simps: thm list, rules: thm list list, induct: thm, tcs: term list}
val add_recdef_i: bool -> xstring -> term -> ((binding * term) * attribute list) list ->
theory -> theory * {lhs: term, simps: thm list, rules: thm list list, induct: thm, tcs: term list}
- val defer_recdef: xstring -> string list -> (Facts.ref * Attrib.src list) list
+ val defer_recdef: xstring -> string list -> (Facts.ref * Token.src list) list
-> theory -> theory * {induct_rules: thm}
val defer_recdef_i: xstring -> term list -> thm list -> theory -> theory * {induct_rules: thm}
- val recdef_tc: bstring * Attrib.src list -> xstring -> int option -> bool ->
+ val recdef_tc: bstring * Token.src list -> xstring -> int option -> bool ->
local_theory -> Proof.state
- val recdef_tc_i: bstring * Attrib.src list -> string -> int option -> bool ->
+ val recdef_tc_i: bstring * Token.src list -> string -> int option -> bool ->
local_theory -> Proof.state
val setup: theory -> theory
end;
@@ -164,7 +164,7 @@
val ctxt =
(case opt_src of
NONE => ctxt0
- | SOME src => #2 (Args.syntax (Method.sections recdef_modifiers) src ctxt0));
+ | SOME src => #2 (Token.syntax (Method.sections recdef_modifiers) src ctxt0));
val {simps, congs, wfs} = get_hints ctxt;
val ctxt' = ctxt addsimps simps |> Simplifier.del_cong @{thm imp_cong};
in (ctxt', rev (map snd congs), wfs) end;
@@ -292,7 +292,7 @@
val hints =
@{keyword "("} |--
Parse.!!! (Parse.position @{keyword "hints"} -- Parse.args --| @{keyword ")"})
- >> uncurry Args.src;
+ >> uncurry Token.src;
val recdef_decl =
Scan.optional
--- a/src/HOL/Tools/try0.ML Tue Aug 19 18:21:29 2014 +0200
+++ b/src/HOL/Tools/try0.ML Tue Aug 19 23:17:51 2014 +0200
@@ -173,7 +173,7 @@
fun string_of_xthm (xref, args) =
Facts.string_of_ref xref ^
- implode (map (enclose "[" "]" o Pretty.str_of o Args.pretty_src @{context}) args);
+ implode (map (enclose "[" "]" o Pretty.str_of o Token.pretty_src @{context}) args);
val parse_fact_refs =
Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) (Parse_Spec.xthm >> string_of_xthm));
--- a/src/Pure/Isar/args.ML Tue Aug 19 18:21:29 2014 +0200
+++ b/src/Pure/Isar/args.ML Tue Aug 19 23:17:51 2014 +0200
@@ -1,22 +1,12 @@
(* Title: Pure/Isar/args.ML
Author: Markus Wenzel, TU Muenchen
-Parsing with implicit value assignment. Concrete argument syntax of
+Quasi-inner syntax based on outer tokens: concrete argument syntax of
attributes, methods etc.
*)
signature ARGS =
sig
- type src
- val src: xstring * Position.T -> Token.T list -> src
- val name_of_src: src -> string * Position.T
- val range_of_src: src -> Position.T
- val unparse_src: src -> string list
- val pretty_src: Proof.context -> src -> Pretty.T
- val check_src: Proof.context -> 'a Name_Space.table -> src -> src * 'a
- val transform_values: morphism -> src -> src
- val init_assignable: src -> src
- val closure: src -> src
val context: Proof.context context_parser
val theory: theory context_parser
val $$$ : string -> string parser
@@ -62,67 +52,13 @@
val type_name: {proper: bool, strict: bool} -> string context_parser
val const: {proper: bool, strict: bool} -> string context_parser
val goal_spec: ((int -> tactic) -> tactic) context_parser
- val attribs: (xstring * Position.T -> string) -> src list parser
- val opt_attribs: (xstring * Position.T -> string) -> src list parser
- val syntax_generic: 'a context_parser -> src -> Context.generic -> 'a * Context.generic
- val syntax: 'a context_parser -> src -> Proof.context -> 'a * Proof.context
+ val attribs: (xstring * Position.T -> string) -> Token.src list parser
+ val opt_attribs: (xstring * Position.T -> string) -> Token.src list parser
end;
structure Args: ARGS =
struct
-(** datatype src **)
-
-datatype src =
- Src of
- {name: string * Position.T,
- args: Token.T list,
- output_info: (string * Markup.T) option};
-
-fun src name args = Src {name = name, args = args, output_info = NONE};
-
-fun name_of_src (Src {name, ...}) = name;
-
-fun range_of_src (Src {name = (_, pos), args, ...}) =
- if null args then pos
- else Position.set_range (pos, #2 (Token.range_of args));
-
-fun unparse_src (Src {args, ...}) = map Token.unparse args;
-
-fun pretty_src ctxt src =
- let
- val Src {name = (name, _), args, output_info} = src;
- val prt_name =
- (case output_info of
- NONE => Pretty.str name
- | SOME (_, markup) => Pretty.mark_str (markup, name));
- val prt_arg = Token.pretty_value ctxt;
- in Pretty.block (Pretty.breaks (prt_name :: map prt_arg args)) end;
-
-
-(* check *)
-
-fun check_src ctxt table (Src {name = (xname, pos), args, output_info = _}) =
- let
- val (name, x) = Name_Space.check (Context.Proof ctxt) table (xname, pos);
- val space = Name_Space.space_of_table table;
- val kind = Name_Space.kind_of space;
- val markup = Name_Space.markup space name;
- in (Src {name = (name, pos), args = args, output_info = SOME (kind, markup)}, x) end;
-
-
-(* values *)
-
-fun map_args f (Src {name, args, output_info}) =
- Src {name = name, args = map f args, output_info = output_info};
-
-val transform_values = map_args o Token.transform_value;
-
-val init_assignable = map_args Token.init_assignable;
-val closure = map_args Token.closure;
-
-
-
(** argument scanners **)
(* context *)
@@ -251,42 +187,9 @@
let
fun intern tok = check (Token.content_of tok, Token.pos_of tok);
val attrib_name = internal_name >> #1 || (symbolic || named) >> evaluate Token.name0 intern;
- val attrib = Parse.position attrib_name -- Parse.!!! Parse.args >> uncurry src;
+ val attrib = Parse.position attrib_name -- Parse.!!! Parse.args >> uncurry Token.src;
in $$$ "[" |-- Parse.!!! (Parse.list attrib --| $$$ "]") end;
fun opt_attribs check = Scan.optional (attribs check) [];
-
-
-(** syntax wrapper **)
-
-fun syntax_generic scan (Src {name = (name, pos), args = args0, output_info}) context =
- let
- val args1 = map Token.init_assignable args0;
- fun reported_text () =
- if Context_Position.is_visible_generic context then
- ((pos, Markup.operator) :: maps (Token.reports_of_value o Token.closure) args1)
- |> map (fn (p, m) => Position.reported_text p m "")
- else [];
- in
- (case Scan.error (Scan.finite' Token.stopper (Scan.option scan)) (context, args1) of
- (SOME x, (context', [])) =>
- let val _ = Output.report (reported_text ())
- in (x, context') end
- | (_, (_, args2)) =>
- let
- val print_name =
- (case output_info of
- NONE => quote name
- | SOME (kind, markup) => plain_words kind ^ " " ^ quote (Markup.markup markup name));
- val print_args =
- if null args2 then "" else ":\n " ^ space_implode " " (map Token.print args2);
- in
- error ("Bad arguments for " ^ print_name ^ Position.here pos ^ print_args ^
- Markup.markup_report (implode (reported_text ())))
- end)
- end;
-
-fun syntax scan src = apsnd Context.the_proof o syntax_generic scan src o Context.Proof;
-
end;
--- a/src/Pure/Isar/attrib.ML Tue Aug 19 18:21:29 2014 +0200
+++ b/src/Pure/Isar/attrib.ML Tue Aug 19 23:17:51 2014 +0200
@@ -6,23 +6,22 @@
signature ATTRIB =
sig
- type src = Args.src
- type binding = binding * src list
+ type binding = binding * Token.src list
val empty_binding: binding
val is_empty_binding: binding -> bool
val print_attributes: Proof.context -> unit
- val define_global: Binding.binding -> (Args.src -> attribute) ->
+ val define_global: Binding.binding -> (Token.src -> attribute) ->
string -> theory -> string * theory
- val define: Binding.binding -> (Args.src -> attribute) ->
+ val define: Binding.binding -> (Token.src -> attribute) ->
string -> local_theory -> string * local_theory
val check_name_generic: Context.generic -> xstring * Position.T -> string
val check_name: Proof.context -> xstring * Position.T -> string
- val check_src: Proof.context -> src -> src
- val pretty_attribs: Proof.context -> src list -> Pretty.T list
- val attribute: Proof.context -> src -> attribute
- val attribute_global: theory -> src -> attribute
- val attribute_cmd: Proof.context -> src -> attribute
- val attribute_cmd_global: theory -> src -> attribute
+ val check_src: Proof.context -> Token.src -> Token.src
+ val pretty_attribs: Proof.context -> Token.src list -> Pretty.T list
+ val attribute: Proof.context -> Token.src -> attribute
+ val attribute_global: theory -> Token.src -> attribute
+ val attribute_cmd: Proof.context -> Token.src -> attribute
+ val attribute_cmd_global: theory -> Token.src -> attribute
val map_specs: ('a list -> 'att list) ->
(('c * 'a list) * 'b) list -> (('c * 'att list) * 'b) list
val map_facts: ('a list -> 'att list) ->
@@ -31,28 +30,28 @@
val map_facts_refs: ('a list -> 'att list) -> ('b -> 'fact) ->
(('c * 'a list) * ('b * 'a list) list) list ->
(('c * 'att list) * ('fact * 'att list) list) list
- val global_notes: string -> (binding * (thm list * src list) list) list ->
+ val global_notes: string -> (binding * (thm list * Token.src list) list) list ->
theory -> (string * thm list) list * theory
- val local_notes: string -> (binding * (thm list * src list) list) list ->
+ val local_notes: string -> (binding * (thm list * Token.src list) list) list ->
Proof.context -> (string * thm list) list * Proof.context
- val generic_notes: string -> (binding * (thm list * src list) list) list ->
+ val generic_notes: string -> (binding * (thm list * Token.src list) list) list ->
Context.generic -> (string * thm list) list * Context.generic
- val eval_thms: Proof.context -> (Facts.ref * src list) list -> thm list
- val attribute_syntax: attribute context_parser -> Args.src -> attribute
+ val eval_thms: Proof.context -> (Facts.ref * Token.src list) list -> thm list
+ val attribute_syntax: attribute context_parser -> Token.src -> attribute
val setup: Binding.binding -> attribute context_parser -> string -> theory -> theory
val local_setup: Binding.binding -> attribute context_parser -> string ->
local_theory -> local_theory
val attribute_setup: bstring * Position.T -> Symbol_Pos.source -> string ->
local_theory -> local_theory
- val internal: (morphism -> attribute) -> src
+ val internal: (morphism -> attribute) -> Token.src
val add_del: attribute -> attribute -> attribute context_parser
val thm_sel: Facts.interval list parser
val thm: thm context_parser
val thms: thm list context_parser
val multi_thm: thm list context_parser
val partial_evaluation: Proof.context ->
- (binding * (thm list * Args.src list) list) list ->
- (binding * (thm list * Args.src list) list) list
+ (binding * (thm list * Token.src list) list) list ->
+ (binding * (thm list * Token.src list) list) list
val print_options: Proof.context -> unit
val config_bool: Binding.binding ->
(Context.generic -> bool) -> bool Config.T * (theory -> theory)
@@ -81,8 +80,7 @@
(* source and bindings *)
-type src = Args.src;
-type binding = binding * src list;
+type binding = binding * Token.src list;
val empty_binding: binding = (Binding.empty, []);
fun is_empty_binding ((b, srcs): binding) = Binding.is_empty b andalso null srcs;
@@ -95,7 +93,7 @@
structure Attributes = Generic_Data
(
- type T = ((src -> attribute) * string) Name_Space.table;
+ type T = ((Token.src -> attribute) * string) Name_Space.table;
val empty : T = Name_Space.empty_table "attribute";
val extend = I;
fun merge data : T = Name_Space.merge_tables data;
@@ -147,21 +145,21 @@
val check_name = check_name_generic o Context.Proof;
fun check_src ctxt src =
- (Context_Position.report ctxt (Args.range_of_src src) Markup.language_attribute;
- #1 (Args.check_src ctxt (get_attributes ctxt) src));
+ (Context_Position.report ctxt (Token.range_of_src src) Markup.language_attribute;
+ #1 (Token.check_src ctxt (get_attributes ctxt) src));
(* pretty printing *)
fun pretty_attribs _ [] = []
- | pretty_attribs ctxt srcs = [Pretty.enum "," "[" "]" (map (Args.pretty_src ctxt) srcs)];
+ | pretty_attribs ctxt srcs = [Pretty.enum "," "[" "]" (map (Token.pretty_src ctxt) srcs)];
(* get attributes *)
fun attribute_generic context =
let val table = Attributes.get context
- in fn src => #1 (Name_Space.get table (#1 (Args.name_of_src src))) src end;
+ in fn src => #1 (Name_Space.get table (#1 (Token.name_of_src src))) src end;
val attribute = attribute_generic o Context.Proof;
val attribute_global = attribute_generic o Context.Theory;
@@ -199,7 +197,7 @@
(* attribute setup *)
fun attribute_syntax scan src (context, th) =
- let val (a, context') = Args.syntax_generic scan src context in a (context', th) end;
+ let val (a, context') = Token.syntax_generic scan src context in a (context', th) end;
fun setup binding scan comment = define_global binding (attribute_syntax scan) comment #> snd;
fun local_setup binding scan comment = define binding (attribute_syntax scan) comment #> snd;
@@ -216,7 +214,7 @@
(* internal attribute *)
-fun internal att = Args.src ("Pure.attribute", Position.none) [Token.mk_attribute att];
+fun internal att = Token.src ("Pure.attribute", Position.none) [Token.mk_attribute att];
val _ = Theory.setup
(setup (Binding.make ("attribute", @{here}))
@@ -287,13 +285,13 @@
fun apply_att src (context, th) =
let
- val src1 = Args.init_assignable src;
+ val src1 = Token.init_assignable_src src;
val result = attribute_generic context src1 (context, th);
- val src2 = Args.closure src1;
+ val src2 = Token.closure_src src1;
in (src2, result) end;
fun err msg src =
- let val (name, pos) = Args.name_of_src src
+ let val (name, pos) = Token.name_of_src src
in error (msg ^ " " ^ quote name ^ Position.here pos) end;
fun eval src ((th, dyn), (decls, context)) =
--- a/src/Pure/Isar/bundle.ML Tue Aug 19 18:21:29 2014 +0200
+++ b/src/Pure/Isar/bundle.ML Tue Aug 19 23:17:51 2014 +0200
@@ -6,13 +6,13 @@
signature BUNDLE =
sig
- type bundle = (thm list * Args.src list) list
+ type bundle = (thm list * Token.src list) list
val check: Proof.context -> xstring * Position.T -> string
val get_bundle: Proof.context -> string -> bundle
val get_bundle_cmd: Proof.context -> xstring * Position.T -> bundle
- val bundle: binding * (thm list * Args.src list) list ->
+ val bundle: binding * (thm list * Token.src list) list ->
(binding * typ option * mixfix) list -> local_theory -> local_theory
- val bundle_cmd: binding * (Facts.ref * Args.src list) list ->
+ val bundle_cmd: binding * (Facts.ref * Token.src list) list ->
(binding * string option * mixfix) list -> local_theory -> local_theory
val includes: string list -> Proof.context -> Proof.context
val includes_cmd: (xstring * Position.T) list -> Proof.context -> Proof.context
@@ -31,10 +31,10 @@
(* maintain bundles *)
-type bundle = (thm list * Args.src list) list;
+type bundle = (thm list * Token.src list) list;
fun transform_bundle phi : bundle -> bundle =
- map (fn (fact, atts) => (Morphism.fact phi fact, map (Args.transform_values phi) atts));
+ map (fn (fact, atts) => (Morphism.fact phi fact, map (Token.transform_src phi) atts));
structure Data = Generic_Data
(
--- a/src/Pure/Isar/calculation.ML Tue Aug 19 18:21:29 2014 +0200
+++ b/src/Pure/Isar/calculation.ML Tue Aug 19 23:17:51 2014 +0200
@@ -14,10 +14,10 @@
val sym_del: attribute
val symmetric: attribute
val also: thm list option -> bool -> Proof.state -> Proof.state Seq.result Seq.seq
- val also_cmd: (Facts.ref * Attrib.src list) list option ->
+ val also_cmd: (Facts.ref * Token.src list) list option ->
bool -> Proof.state -> Proof.state Seq.result Seq.seq
val finally: thm list option -> bool -> Proof.state -> Proof.state Seq.result Seq.seq
- val finally_cmd: (Facts.ref * Attrib.src list) list option -> bool ->
+ val finally_cmd: (Facts.ref * Token.src list) list option -> bool ->
Proof.state -> Proof.state Seq.result Seq.seq
val moreover: bool -> Proof.state -> Proof.state
val ultimately: bool -> Proof.state -> Proof.state
--- a/src/Pure/Isar/code.ML Tue Aug 19 18:21:29 2014 +0200
+++ b/src/Pure/Isar/code.ML Tue Aug 19 23:17:51 2014 +0200
@@ -49,13 +49,13 @@
val add_nbe_eqn: thm -> theory -> theory
val add_abs_eqn: thm -> theory -> theory
val add_abs_eqn_attribute: attribute
- val add_abs_eqn_attrib: Attrib.src
+ val add_abs_eqn_attrib: Token.src
val add_default_eqn: thm -> theory -> theory
val add_default_eqn_attribute: attribute
- val add_default_eqn_attrib: Attrib.src
+ val add_default_eqn_attrib: Token.src
val add_nbe_default_eqn: thm -> theory -> theory
val add_nbe_default_eqn_attribute: attribute
- val add_nbe_default_eqn_attrib: Attrib.src
+ val add_nbe_default_eqn_attrib: Token.src
val del_eqn: thm -> theory -> theory
val del_eqns: string -> theory -> theory
val del_exception: string -> theory -> theory
--- a/src/Pure/Isar/element.ML Tue Aug 19 18:21:29 2014 +0200
+++ b/src/Pure/Isar/element.ML Tue Aug 19 23:17:51 2014 +0200
@@ -17,18 +17,18 @@
Constrains of (string * 'typ) list |
Assumes of (Attrib.binding * ('term * 'term list) list) list |
Defines of (Attrib.binding * ('term * 'term list)) list |
- Notes of string * (Attrib.binding * ('fact * Attrib.src list) list) list
+ Notes of string * (Attrib.binding * ('fact * Token.src list) list) list
type context = (string, string, Facts.ref) ctxt
type context_i = (typ, term, thm list) ctxt
val map_ctxt: {binding: binding -> binding, typ: 'typ -> 'a, term: 'term -> 'b,
- pattern: 'term -> 'b, fact: 'fact -> 'c, attrib: Attrib.src -> Attrib.src} ->
+ pattern: 'term -> 'b, fact: 'fact -> 'c, attrib: Token.src -> Token.src} ->
('typ, 'term, 'fact) ctxt -> ('a, 'b, 'c) ctxt
- val map_ctxt_attrib: (Attrib.src -> Attrib.src) ->
+ val map_ctxt_attrib: (Token.src -> Token.src) ->
('typ, 'term, 'fact) ctxt -> ('typ, 'term, 'fact) ctxt
val transform_ctxt: morphism -> context_i -> context_i
val transform_facts: morphism ->
- (Attrib.binding * (thm list * Args.src list) list) list ->
- (Attrib.binding * (thm list * Args.src list) list) list
+ (Attrib.binding * (thm list * Token.src list) list) list ->
+ (Attrib.binding * (thm list * Token.src list) list) list
val pretty_stmt: Proof.context -> statement_i -> Pretty.T list
val pretty_ctxt: Proof.context -> context_i -> Pretty.T list
val pretty_statement: Proof.context -> string -> thm -> Pretty.T
@@ -78,7 +78,7 @@
Constrains of (string * 'typ) list |
Assumes of (Attrib.binding * ('term * 'term list) list) list |
Defines of (Attrib.binding * ('term * 'term list)) list |
- Notes of string * (Attrib.binding * ('fact * Attrib.src list) list) list;
+ Notes of string * (Attrib.binding * ('fact * Token.src list) list) list;
type context = (string, string, Facts.ref) ctxt;
type context_i = (typ, term, thm list) ctxt;
@@ -103,7 +103,7 @@
term = Morphism.term phi,
pattern = Morphism.term phi,
fact = Morphism.fact phi,
- attrib = Args.transform_values phi};
+ attrib = Token.transform_src phi};
fun transform_facts phi facts =
Notes ("", facts) |> transform_ctxt phi |> (fn Notes (_, facts') => facts');
@@ -509,14 +509,14 @@
fun activate_i elem ctxt =
let
val elem' =
- (case map_ctxt_attrib Args.init_assignable elem of
+ (case map_ctxt_attrib Token.init_assignable_src elem of
Defines defs =>
Defines (defs |> map (fn ((a, atts), (t, ps)) =>
((Thm.def_binding_optional (Binding.name (#1 (#1 (Local_Defs.cert_def ctxt t)))) a, atts),
(t, ps))))
| e => e);
val ctxt' = Context.proof_map (init elem') ctxt;
- in (map_ctxt_attrib Args.closure elem', ctxt') end;
+ in (map_ctxt_attrib Token.closure_src elem', ctxt') end;
fun activate raw_elem ctxt =
let val elem = raw_elem |> map_ctxt
--- a/src/Pure/Isar/generic_target.ML Tue Aug 19 18:21:29 2014 +0200
+++ b/src/Pure/Isar/generic_target.ML Tue Aug 19 23:17:51 2014 +0200
@@ -23,9 +23,9 @@
bool -> (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
(term * (string * thm)) * local_theory
val notes:
- (string -> (Attrib.binding * (thm list * Args.src list) list) list ->
- (Attrib.binding * (thm list * Args.src list) list) list -> local_theory -> local_theory) ->
- string -> (Attrib.binding * (thm list * Args.src list) list) list -> local_theory ->
+ (string -> (Attrib.binding * (thm list * Token.src list) list) list ->
+ (Attrib.binding * (thm list * Token.src list) list) list -> local_theory -> local_theory) ->
+ string -> (Attrib.binding * (thm list * Token.src list) list) list -> local_theory ->
(string * thm list) list * local_theory
val abbrev: (string * bool -> binding * mixfix -> term ->
term list * term list -> local_theory -> local_theory) ->
@@ -35,8 +35,8 @@
val theory_foundation: ((binding * typ) * mixfix) * (binding * term) ->
term list * term list -> local_theory -> (term * thm) * local_theory
val theory_notes: string ->
- (Attrib.binding * (thm list * Args.src list) list) list ->
- (Attrib.binding * (thm list * Args.src list) list) list ->
+ (Attrib.binding * (thm list * Token.src list) list) list ->
+ (Attrib.binding * (thm list * Token.src list) list) list ->
local_theory -> local_theory
val theory_declaration: declaration -> local_theory -> local_theory
val theory_abbrev: Syntax.mode -> (binding * mixfix) -> term -> term list * term list ->
@@ -46,8 +46,8 @@
(* locale operations *)
val locale_notes: string -> string ->
- (Attrib.binding * (thm list * Args.src list) list) list ->
- (Attrib.binding * (thm list * Args.src list) list) list ->
+ (Attrib.binding * (thm list * Token.src list) list) list ->
+ (Attrib.binding * (thm list * Token.src list) list) list ->
local_theory -> local_theory
val locale_target_declaration: string -> bool -> declaration -> local_theory -> local_theory
val locale_declaration: string -> {syntax: bool, pervasive: bool} -> declaration ->
--- a/src/Pure/Isar/isar_cmd.ML Tue Aug 19 18:21:29 2014 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Tue Aug 19 23:17:51 2014 +0200
@@ -16,7 +16,7 @@
val translations: (xstring * string) Syntax.trrule list -> theory -> theory
val no_translations: (xstring * string) Syntax.trrule list -> theory -> theory
val oracle: bstring * Position.T -> Symbol_Pos.source -> theory -> theory
- val add_defs: (bool * bool) * ((binding * string) * Attrib.src list) list -> theory -> theory
+ val add_defs: (bool * bool) * ((binding * string) * Token.src list) list -> theory -> theory
val declaration: {syntax: bool, pervasive: bool} ->
Symbol_Pos.source -> local_theory -> local_theory
val simproc_setup: string * Position.T -> string list -> Symbol_Pos.source ->
@@ -39,11 +39,11 @@
val thy_deps: Toplevel.transition -> Toplevel.transition
val locale_deps: Toplevel.transition -> Toplevel.transition
val class_deps: Toplevel.transition -> Toplevel.transition
- val print_stmts: string list * (Facts.ref * Attrib.src list) list
+ val print_stmts: string list * (Facts.ref * Token.src list) list
-> Toplevel.transition -> Toplevel.transition
- val print_thms: string list * (Facts.ref * Attrib.src list) list
+ val print_thms: string list * (Facts.ref * Token.src list) list
-> Toplevel.transition -> Toplevel.transition
- val print_prfs: bool -> string list * (Facts.ref * Attrib.src list) list option
+ val print_prfs: bool -> string list * (Facts.ref * Token.src list) list option
-> Toplevel.transition -> Toplevel.transition
val print_prop: (string list * string) -> Toplevel.transition -> Toplevel.transition
val print_term: (string list * string) -> Toplevel.transition -> Toplevel.transition
--- a/src/Pure/Isar/local_theory.ML Tue Aug 19 18:21:29 2014 +0200
+++ b/src/Pure/Isar/local_theory.ML Tue Aug 19 23:17:51 2014 +0200
@@ -9,8 +9,7 @@
structure Attrib =
struct
- type src = Args.src;
- type binding = binding * src list;
+ type binding = binding * Token.src list;
end;
signature LOCAL_THEORY =
@@ -49,9 +48,9 @@
val define_internal: (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
(term * (string * thm)) * local_theory
val note: Attrib.binding * thm list -> local_theory -> (string * thm list) * local_theory
- val notes: (Attrib.binding * (thm list * Attrib.src list) list) list ->
+ val notes: (Attrib.binding * (thm list * Token.src list) list) list ->
local_theory -> (string * thm list) list * local_theory
- val notes_kind: string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
+ val notes_kind: string -> (Attrib.binding * (thm list * Token.src list) list) list ->
local_theory -> (string * thm list) list * local_theory
val abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
(term * term) * local_theory
@@ -87,7 +86,7 @@
{define: bool -> (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
(term * (string * thm)) * local_theory,
notes: string ->
- (Attrib.binding * (thm list * Attrib.src list) list) list ->
+ (Attrib.binding * (thm list * Token.src list) list) list ->
local_theory -> (string * thm list) list * local_theory,
abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
(term * term) * local_theory,
--- a/src/Pure/Isar/locale.ML Tue Aug 19 18:21:29 2014 +0200
+++ b/src/Pure/Isar/locale.ML Tue Aug 19 23:17:51 2014 +0200
@@ -34,7 +34,7 @@
term option * term list ->
thm option * thm option -> thm list ->
declaration list ->
- (string * (Attrib.binding * (thm list * Attrib.src list) list) list) list ->
+ (string * (Attrib.binding * (thm list * Token.src list) list) list) list ->
(string * morphism) list -> theory -> theory
val intern: theory -> xstring -> string
val check: theory -> xstring * Position.T -> string
@@ -49,7 +49,7 @@
val specification_of: theory -> string -> term option * term list
(* Storing results *)
- val add_thmss: string -> string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
+ val add_thmss: string -> string -> (Attrib.binding * (thm list * Token.src list) list) list ->
Proof.context -> Proof.context
val add_declaration: string -> bool -> declaration -> Proof.context -> Proof.context
@@ -127,7 +127,7 @@
(** dynamic part **)
syntax_decls: (declaration * serial) list,
(* syntax declarations *)
- notes: ((string * (Attrib.binding * (thm list * Attrib.src list) list) list) * serial) list,
+ notes: ((string * (Attrib.binding * (thm list * Token.src list) list) list) * serial) list,
(* theorem declarations *)
dependencies: ((string * (morphism * morphism)) * serial) list
(* locale dependencies (sublocale relation) in reverse order *),
--- a/src/Pure/Isar/method.ML Tue Aug 19 18:21:29 2014 +0200
+++ b/src/Pure/Isar/method.ML Tue Aug 19 23:17:51 2014 +0200
@@ -41,15 +41,14 @@
val set_tactic: (thm list -> tactic) -> Proof.context -> Proof.context
val tactic: Symbol_Pos.source -> Proof.context -> method
val raw_tactic: Symbol_Pos.source -> Proof.context -> method
- type src = Args.src
type combinator_info
val no_combinator_info: combinator_info
datatype combinator = Then | Orelse | Try | Repeat1 | Select_Goals of int
datatype text =
- Source of src |
+ Source of Token.src |
Basic of Proof.context -> method |
Combinator of combinator_info * combinator * text list
- val map_source: (src -> src) -> text -> text
+ val map_source: (Token.src -> Token.src) -> text -> text
val primitive_text: (Proof.context -> thm -> thm) -> text
val succeed_text: text
val default_text: text
@@ -59,15 +58,16 @@
val finish_text: text option * bool -> text
val print_methods: Proof.context -> unit
val check_name: Proof.context -> xstring * Position.T -> string
- val method_syntax: (Proof.context -> method) context_parser -> Args.src -> Proof.context -> method
+ val method_syntax: (Proof.context -> method) context_parser ->
+ Token.src -> Proof.context -> method
val setup: binding -> (Proof.context -> method) context_parser -> string -> theory -> theory
val local_setup: binding -> (Proof.context -> method) context_parser -> string ->
local_theory -> local_theory
val method_setup: bstring * Position.T -> Symbol_Pos.source -> string ->
local_theory -> local_theory
- val method: Proof.context -> src -> Proof.context -> method
- val method_closure: Proof.context -> src -> src
- val method_cmd: Proof.context -> src -> Proof.context -> method
+ val method: Proof.context -> Token.src -> Proof.context -> method
+ val method_closure: Proof.context -> Token.src -> Token.src
+ val method_cmd: Proof.context -> Token.src -> Proof.context -> method
val evaluate: text -> Proof.context -> method
type modifier = (Proof.context -> Proof.context) * attribute
val section: modifier parser list -> thm list context_parser
@@ -274,8 +274,6 @@
(* method text *)
-type src = Args.src;
-
datatype combinator_info = Combinator_Info of {keywords: Position.T list};
fun combinator_info keywords = Combinator_Info {keywords = keywords};
val no_combinator_info = combinator_info [];
@@ -283,7 +281,7 @@
datatype combinator = Then | Orelse | Try | Repeat1 | Select_Goals of int;
datatype text =
- Source of src |
+ Source of Token.src |
Basic of Proof.context -> method |
Combinator of combinator_info * combinator * text list;
@@ -293,7 +291,7 @@
fun primitive_text r = Basic (SIMPLE_METHOD o PRIMITIVE o r);
val succeed_text = Basic (K succeed);
-val default_text = Source (Args.src ("default", Position.none) []);
+val default_text = Source (Token.src ("default", Position.none) []);
val this_text = Basic (K this);
val done_text = Basic (K (SIMPLE_METHOD all_tac));
fun sorry_text int = Basic (fn ctxt => cheating ctxt int);
@@ -307,7 +305,7 @@
structure Methods = Generic_Data
(
- type T = ((src -> Proof.context -> method) * string) Name_Space.table;
+ type T = ((Token.src -> Proof.context -> method) * string) Name_Space.table;
val empty : T = Name_Space.empty_table "method";
val extend = I;
fun merge data : T = Name_Space.merge_tables data;
@@ -354,13 +352,13 @@
(* check *)
fun check_name ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_methods ctxt);
-fun check_src ctxt src = Args.check_src ctxt (get_methods ctxt) src;
+fun check_src ctxt src = Token.check_src ctxt (get_methods ctxt) src;
(* method setup *)
fun method_syntax scan src ctxt : method =
- let val (m, ctxt') = Args.syntax scan src ctxt in m ctxt' end;
+ let val (m, ctxt') = Token.syntax scan src ctxt in m ctxt' end;
fun setup binding scan comment = define_global binding (method_syntax scan) comment #> snd;
fun local_setup binding scan comment = define binding (method_syntax scan) comment #> snd;
@@ -379,15 +377,15 @@
fun method ctxt =
let val table = get_methods ctxt
- in fn src => #1 (Name_Space.get table (#1 (Args.name_of_src src))) src end;
+ in fn src => #1 (Name_Space.get table (#1 (Token.name_of_src src))) src end;
fun method_closure ctxt0 src0 =
let
val (src1, meth) = check_src ctxt0 src0;
- val src2 = Args.init_assignable src1;
+ val src2 = Token.init_assignable_src src1;
val ctxt = Context_Position.not_really ctxt0;
val _ = Seq.pull (method ctxt src2 ctxt [] (Goal.protect 0 Drule.dummy_thm));
- in Args.closure src2 end;
+ in Token.closure_src src2 end;
fun method_cmd ctxt = method ctxt o method_closure ctxt;
@@ -505,9 +503,9 @@
local
fun meth4 x =
- (Parse.position Parse.xname >> (fn name => Source (Args.src name [])) ||
+ (Parse.position Parse.xname >> (fn name => Source (Token.src name [])) ||
Scan.ahead Parse.cartouche |-- Parse.not_eof >> (fn tok =>
- Source (Args.src ("cartouche", Token.pos_of tok) [tok])) ||
+ Source (Token.src ("cartouche", Token.pos_of tok) [tok])) ||
Parse.$$$ "(" |-- Parse.!!! (meth0 --| Parse.$$$ ")")) x
and meth3 x =
(meth4 -- Parse.position (Parse.$$$ "?")
@@ -520,7 +518,7 @@
Combinator (combinator_info [pos1, pos2], Select_Goals n, [m])) ||
meth4) x
and meth2 x =
- (Parse.position Parse.xname -- Parse.args1 is_symid_meth >> (Source o uncurry Args.src) ||
+ (Parse.position Parse.xname -- Parse.args1 is_symid_meth >> (Source o uncurry Token.src) ||
meth3) x
and meth1 x =
(Parse.enum1_positions "," meth2
--- a/src/Pure/Isar/parse.ML Tue Aug 19 18:21:29 2014 +0200
+++ b/src/Pure/Isar/parse.ML Tue Aug 19 23:17:51 2014 +0200
@@ -6,8 +6,6 @@
signature PARSE =
sig
- type 'a parser = Token.T list -> 'a * Token.T list
- type 'a context_parser = Context.generic * Token.T list -> 'a * (Context.generic * Token.T list)
val group: (unit -> string) -> (Token.T list -> 'a) -> Token.T list -> 'a
val !!! : (Token.T list -> 'a) -> Token.T list -> 'a
val !!!! : (Token.T list -> 'a) -> Token.T list -> 'a
@@ -114,10 +112,6 @@
structure Parse: PARSE =
struct
-type 'a parser = Token.T list -> 'a * Token.T list;
-type 'a context_parser = Context.generic * Token.T list -> 'a * (Context.generic * Token.T list);
-
-
(** error handling **)
(* group atomic parsers (no cuts!) *)
@@ -441,6 +435,3 @@
end;
-type 'a parser = 'a Parse.parser;
-type 'a context_parser = 'a Parse.context_parser;
-
--- a/src/Pure/Isar/parse_spec.ML Tue Aug 19 18:21:29 2014 +0200
+++ b/src/Pure/Isar/parse_spec.ML Tue Aug 19 23:17:51 2014 +0200
@@ -6,17 +6,17 @@
signature PARSE_SPEC =
sig
- val attribs: Attrib.src list parser
- val opt_attribs: Attrib.src list parser
+ val attribs: Token.src list parser
+ val opt_attribs: Token.src list parser
val thm_name: string -> Attrib.binding parser
val opt_thm_name: string -> Attrib.binding parser
val spec: (Attrib.binding * string) parser
val specs: (Attrib.binding * string list) parser
val alt_specs: (Attrib.binding * string) list parser
val where_alt_specs: (Attrib.binding * string) list parser
- val xthm: (Facts.ref * Attrib.src list) parser
- val xthms1: (Facts.ref * Attrib.src list) list parser
- val name_facts: (Attrib.binding * (Facts.ref * Attrib.src list) list) list parser
+ val xthm: (Facts.ref * Token.src list) parser
+ val xthms1: (Facts.ref * Token.src list) list parser
+ val name_facts: (Attrib.binding * (Facts.ref * Token.src list) list) list parser
val constdecl: (binding * string option * mixfix) parser
val constdef: ((binding * string option * mixfix) option * (Attrib.binding * string)) parser
val includes: (xstring * Position.T) list parser
@@ -37,7 +37,7 @@
(* theorem specifications *)
-val attrib = Parse.position Parse.liberal_name -- Parse.!!! Parse.args >> uncurry Args.src;
+val attrib = Parse.position Parse.liberal_name -- Parse.!!! Parse.args >> uncurry Token.src;
val attribs = Parse.$$$ "[" |-- Parse.list attrib --| Parse.$$$ "]";
val opt_attribs = Scan.optional attribs [];
--- a/src/Pure/Isar/proof.ML Tue Aug 19 18:21:29 2014 +0200
+++ b/src/Pure/Isar/proof.ML Tue Aug 19 23:17:51 2014 +0200
@@ -61,18 +61,18 @@
val chain: state -> state
val chain_facts: thm list -> state -> state
val note_thmss: (Thm.binding * (thm list * attribute list) list) list -> state -> state
- val note_thmss_cmd: (Attrib.binding * (Facts.ref * Attrib.src list) list) list -> state -> state
+ val note_thmss_cmd: (Attrib.binding * (Facts.ref * Token.src list) list) list -> state -> state
val from_thmss: ((thm list * attribute list) list) list -> state -> state
- val from_thmss_cmd: ((Facts.ref * Attrib.src list) list) list -> state -> state
+ val from_thmss_cmd: ((Facts.ref * Token.src list) list) list -> state -> state
val with_thmss: ((thm list * attribute list) list) list -> state -> state
- val with_thmss_cmd: ((Facts.ref * Attrib.src list) list) list -> state -> state
+ val with_thmss_cmd: ((Facts.ref * Token.src list) list) list -> state -> state
val using: ((thm list * attribute list) list) list -> state -> state
- val using_cmd: ((Facts.ref * Attrib.src list) list) list -> state -> state
+ val using_cmd: ((Facts.ref * Token.src list) list) list -> state -> state
val unfolding: ((thm list * attribute list) list) list -> state -> state
- val unfolding_cmd: ((Facts.ref * Attrib.src list) list) list -> state -> state
+ val unfolding_cmd: ((Facts.ref * Token.src list) list) list -> state -> state
val invoke_case: (string * Position.T) * binding option list * attribute list ->
state -> state
- val invoke_case_cmd: (string * Position.T) * binding option list * Attrib.src list ->
+ val invoke_case_cmd: (string * Position.T) * binding option list * Token.src list ->
state -> state
val begin_block: state -> state
val next_block: state -> state
--- a/src/Pure/Isar/specification.ML Tue Aug 19 18:21:29 2014 +0200
+++ b/src/Pure/Isar/specification.ML Tue Aug 19 23:17:51 2014 +0200
@@ -51,11 +51,11 @@
val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
val notation_cmd: bool -> Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
val theorems: string ->
- (Attrib.binding * (thm list * Attrib.src list) list) list ->
+ (Attrib.binding * (thm list * Token.src list) list) list ->
(binding * typ option * mixfix) list ->
bool -> local_theory -> (string * thm list) list * local_theory
val theorems_cmd: string ->
- (Attrib.binding * (Facts.ref * Attrib.src list) list) list ->
+ (Attrib.binding * (Facts.ref * Token.src list) list) list ->
(binding * string option * mixfix) list ->
bool -> local_theory -> (string * thm list) list * local_theory
val theorem: string -> Method.text option ->
--- a/src/Pure/Isar/token.ML Tue Aug 19 18:21:29 2014 +0200
+++ b/src/Pure/Isar/token.ML Tue Aug 19 23:17:51 2014 +0200
@@ -66,10 +66,22 @@
val mk_term: term -> T
val mk_fact: string option * thm list -> T
val mk_attribute: (morphism -> attribute) -> T
- val transform_value: morphism -> T -> T
+ val transform: morphism -> T -> T
val init_assignable: T -> T
val assign: value option -> T -> unit
val closure: T -> T
+
+ type src
+ val src: xstring * Position.T -> T list -> src
+ val name_of_src: src -> string * Position.T
+ val range_of_src: src -> Position.T
+ val unparse_src: src -> string list
+ val pretty_src: Proof.context -> src -> Pretty.T
+ val check_src: Proof.context -> 'a Name_Space.table -> src -> src * 'a
+ val transform_src: morphism -> src -> src
+ val init_assignable_src: src -> src
+ val closure_src: src -> src
+
val ident_or_symbolic: string -> bool
val source_proper: (T, 'a) Source.source -> (T, (T, 'a) Source.source) Source.source
val source': {do_recover: bool option} -> (unit -> Scan.lexicon * Scan.lexicon) ->
@@ -78,6 +90,11 @@
Position.T -> (Symbol.symbol, 'a) Source.source -> (T,
(Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source) Source.source
val read_antiq: Scan.lexicon -> (T list -> 'a * T list) -> Symbol_Pos.T list * Position.T -> 'a
+
+ type 'a parser = T list -> 'a * T list
+ type 'a context_parser = Context.generic * T list -> 'a * (Context.generic * T list)
+ val syntax_generic: 'a context_parser -> src -> Context.generic -> 'a * Context.generic
+ val syntax: 'a context_parser -> src -> Proof.context -> 'a * Proof.context
end;
structure Token: TOKEN =
@@ -378,7 +395,7 @@
(* transform value *)
-fun transform_value phi =
+fun transform phi =
map_value (fn v =>
(case v of
Literal _ => v
@@ -407,6 +424,58 @@
+(** src **)
+
+datatype src =
+ Src of
+ {name: string * Position.T,
+ args: T list,
+ output_info: (string * Markup.T) option};
+
+fun src name args = Src {name = name, args = args, output_info = NONE};
+
+fun name_of_src (Src {name, ...}) = name;
+
+fun range_of_src (Src {name = (_, pos), args, ...}) =
+ if null args then pos
+ else Position.set_range (pos, #2 (range_of args));
+
+fun unparse_src (Src {args, ...}) = map unparse args;
+
+fun pretty_src ctxt src =
+ let
+ val Src {name = (name, _), args, output_info} = src;
+ val prt_name =
+ (case output_info of
+ NONE => Pretty.str name
+ | SOME (_, markup) => Pretty.mark_str (markup, name));
+ val prt_arg = pretty_value ctxt;
+ in Pretty.block (Pretty.breaks (prt_name :: map prt_arg args)) end;
+
+
+(* check *)
+
+fun check_src ctxt table (Src {name = (xname, pos), args, output_info = _}) =
+ let
+ val (name, x) = Name_Space.check (Context.Proof ctxt) table (xname, pos);
+ val space = Name_Space.space_of_table table;
+ val kind = Name_Space.kind_of space;
+ val markup = Name_Space.markup space name;
+ in (Src {name = (name, pos), args = args, output_info = SOME (kind, markup)}, x) end;
+
+
+(* values *)
+
+fun map_args f (Src {name, args, output_info}) =
+ Src {name = name, args = map f args, output_info = output_info};
+
+val transform_src = map_args o transform;
+
+val init_assignable_src = map_args init_assignable;
+val closure_src = map_args closure;
+
+
+
(** scanners **)
open Basic_Symbol_Pos;
@@ -546,4 +615,44 @@
|> Source.exhaust;
in (case res of [x] => x | _ => err "") handle ERROR msg => err msg end;
+
+
+(** parsers **)
+
+type 'a parser = T list -> 'a * T list;
+type 'a context_parser = Context.generic * T list -> 'a * (Context.generic * T list);
+
+fun syntax_generic scan (Src {name = (name, pos), args = args0, output_info}) context =
+ let
+ val args1 = map init_assignable args0;
+ fun reported_text () =
+ if Context_Position.is_visible_generic context then
+ ((pos, Markup.operator) :: maps (reports_of_value o closure) args1)
+ |> map (fn (p, m) => Position.reported_text p m "")
+ else [];
+ in
+ (case Scan.error (Scan.finite' stopper (Scan.option scan)) (context, args1) of
+ (SOME x, (context', [])) =>
+ let val _ = Output.report (reported_text ())
+ in (x, context') end
+ | (_, (_, args2)) =>
+ let
+ val print_name =
+ (case output_info of
+ NONE => quote name
+ | SOME (kind, markup) => plain_words kind ^ " " ^ quote (Markup.markup markup name));
+ val print_args =
+ if null args2 then "" else ":\n " ^ space_implode " " (map print args2);
+ in
+ error ("Bad arguments for " ^ print_name ^ Position.here pos ^ print_args ^
+ Markup.markup_report (implode (reported_text ())))
+ end)
+ end;
+
+fun syntax scan src = apsnd Context.the_proof o syntax_generic scan src o Context.Proof;
+
end;
+
+type 'a parser = 'a Token.parser;
+type 'a context_parser = 'a Token.context_parser;
+
--- a/src/Pure/ML/ml_antiquotation.ML Tue Aug 19 18:21:29 2014 +0200
+++ b/src/Pure/ML/ml_antiquotation.ML Tue Aug 19 23:17:51 2014 +0200
@@ -8,7 +8,7 @@
sig
val variant: string -> Proof.context -> string * Proof.context
val declaration: binding -> 'a context_parser ->
- (Args.src -> 'a -> Proof.context -> ML_Context.decl * Proof.context) ->
+ (Token.src -> 'a -> Proof.context -> ML_Context.decl * Proof.context) ->
theory -> theory
val inline: binding -> string context_parser -> theory -> theory
val value: binding -> string context_parser -> theory -> theory
@@ -40,7 +40,7 @@
fun declaration name scan body =
ML_Context.add_antiquotation name
(fn src => fn orig_ctxt =>
- let val (x, _) = Args.syntax scan src orig_ctxt
+ let val (x, _) = Token.syntax scan src orig_ctxt
in body src x orig_ctxt end);
fun inline name scan =
@@ -62,7 +62,7 @@
(fn src => fn () => fn ctxt =>
let
val (a, ctxt') = variant "position" ctxt;
- val (_, pos) = Args.name_of_src src;
+ val (_, pos) = Token.name_of_src src;
val env = "val " ^ a ^ " = " ^ ML_Syntax.print_position pos ^ ";\n";
val body = "Isabelle." ^ a;
in (K (env, body), ctxt') end) #>
--- a/src/Pure/ML/ml_antiquotations.ML Tue Aug 19 18:21:29 2014 +0200
+++ b/src/Pure/ML/ml_antiquotations.ML Tue Aug 19 23:17:51 2014 +0200
@@ -64,7 +64,7 @@
(Scan.lift (Scan.optional Args.name "Output.writeln"))
(fn src => fn output => fn ctxt =>
let
- val (_, pos) = Args.name_of_src src;
+ val (_, pos) = Token.name_of_src src;
val (a, ctxt') = ML_Antiquotation.variant "output" ctxt;
val env =
"val " ^ a ^ ": string -> unit =\n\
--- a/src/Pure/ML/ml_context.ML Tue Aug 19 18:21:29 2014 +0200
+++ b/src/Pure/ML/ml_context.ML Tue Aug 19 23:17:51 2014 +0200
@@ -14,7 +14,7 @@
val exec: (unit -> unit) -> Context.generic -> Context.generic
val check_antiquotation: Proof.context -> xstring * Position.T -> string
type decl = Proof.context -> string * string
- val add_antiquotation: binding -> (Args.src -> Proof.context -> decl * Proof.context) ->
+ val add_antiquotation: binding -> (Token.src -> Proof.context -> decl * Proof.context) ->
theory -> theory
val print_antiquotations: Proof.context -> unit
val eval_antiquotes: ML_Lex.token Antiquote.antiquote list * Position.T ->
@@ -55,7 +55,7 @@
type decl = Proof.context -> string * string; (*final context -> ML env, ML body*)
structure Antiquotations = Theory_Data
(
- type T = (Args.src -> Proof.context -> decl * Proof.context) Name_Space.table;
+ type T = (Token.src -> Proof.context -> decl * Proof.context) Name_Space.table;
val empty : T = Name_Space.empty_table Markup.ML_antiquotationN;
val extend = I;
fun merge data : T = Name_Space.merge_tables data;
@@ -75,7 +75,7 @@
|> Pretty.writeln;
fun apply_antiquotation src ctxt =
- let val (src', f) = Args.check_src ctxt (get_antiquotations ctxt) src
+ let val (src', f) = Token.check_src ctxt (get_antiquotations ctxt) src
in f src' ctxt end;
@@ -85,7 +85,7 @@
val antiq =
Parse.!!! (Parse.position Parse.xname -- Parse.args --| Scan.ahead Parse.eof)
- >> uncurry Args.src;
+ >> uncurry Token.src;
val begin_env0 = ML_Lex.tokenize "structure Isabelle =\nstruct\n";
--- a/src/Pure/ML/ml_thms.ML Tue Aug 19 18:21:29 2014 +0200
+++ b/src/Pure/ML/ml_thms.ML Tue Aug 19 23:17:51 2014 +0200
@@ -6,7 +6,7 @@
signature ML_THMS =
sig
- val the_attributes: Proof.context -> int -> Args.src list
+ val the_attributes: Proof.context -> int -> Token.src list
val the_thmss: Proof.context -> thm list list
val get_stored_thms: unit -> thm list
val get_stored_thm: unit -> thm
@@ -25,7 +25,7 @@
structure Data = Proof_Data
(
- type T = Args.src list Inttab.table * thms list;
+ type T = Token.src list Inttab.table * thms list;
fun init _ = (Inttab.empty, []);
);
--- a/src/Pure/Thy/term_style.ML Tue Aug 19 18:21:29 2014 +0200
+++ b/src/Pure/Thy/term_style.ML Tue Aug 19 23:17:51 2014 +0200
@@ -35,8 +35,8 @@
fun parse_single ctxt =
Parse.position Parse.xname -- Parse.args >> (fn (name, args) =>
let
- val (src, parse) = Args.check_src ctxt (get_data ctxt) (Args.src name args);
- val (f, _) = Args.syntax (Scan.lift parse) src ctxt;
+ val (src, parse) = Token.check_src ctxt (get_data ctxt) (Token.src name args);
+ val (f, _) = Token.syntax (Scan.lift parse) src ctxt;
in f ctxt end);
val parse = Args.context :|-- (fn ctxt => Scan.lift
--- a/src/Pure/Thy/thy_output.ML Tue Aug 19 18:21:29 2014 +0200
+++ b/src/Pure/Thy/thy_output.ML Tue Aug 19 23:17:51 2014 +0200
@@ -18,7 +18,7 @@
val check_option: Proof.context -> xstring * Position.T -> string
val print_antiquotations: Proof.context -> unit
val antiquotation: binding -> 'a context_parser ->
- ({source: Args.src, state: Toplevel.state, context: Proof.context} -> 'a -> string) ->
+ ({source: Token.src, state: Toplevel.state, context: Proof.context} -> 'a -> string) ->
theory -> theory
val boolean: string -> bool
val integer: string -> int
@@ -30,9 +30,9 @@
val pretty_text: Proof.context -> string -> Pretty.T
val pretty_term: Proof.context -> term -> Pretty.T
val pretty_thm: Proof.context -> thm -> Pretty.T
- val str_of_source: Args.src -> string
+ val str_of_source: Token.src -> string
val maybe_pretty_source: (Proof.context -> 'a -> Pretty.T) -> Proof.context ->
- Args.src -> 'a list -> Pretty.T list
+ Token.src -> 'a list -> Pretty.T list
val output: Proof.context -> Pretty.T list -> string
val verb_text: string -> string
end;
@@ -67,7 +67,7 @@
structure Antiquotations = Theory_Data
(
type T =
- (Args.src -> Toplevel.state -> Proof.context -> string) Name_Space.table *
+ (Token.src -> Toplevel.state -> Proof.context -> string) Name_Space.table *
(string -> Proof.context -> Proof.context) Name_Space.table;
val empty : T =
(Name_Space.empty_table Markup.document_antiquotationN,
@@ -91,7 +91,7 @@
fun check_option ctxt = #1 o Name_Space.check (Context.Proof ctxt) (#2 (get_antiquotations ctxt));
fun command src state ctxt =
- let val (src', f) = Args.check_src ctxt (#1 (get_antiquotations ctxt)) src
+ let val (src', f) = Token.check_src ctxt (#1 (get_antiquotations ctxt)) src
in f src' state ctxt end;
fun option ((xname, pos), s) ctxt =
@@ -114,7 +114,7 @@
fun antiquotation name scan body =
add_command name
(fn src => fn state => fn ctxt =>
- let val (x, ctxt') = Args.syntax scan src ctxt
+ let val (x, ctxt') = Token.syntax scan src ctxt
in body {source = src, state = state, context = ctxt'} x end);
@@ -151,7 +151,7 @@
val antiq =
Parse.!!!
(Parse.position Parse.liberal_name -- properties -- Parse.args --| Scan.ahead Parse.eof)
- >> (fn ((name, props), args) => (props, Args.src name args));
+ >> (fn ((name, props), args) => (props, Token.src name args));
end;
@@ -534,7 +534,7 @@
(* default output *)
-val str_of_source = space_implode " " o Args.unparse_src;
+val str_of_source = space_implode " " o Token.unparse_src;
fun maybe_pretty_source pretty ctxt src xs =
map (pretty ctxt) xs (*always pretty in order to exhibit errors!*)
@@ -624,7 +624,7 @@
Scan.lift (Parse.position (Args.$$$ "by") -- Method.parse -- Scan.option Method.parse))
(fn {source, context = ctxt, ...} => fn ((prop_token, prop), (((_, by_pos), m1), m2)) =>
let
- val prop_src = Args.src (Args.name_of_src source) [prop_token];
+ val prop_src = Token.src (Token.name_of_src source) [prop_token];
val reports = (by_pos, Markup.keyword1) :: maps Method.reports_of (m1 :: the_list m2);
val _ = Context_Position.reports ctxt reports;
--- a/src/ZF/Tools/datatype_package.ML Tue Aug 19 18:21:29 2014 +0200
+++ b/src/ZF/Tools/datatype_package.ML Tue Aug 19 23:17:51 2014 +0200
@@ -32,8 +32,8 @@
val add_datatype_i: term * term list -> Ind_Syntax.constructor_spec list list ->
thm list * thm list * thm list -> theory -> theory * inductive_result * datatype_result
val add_datatype: string * string list -> (string * string list * mixfix) list list ->
- (Facts.ref * Attrib.src list) list * (Facts.ref * Attrib.src list) list *
- (Facts.ref * Attrib.src list) list -> theory -> theory * inductive_result * datatype_result
+ (Facts.ref * Token.src list) list * (Facts.ref * Token.src list) list *
+ (Facts.ref * Token.src list) list -> theory -> theory * inductive_result * datatype_result
end;
functor Add_datatype_def_Fun
--- a/src/ZF/Tools/induct_tacs.ML Tue Aug 19 18:21:29 2014 +0200
+++ b/src/ZF/Tools/induct_tacs.ML Tue Aug 19 23:17:51 2014 +0200
@@ -12,8 +12,8 @@
val induct_tac: Proof.context -> string -> int -> tactic
val exhaust_tac: Proof.context -> string -> int -> tactic
val rep_datatype_i: thm -> thm -> thm list -> thm list -> theory -> theory
- val rep_datatype: Facts.ref * Attrib.src list -> Facts.ref * Attrib.src list ->
- (Facts.ref * Attrib.src list) list -> (Facts.ref * Attrib.src list) list -> theory -> theory
+ val rep_datatype: Facts.ref * Token.src list -> Facts.ref * Token.src list ->
+ (Facts.ref * Token.src list) list -> (Facts.ref * Token.src list) list -> theory -> theory
val setup: theory -> theory
end;
--- a/src/ZF/Tools/inductive_package.ML Tue Aug 19 18:21:29 2014 +0200
+++ b/src/ZF/Tools/inductive_package.ML Tue Aug 19 23:17:51 2014 +0200
@@ -29,9 +29,9 @@
((binding * term) * attribute list) list ->
thm list * thm list * thm list * thm list -> theory -> theory * inductive_result
val add_inductive: string list * string ->
- ((binding * string) * Attrib.src list) list ->
- (Facts.ref * Attrib.src list) list * (Facts.ref * Attrib.src list) list *
- (Facts.ref * Attrib.src list) list * (Facts.ref * Attrib.src list) list ->
+ ((binding * string) * Token.src list) list ->
+ (Facts.ref * Token.src list) list * (Facts.ref * Token.src list) list *
+ (Facts.ref * Token.src list) list * (Facts.ref * Token.src list) list ->
theory -> theory * inductive_result
end;
--- a/src/ZF/Tools/primrec_package.ML Tue Aug 19 18:21:29 2014 +0200
+++ b/src/ZF/Tools/primrec_package.ML Tue Aug 19 23:17:51 2014 +0200
@@ -8,7 +8,7 @@
signature PRIMREC_PACKAGE =
sig
- val add_primrec: ((binding * string) * Attrib.src list) list -> theory -> theory * thm list
+ val add_primrec: ((binding * string) * Token.src list) list -> theory -> theory * thm list
val add_primrec_i: ((binding * term) * attribute list) list -> theory -> theory * thm list
end;