# HG changeset patch # User wenzelm # Date 1430671886 -7200 # Node ID f7e4294216d2fe33fd0cff3723767b32857ae7f2 # Parent 6a5015b096a2c45fd3ebae3fc994427618758bf6 updated Eisbach, using version fb741500f533 of its Bitbucket repository; diff -r 6a5015b096a2 -r f7e4294216d2 src/HOL/Eisbach/Eisbach.thy --- a/src/HOL/Eisbach/Eisbach.thy Sun May 03 18:45:58 2015 +0200 +++ b/src/HOL/Eisbach/Eisbach.thy Sun May 03 18:51:26 2015 +0200 @@ -1,11 +1,11 @@ -(* Title: Eisbach.thy +(* Title: HOL/Eisbach/Eisbach.thy Author: Daniel Matichuk, NICTA/UNSW Main entry point for Eisbach proof method language. *) theory Eisbach -imports Pure +imports Main keywords "method" :: thy_decl and "conclusion" @@ -16,7 +16,6 @@ "uses" begin - ML_file "parse_tools.ML" ML_file "eisbach_rule_insts.ML" ML_file "method_closure.ML" @@ -24,20 +23,12 @@ ML_file "eisbach_antiquotations.ML" (* FIXME reform Isabelle/Pure attributes to make this work by default *) -attribute_setup THEN = - \Scan.lift (Scan.optional (Args.bracks Parse.nat) 1) -- Attrib.thm >> (fn (i, B) => - Method_Closure.free_aware_rule_attribute [B] (fn _ => fn A => A RSN (i, B)))\ - "resolution with rule" - -attribute_setup OF = - \Attrib.thms >> (fn Bs => - Method_Closure.free_aware_rule_attribute Bs (fn _ => fn A => A OF Bs))\ - "rule resolved with facts" - -attribute_setup rotated = - \Scan.lift (Scan.optional Parse.int 1 >> (fn n => - Method_Closure.free_aware_rule_attribute [] (fn _ => rotate_prems n)))\ - "rotated theorem premises" +setup \ + fold (Method_Closure.wrap_attribute true) + [@{binding intro}, @{binding elim}, @{binding dest}, @{binding simp}] #> + fold (Method_Closure.wrap_attribute false) + [@{binding THEN}, @{binding OF}, @{binding rotated}, @{binding simplified}] +\ method solves methods m = (m; fail) diff -r 6a5015b096a2 -r f7e4294216d2 src/HOL/Eisbach/Eisbach_Tools.thy --- a/src/HOL/Eisbach/Eisbach_Tools.thy Sun May 03 18:45:58 2015 +0200 +++ b/src/HOL/Eisbach/Eisbach_Tools.thy Sun May 03 18:51:26 2015 +0200 @@ -1,4 +1,4 @@ -(* Title: Eisbach_Tools.thy +(* Title: HOL/Eisbach/Eisbach_Tools.thy Author: Daniel Matichuk, NICTA/UNSW Usability tools for Eisbach. diff -r 6a5015b096a2 -r f7e4294216d2 src/HOL/Eisbach/Examples.thy --- a/src/HOL/Eisbach/Examples.thy Sun May 03 18:45:58 2015 +0200 +++ b/src/HOL/Eisbach/Examples.thy Sun May 03 18:51:26 2015 +0200 @@ -1,4 +1,4 @@ -(* Title: Examples.thy +(* Title: HOL/Eisbach/Examples.thy Author: Daniel Matichuk, NICTA/UNSW *) diff -r 6a5015b096a2 -r f7e4294216d2 src/HOL/Eisbach/Tests.thy --- a/src/HOL/Eisbach/Tests.thy Sun May 03 18:45:58 2015 +0200 +++ b/src/HOL/Eisbach/Tests.thy Sun May 03 18:51:26 2015 +0200 @@ -1,4 +1,4 @@ -(* Title: Tests.thy +(* Title: HOL/Eisbach/Tests.thy Author: Daniel Matichuk, NICTA/UNSW *) @@ -9,6 +9,7 @@ begin + section \Named Theorems Tests\ named_theorems foo @@ -161,6 +162,7 @@ end + (* Testing inner focusing. This fails if we don't smash flex-flex pairs produced by retrofitting. This needs to be done more carefully to avoid smashing legitimate pairs.*) @@ -292,7 +294,7 @@ done -ML {* +ML \ structure Data = Generic_Data ( type T = thm list; @@ -300,7 +302,7 @@ val extend = I; fun merge data : T = Thm.merge_thms data; ); -*} +\ local_setup \Local_Theory.add_thms_dynamic (@{binding test_dyn}, Data.get)\ @@ -321,6 +323,34 @@ end + +notepad begin + fix A x + assume X: "\x. A x" + have "A x" + by (match X in H[of x]:"\x. A x" \ \print_fact H,match H in "A x" \ \rule H\\) + + fix A x B + assume X: "\x :: bool. A x \ B" "\x. A x" + assume Y: "A B" + have "B \ B \ B \ B \ B \ B" + apply (intro conjI) + apply (match X in H[OF X(2)]:"\x. A x \ B" \ \print_fact H,rule H\) + apply (match X in H':"\x. A x" and H[OF H']:"\x. A x \ B" \ \print_fact H',print_fact H,rule H\) + apply (match X in H[of Q]:"\x. A x \ ?R" and "?P \ Q" for Q \ \print_fact H,rule H, rule Y\) + apply (match X in H[of Q,OF Y]:"\x. A x \ ?R" and "?P \ Q" for Q \ \print_fact H,rule H\) + apply (match X in H[OF Y,intro]:"\x. A x \ ?R" \ \print_fact H,fastforce\) + apply (match X in H[intro]:"\x. A x \ ?R" \ \rule H[where x=B], rule Y\) + done + + fix x :: "prop" and A + assume X: "TERM x" + assume Y: "\x :: prop. A x" + have "A TERM x" + apply (match X in "PROP y" for y \ \rule Y[where x="PROP y"]\) + done +end + (* Method name internalization test *) method test2 = (simp) diff -r 6a5015b096a2 -r f7e4294216d2 src/HOL/Eisbach/eisbach_antiquotations.ML --- a/src/HOL/Eisbach/eisbach_antiquotations.ML Sun May 03 18:45:58 2015 +0200 +++ b/src/HOL/Eisbach/eisbach_antiquotations.ML Sun May 03 18:51:26 2015 +0200 @@ -1,4 +1,4 @@ -(* Title: eisbach_antiquotations.ML +(* Title: HOL/Eisbach/eisbach_antiquotations.ML Author: Daniel Matichuk, NICTA/UNSW ML antiquotations for Eisbach. diff -r 6a5015b096a2 -r f7e4294216d2 src/HOL/Eisbach/eisbach_rule_insts.ML --- a/src/HOL/Eisbach/eisbach_rule_insts.ML Sun May 03 18:45:58 2015 +0200 +++ b/src/HOL/Eisbach/eisbach_rule_insts.ML Sun May 03 18:51:26 2015 +0200 @@ -1,4 +1,4 @@ -(* Title: eisbach_rule_insts.ML +(* Title: HOL/Eisbach/eisbach_rule_insts.ML Author: Daniel Matichuk, NICTA/UNSW Eisbach-aware variants of the "where" and "of" attributes. @@ -77,10 +77,11 @@ Named_Insts of ((indexname * string) * (term -> unit)) list | Term_Insts of (indexname * term) list; -fun embed_indexname ((xi,s),f) = +fun embed_indexname ((xi, s), f) = let - fun wrap_xi xi t = Logic.mk_conjunction (Logic.mk_term (Var (xi,fastype_of t)),Logic.mk_term t); - in ((xi,s),f o wrap_xi xi) end; + fun wrap_xi xi t = + Logic.mk_conjunction (Logic.mk_term (Var (xi, fastype_of t)), Logic.mk_term t); + in ((xi, s), f o wrap_xi xi) end; fun unembed_indexname t = let @@ -98,9 +99,9 @@ val insts' = if forall (fn (_, v) => Parse_Tools.is_real_val v) insts - then Term_Insts (map (fn (_,t) => unembed_indexname (Parse_Tools.the_real_val t)) insts) + then Term_Insts (map (fn (_, t) => unembed_indexname (Parse_Tools.the_real_val t)) insts) else Named_Insts (map (fn (xi, p) => embed_indexname - ((xi,Parse_Tools.the_parse_val p),Parse_Tools.the_parse_fun p)) insts); + ((xi, Parse_Tools.the_parse_val p), Parse_Tools.the_parse_fun p)) insts); in (insts', fixes) end; @@ -132,13 +133,14 @@ if forall (fn SOME t => Parse_Tools.is_real_val t | NONE => true) (insts @ concl_insts) then Term_Insts - (map_filter (Option.map (Parse_Tools.the_real_val #> unembed_indexname)) (insts @ concl_insts)) - + (map_filter + (Option.map (Parse_Tools.the_real_val #> unembed_indexname)) (insts @ concl_insts)) else Named_Insts - (apply2 (map (Option.map (fn p => (Parse_Tools.the_parse_val p,Parse_Tools.the_parse_fun p)))) + (apply2 + (map (Option.map (fn p => (Parse_Tools.the_parse_val p, Parse_Tools.the_parse_fun p)))) (insts, concl_insts) - |> of_rule thm |> map ((fn (xi, (nm, tok)) => embed_indexname ((xi, nm), tok)))); + |> of_rule thm |> map ((fn (xi, (nm, tok)) => embed_indexname ((xi, nm), tok)))); in (insts', fixes) end; diff -r 6a5015b096a2 -r f7e4294216d2 src/HOL/Eisbach/match_method.ML --- a/src/HOL/Eisbach/match_method.ML Sun May 03 18:45:58 2015 +0200 +++ b/src/HOL/Eisbach/match_method.ML Sun May 03 18:51:26 2015 +0200 @@ -1,4 +1,4 @@ -(* Title: match_method.ML +(* Title: HOL/Eisbach/match_method.ML Author: Daniel Matichuk, NICTA/UNSW Setup for "match" proof method. It provides basic fact/term matching in @@ -61,8 +61,8 @@ val fixes = Parse.and_list1 (Scan.repeat1 (Parse.position bound_term) -- - Scan.option (@{keyword "::"} |-- Parse.!!! Parse.typ) >> (fn (xs, T) => map (fn (nm,pos) => ((nm,T),pos)) xs)) - >> flat; + Scan.option (@{keyword "::"} |-- Parse.!!! Parse.typ) + >> (fn (xs, T) => map (fn (nm, pos) => ((nm, T), pos)) xs)) >> flat; val for_fixes = Scan.optional (@{keyword "for"} |-- fixes) []; @@ -89,7 +89,6 @@ | "cut" => {multi = multi, cut = true})) ss {multi = false, cut = false}); -(*TODO: Shape holes in thms *) fun parse_named_pats match_kind = Args.context :|-- (fn ctxt => Scan.lift (Parse.and_list1 (Scan.option (dynamic_fact ctxt --| Args.colon) :-- @@ -105,20 +104,18 @@ SOME (Token.Source src) => let val text = Method_Closure.read_inner_method ctxt src - (*TODO: Correct parse context for attributes?*) val ts' = map (fn (b, (Parse_Tools.Real_Val v, match_args)) => ((Option.map (fn (b, att) => - (Parse_Tools.the_real_val b, - map (Attrib.attribute ctxt) att)) b, match_args), v) + (Parse_Tools.the_real_val b, att)) b, match_args), v) | _ => raise Fail "Expected closed term") ts - val fixes' = map (fn ((p, _),_) => Parse_Tools.the_real_val p) fixes + val fixes' = map (fn ((p, _), _) => Parse_Tools.the_real_val p) fixes in (ts', fixes', text) end | SOME _ => error "Unexpected token value in match cartouche" | NONE => let - val fixes' = map (fn ((pb, otyp),_) => (Parse_Tools.the_parse_val pb, otyp, NoSyn)) fixes; + val fixes' = map (fn ((pb, otyp), _) => (Parse_Tools.the_parse_val pb, otyp, NoSyn)) fixes; val (fixes'', ctxt1) = Proof_Context.read_vars fixes' ctxt; val (fix_nms, ctxt2) = Proof_Context.add_fixes fixes'' ctxt1; @@ -135,9 +132,11 @@ val pat_fixes = fold (Term.add_frees) pats [] |> map fst; - val _ = map2 (fn nm => fn (_,pos) => member (op =) pat_fixes nm orelse - error ("For-fixed variable must be bound in some pattern." ^ Position.here pos)) - fix_nms fixes; + val _ = + map2 (fn nm => fn (_, pos) => + member (op =) pat_fixes nm orelse + error ("For-fixed variable must be bound in some pattern" ^ Position.here pos)) + fix_nms fixes; val _ = map (Term.map_types Type.no_tvars) pats @@ -164,20 +163,27 @@ val param_thm = map (Drule.mk_term o Thm.cterm_of ctxt' o Free) abs_nms |> Conjunction.intr_balanced - |> Drule.generalize ([], map fst abs_nms); + |> Drule.generalize ([], map fst abs_nms) + |> Method_Closure.tag_free_thm; - val thm = + val atts = map (Attrib.attribute ctxt') att; + val (param_thm', ctxt'') = Thm.proof_attributes atts param_thm ctxt'; + + fun label_thm thm = Thm.cterm_of ctxt' (Free (nm, propT)) |> Drule.mk_term - |> not (null abs_nms) ? Conjunction.intr param_thm - |> Drule.zero_var_indexes - |> Method_Closure.tag_free_thm; + |> not (null abs_nms) ? Conjunction.intr thm + + val [head_thm, body_thm] = + Drule.zero_var_indexes_list (map label_thm [param_thm, param_thm']) + |> map Method_Closure.tag_free_thm; - (*TODO: Preprocess attributes here?*) - - val (_, ctxt'') = Proof_Context.note_thmss "" [((b, []), [([thm], [])])] ctxt'; + val ctxt''' = + Attrib.local_notes "" [((b, []), [([body_thm], [])])] ctxt'' + |> snd + |> Variable.declare_maxidx (Thm.maxidx_of head_thm); in - (SOME (Thm.prop_of thm, map (Attrib.attribute ctxt) att) :: tms, ctxt'') + (SOME (Thm.prop_of head_thm, att) :: tms, ctxt''') end | upd_ctxt NONE _ (tms, ctxt) = (NONE :: tms, ctxt); @@ -196,7 +202,20 @@ val pats' = map (Term.map_types Type_Infer.paramify_vars #> Morphism.term morphism) pats; val _ = ListPair.app (fn ((_, (Parse_Tools.Parse_Val (_, f), _)), t) => f t) (ts, pats'); - val binds' = map (Option.map (fn (t, atts) => (Morphism.term morphism t, atts))) binds; + fun close_src src = + let + val src' = Token.closure_src src |> Token.transform_src morphism; + val _ = + map2 (fn tok1 => fn tok2 => + (case (Token.get_value tok2) of + SOME value => Token.assign (SOME value) tok1 + | NONE => ())) + (Token.args_of_src src) + (Token.args_of_src src'); + in src' end; + + val binds' = + map (Option.map (fn (t, atts) => (Morphism.term morphism t, map close_src atts))) binds; val _ = ListPair.app @@ -207,7 +226,8 @@ val real_fixes' = map (Morphism.term morphism) real_fixes; val _ = - ListPair.app (fn (( (Parse_Tools.Parse_Val (_, f),_) , _), t) => f t) (fixes, real_fixes'); + ListPair.app (fn (( (Parse_Tools.Parse_Val (_, f), _) , _), t) => f t) + (fixes, real_fixes'); val match_args = map (fn (_, (_, match_args)) => match_args) ts; val binds'' = (binds' ~~ match_args) ~~ pats'; @@ -247,36 +267,30 @@ (fn ((((SOME ((_, head), att), _), _), _), thms) => SOME (head, (thms, att)) | _ => NONE) fact_insts'; - fun apply_attribute thm att ctxt = - let - val (opt_context', thm') = att (Context.Proof ctxt, thm) - in - (case thm' of - SOME _ => error "Rule attributes cannot be applied here" - | _ => the_default ctxt (Option.map Context.proof_of opt_context')) - end; - - fun apply_attributes atts thm = fold (apply_attribute thm) atts; - - (*TODO: What to do about attributes that raise errors?*) - val (fact_insts, ctxt') = - fold_map (fn (head, (thms, atts : attribute list)) => fn ctxt => - ((head, thms), fold (apply_attributes atts) thms ctxt)) fact_insts ctxt; - fun try_dest_term thm = try (Thm.prop_of #> dest_internal_fact #> snd) thm; - fun expand_fact thm = + fun expand_fact fact_insts thm = the_default [thm] (case try_dest_term thm of SOME t_ident => AList.lookup (op aconv) fact_insts t_ident | NONE => NONE); - val morphism = + fun fact_morphism fact_insts = Morphism.term_morphism "do_inst.term" (Envir.norm_term env) $> Morphism.typ_morphism "do_inst.type" (Envir.norm_type (Envir.type_env env)) $> - Morphism.fact_morphism "do_inst.fact" (maps expand_fact); + Morphism.fact_morphism "do_inst.fact" (maps (expand_fact fact_insts)); - val text' = Method.map_source (Token.transform_src morphism) text; + fun apply_attribute (head, (fact, atts)) (fact_insts, ctxt) = + let + val morphism = fact_morphism fact_insts; + val atts' = map (Attrib.attribute ctxt o Token.transform_src morphism) atts; + val (fact'', ctxt') = fold_map (Thm.proof_attributes atts') fact ctxt; + in ((head, fact'') :: fact_insts, ctxt') end; + + (*TODO: What to do about attributes that raise errors?*) + val (fact_insts', ctxt') = fold_rev (apply_attribute) fact_insts ([], ctxt); + + val text' = Method.map_source (Token.transform_src (fact_morphism fact_insts')) text; in (text', ctxt') end; @@ -304,27 +318,27 @@ let val tenv = Envir.term_env env; val tyenv = Envir.type_env env; - val max_tidx = Vartab.fold (fn (_,(_,t)) => curry Int.max (maxidx_of_term t)) tenv ~1; - val max_Tidx = Vartab.fold (fn (_,(_,T)) => curry Int.max (maxidx_of_typ T)) tyenv ~1; + val max_tidx = Vartab.fold (fn (_, (_, t)) => curry Int.max (maxidx_of_term t)) tenv ~1; + val max_Tidx = Vartab.fold (fn (_, (_, T)) => curry Int.max (maxidx_of_typ T)) tyenv ~1; in Envir.Envir - {maxidx = Int.max (Int.max (max_tidx,max_Tidx),Envir.maxidx_of env), + {maxidx = Int.max (Int.max (max_tidx, max_Tidx), Envir.maxidx_of env), tenv = tenv, tyenv = tyenv} end fun match_filter_env inner_ctxt morphism pat_vars fixes (ts, params) thm inner_env = let val tenv = Envir.term_env inner_env - |> Vartab.map (K (fn (T,t) => (Morphism.typ morphism T,Morphism.term morphism t))); + |> Vartab.map (K (fn (T, t) => (Morphism.typ morphism T, Morphism.term morphism t))); val tyenv = Envir.type_env inner_env - |> Vartab.map (K (fn (S,T) => (S,Morphism.typ morphism T))); + |> Vartab.map (K (fn (S, T) => (S, Morphism.typ morphism T))); val outer_env = Envir.Envir {maxidx = Envir.maxidx_of inner_env, tenv = tenv, tyenv = tyenv}; val param_vars = map Term.dest_Var params; - val params' = map (fn (xi,_) => Vartab.lookup (Envir.term_env outer_env) xi) param_vars; + val params' = map (fn (xi, _) => Vartab.lookup (Envir.term_env outer_env) xi) param_vars; val fixes_vars = map Term.dest_Var fixes; @@ -339,11 +353,11 @@ Envir.Envir {maxidx = Envir.maxidx_of outer_env, tenv = tenv', tyenv = tyenv} |> recalculate_maxidx; - val all_params_bound = forall (fn SOME (_,(Var _)) => true | _ => false) params'; + val all_params_bound = forall (fn SOME (_, Var _) => true | _ => false) params'; val pat_fixes = inter (eq_fst (op =)) fixes_vars pat_vars; - val all_pat_fixes_bound = forall (fn (xi,_) => is_some (Vartab.lookup tenv' xi)) pat_fixes; + val all_pat_fixes_bound = forall (fn (xi, _) => is_some (Vartab.lookup tenv' xi)) pat_fixes; val thm' = Morphism.thm morphism thm; @@ -469,7 +483,7 @@ SOME (x, seq') => if member eq prev x then Seq.pull (deduplicate eq prev seq') - else SOME (x,deduplicate eq (x :: prev) seq') + else SOME (x, deduplicate eq (x :: prev) seq') | NONE => NONE)); fun consistent_env env = @@ -480,7 +494,7 @@ forall (fn (_, (T, t)) => Envir.norm_type tyenv T = fastype_of t) (Vartab.dest tenv) end; -fun eq_env (env1,env2) = +fun eq_env (env1, env2) = let val tyenv1 = Envir.type_env env1; val tyenv2 = Envir.type_env env2; @@ -492,7 +506,7 @@ Envir.eta_contract (Envir.norm_term env2 t'))) (apply2 Vartab.dest (Envir.term_env env1, Envir.term_env env2)) andalso - ListPair.allEq (fn ((var, (_, T)), (var', (_,T'))) => + ListPair.allEq (fn ((var, (_, T)), (var', (_, T'))) => var = var' andalso Envir.norm_type tyenv1 T = Envir.norm_type tyenv2 T') (apply2 Vartab.dest (Envir.type_env env1, Envir.type_env env2)) end; @@ -505,15 +519,13 @@ fun match_thm (((x, params), pat), thm) env = let - fun try_dest_term term = the_default term (try Logic.dest_term term); - val pat_vars = Term.add_vars pat []; - val pat' = pat |> Envir.norm_term env |> try_dest_term; + val pat' = pat |> Envir.norm_term env; - val (((Tinsts', insts),[thm']), inner_ctxt) = Variable.import false [thm] ctxt + val (((Tinsts', insts), [thm']), inner_ctxt) = Variable.import false [thm] ctxt; - val item' = Thm.prop_of thm' |> try_dest_term; + val item' = Thm.prop_of thm'; val ts = Option.map (fst o fst) (fst x); @@ -572,7 +584,6 @@ |> Seq.map (fn (fact_insts, env) => do_inst fact_insts env text ctxt') end; - (*TODO: Slightly hacky re-use of fact match implementation in plain term matching *) fun make_term_matches ctxt get = let val pats' = diff -r 6a5015b096a2 -r f7e4294216d2 src/HOL/Eisbach/method_closure.ML --- a/src/HOL/Eisbach/method_closure.ML Sun May 03 18:45:58 2015 +0200 +++ b/src/HOL/Eisbach/method_closure.ML Sun May 03 18:51:26 2015 +0200 @@ -1,4 +1,4 @@ -(* Title: method_closure.ML +(* Title: HOL/Eisbach/method_closure.ML Author: Daniel Matichuk, NICTA/UNSW Facilities for treating method syntax as a closure, with abstraction @@ -13,6 +13,7 @@ val is_dummy: thm -> bool val tag_free_thm: thm -> thm val free_aware_rule_attribute: thm list -> (Context.generic -> thm -> thm) -> Thm.attribute + val wrap_attribute: bool -> Binding.binding -> theory -> theory val read_inner_method: Proof.context -> Token.src -> Method.text val read_text_closure: Proof.context -> Token.src -> Token.src * Method.text val read_inner_text_closure: Proof.context -> Input.source -> Token.src * Method.text @@ -35,12 +36,10 @@ structure Data = Generic_Data ( - type T = - ((term list * (string list * string list)) * Method.text) Symtab.table; + type T = ((term list * (string list * string list)) * Method.text) Symtab.table; val empty: T = Symtab.empty; val extend = I; - fun merge (methods1,methods2) : T = - (Symtab.merge (K true) (methods1, methods2)); + fun merge data : T = Symtab.merge (K true) data; ); val get_methods = Data.get o Context.Proof; @@ -88,6 +87,32 @@ if exists is_free_thm (thm :: args) then dummy_free_thm else f context thm); +fun free_aware_attribute thy declaration src (context, thm) = + let + val src' = Token.init_assignable_src src; + fun apply_att thm = (Attrib.attribute_global thy src') (context, thm); + val _ = try apply_att Drule.dummy_thm; + val src'' = Token.closure_src src'; + val thms = + map_filter Token.get_value (Token.args_of_src src'') + |> map_filter (fn (Token.Fact (_, f)) => SOME f | _ => NONE) + |> flat; + in + if exists is_free_thm (thm :: thms) then + if declaration then (NONE, NONE) + else (NONE, SOME dummy_free_thm) + else apply_att thm + end; + +fun wrap_attribute declaration binding thy = + let + val name = Binding.name_of binding; + val name' = Attrib.check_name_generic (Context.Theory thy) (name, Position.none); + fun get_src src = Token.src (name', Token.range_of_src src) (Token.args_of_src src); + in + Attrib.define_global binding (free_aware_attribute thy declaration o get_src) "" thy + |> snd + end; (* thm semantics for combined methods with internal parser. Simulates outer syntax parsing. *) (* Creates closures for each combined method while parsing, based on the parse context *) @@ -108,7 +133,8 @@ val method_text = read_inner_method ctxt src; val method_text' = Method.map_source (Method.method_closure ctxt) method_text; (*FIXME: Does not markup method parameters. Needs to be done by Method.parser' directly. *) - val _ = Method.map_source (fn src => (try (Method.check_name ctxt) (Token.name_of_src src);src)) method_text; + val _ = Method.map_source (fn src => + (try (Method.check_name ctxt) (Token.name_of_src src);src)) method_text; val src' = Token.closure_src src; in (src', method_text') end; @@ -127,7 +153,7 @@ NONE => let val input = Token.input_of tok; - val (src,text) = read_inner_text_closure ctxt input; + val (src, text) = read_inner_text_closure ctxt input; val _ = Token.assign (SOME (Token.Source src)) tok; in text end | SOME (Token.Source src) => read_inner_method ctxt src diff -r 6a5015b096a2 -r f7e4294216d2 src/HOL/Eisbach/parse_tools.ML --- a/src/HOL/Eisbach/parse_tools.ML Sun May 03 18:45:58 2015 +0200 +++ b/src/HOL/Eisbach/parse_tools.ML Sun May 03 18:51:26 2015 +0200 @@ -1,4 +1,4 @@ -(* Title: parse_tools.ML +(* Title: HOL/Eisbach/parse_tools.ML Author: Daniel Matichuk, NICTA/UNSW Simple tools for deferred stateful token values.