# HG changeset patch # User wenzelm # Date 1408483071 -7200 # Node ID bc6bced136e5dd0c29e4e2132996214af7b96ae1 # Parent 568840962230b1a3a5de7b1c2dcab9f26653317e tuned signature -- moved type src to Token, without aliases; diff -r 568840962230 -r bc6bced136e5 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- 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), diff -r 568840962230 -r bc6bced136e5 src/HOL/Tools/Function/function_common.ML --- 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, diff -r 568840962230 -r bc6bced136e5 src/HOL/Tools/Lifting/lifting_def.ML --- 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 diff -r 568840962230 -r bc6bced136e5 src/HOL/Tools/Lifting/lifting_setup.ML --- 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." diff -r 568840962230 -r bc6bced136e5 src/HOL/Tools/Quotient/quotient_type.ML --- 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 = diff -r 568840962230 -r bc6bced136e5 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML --- 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 diff -r 568840962230 -r bc6bced136e5 src/HOL/Tools/inductive.ML --- 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; diff -r 568840962230 -r bc6bced136e5 src/HOL/Tools/inductive_set.ML --- 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 diff -r 568840962230 -r bc6bced136e5 src/HOL/Tools/recdef.ML --- 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 diff -r 568840962230 -r bc6bced136e5 src/HOL/Tools/try0.ML --- 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)); diff -r 568840962230 -r bc6bced136e5 src/Pure/Isar/args.ML --- 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; diff -r 568840962230 -r bc6bced136e5 src/Pure/Isar/attrib.ML --- 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)) = diff -r 568840962230 -r bc6bced136e5 src/Pure/Isar/bundle.ML --- 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 ( diff -r 568840962230 -r bc6bced136e5 src/Pure/Isar/calculation.ML --- 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 diff -r 568840962230 -r bc6bced136e5 src/Pure/Isar/code.ML --- 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 diff -r 568840962230 -r bc6bced136e5 src/Pure/Isar/element.ML --- 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 diff -r 568840962230 -r bc6bced136e5 src/Pure/Isar/generic_target.ML --- 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 -> diff -r 568840962230 -r bc6bced136e5 src/Pure/Isar/isar_cmd.ML --- 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 diff -r 568840962230 -r bc6bced136e5 src/Pure/Isar/local_theory.ML --- 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, diff -r 568840962230 -r bc6bced136e5 src/Pure/Isar/locale.ML --- 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 *), diff -r 568840962230 -r bc6bced136e5 src/Pure/Isar/method.ML --- 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 diff -r 568840962230 -r bc6bced136e5 src/Pure/Isar/parse.ML --- 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; - diff -r 568840962230 -r bc6bced136e5 src/Pure/Isar/parse_spec.ML --- 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 []; diff -r 568840962230 -r bc6bced136e5 src/Pure/Isar/proof.ML --- 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 diff -r 568840962230 -r bc6bced136e5 src/Pure/Isar/specification.ML --- 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 -> diff -r 568840962230 -r bc6bced136e5 src/Pure/Isar/token.ML --- 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; + diff -r 568840962230 -r bc6bced136e5 src/Pure/ML/ml_antiquotation.ML --- 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) #> diff -r 568840962230 -r bc6bced136e5 src/Pure/ML/ml_antiquotations.ML --- 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\ diff -r 568840962230 -r bc6bced136e5 src/Pure/ML/ml_context.ML --- 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"; diff -r 568840962230 -r bc6bced136e5 src/Pure/ML/ml_thms.ML --- 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, []); ); diff -r 568840962230 -r bc6bced136e5 src/Pure/Thy/term_style.ML --- 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 diff -r 568840962230 -r bc6bced136e5 src/Pure/Thy/thy_output.ML --- 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; diff -r 568840962230 -r bc6bced136e5 src/ZF/Tools/datatype_package.ML --- 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 diff -r 568840962230 -r bc6bced136e5 src/ZF/Tools/induct_tacs.ML --- 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; diff -r 568840962230 -r bc6bced136e5 src/ZF/Tools/inductive_package.ML --- 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; diff -r 568840962230 -r bc6bced136e5 src/ZF/Tools/primrec_package.ML --- 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;