# HG changeset patch # User wenzelm # Date 1377280407 -7200 # Node ID e2d31807cbf6566470614731c71fa65e35ee93b9 # Parent d998de7f0efccf94e741a02f590259587ae0ad3c clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context; subtle change of semantics of ML_Context.add_antiq: need to avoid accidental update of context due to concrete syntax parser (cf. Scan.pass); diff -r d998de7f0efc -r e2d31807cbf6 src/Pure/ML/ml_antiquote.ML --- a/src/Pure/ML/ml_antiquote.ML Fri Aug 23 17:01:12 2013 +0200 +++ b/src/Pure/ML/ml_antiquote.ML Fri Aug 23 19:53:27 2013 +0200 @@ -7,9 +7,7 @@ signature ML_ANTIQUOTE = sig val variant: string -> Proof.context -> string * Proof.context - val macro: binding -> Proof.context context_parser -> theory -> theory val inline: binding -> string context_parser -> theory -> theory - val declaration: string -> binding -> string context_parser -> theory -> theory val value: binding -> string context_parser -> theory -> theory end; @@ -38,23 +36,20 @@ (* specific antiquotations *) -fun macro name scan = ML_Context.add_antiq name - (fn _ => scan :|-- (fn ctxt => Scan.depend (fn _ => Scan.succeed - (Context.Proof ctxt, fn background => (K ("", ""), background))))); - -fun inline name scan = ML_Context.add_antiq name - (fn _ => scan >> (fn s => fn background => (K ("", s), background))); +fun inline name scan = + ML_Context.add_antiq name + (Scan.depend (fn context => Scan.pass context scan >> (fn s => (context, K ("", s))))); -fun declaration kind name scan = ML_Context.add_antiq name - (fn _ => scan >> (fn s => fn background => - let - val (a, background') = - variant (translate_string (fn "." => "_" | c => c) (Binding.name_of name)) background; - val env = kind ^ " " ^ a ^ " = " ^ s ^ ";\n"; - val body = "Isabelle." ^ a; - in (K (env, body), background') end)); - -val value = declaration "val"; +fun value name scan = + ML_Context.add_antiq name + (Scan.depend (fn context => Scan.pass context scan >> (fn s => + let + val ctxt = Context.the_proof context; + val (a, ctxt') = + variant (translate_string (fn "." => "_" | c => c) (Binding.name_of name)) ctxt; + val env = "val " ^ a ^ " = " ^ s ^ ";\n"; + val body = "Isabelle." ^ a; + in (Context.Proof ctxt', (K (env, body))) end))); diff -r d998de7f0efc -r e2d31807cbf6 src/Pure/ML/ml_context.ML --- a/src/Pure/ML/ml_context.ML Fri Aug 23 17:01:12 2013 +0200 +++ b/src/Pure/ML/ml_context.ML Fri Aug 23 19:53:27 2013 +0200 @@ -23,8 +23,8 @@ val get_stored_thm: unit -> thm val ml_store_thms: string * thm list -> unit val ml_store_thm: string * thm -> unit - type antiq = Proof.context -> (Proof.context -> string * string) * Proof.context - val add_antiq: binding -> (Position.T -> antiq context_parser) -> theory -> theory + type antiq = Proof.context -> string * string + val add_antiq: binding -> antiq context_parser -> theory -> theory val check_antiq: theory -> xstring * Position.T -> string val trace_raw: Config.raw val trace: bool Config.T @@ -97,11 +97,11 @@ (* antiquotation commands *) -type antiq = Proof.context -> (Proof.context -> string * string) * Proof.context; +type antiq = Proof.context -> string * string; structure Antiq_Parsers = Theory_Data ( - type T = (Position.T -> antiq context_parser) Name_Space.table; + type T = antiq context_parser 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; @@ -117,7 +117,7 @@ val thy = Proof_Context.theory_of ctxt; val ((xname, _), pos) = Args.dest_src src; val (_, scan) = Name_Space.check (Context.Proof ctxt) (Antiq_Parsers.get thy) (xname, pos); - in Args.context_syntax Markup.ML_antiquotationN (scan pos) src ctxt end; + in Args.context_syntax Markup.ML_antiquotationN scan src ctxt end; (* parsing and evaluation *) @@ -160,9 +160,7 @@ fun expand (Antiquote.Text tok) ctxt = (K ([], [tok]), ctxt) | expand (Antiquote.Antiq (ss, range)) ctxt = let - val (f, _) = - antiquotation (Token.read_antiq lex antiq (ss, #1 range)) ctxt; - val (decl, ctxt') = f ctxt; (* FIXME ?? *) + val (decl, ctxt') = antiquotation (Token.read_antiq lex antiq (ss, #1 range)) ctxt; val decl' = decl #> pairself (ML_Lex.tokenize #> map (ML_Lex.set_range range)); in (decl', ctxt') end; diff -r d998de7f0efc -r e2d31807cbf6 src/Pure/ML/ml_thms.ML --- a/src/Pure/ML/ml_thms.ML Fri Aug 23 17:01:12 2013 +0200 +++ b/src/Pure/ML/ml_thms.ML Fri Aug 23 19:53:27 2013 +0200 @@ -37,43 +37,50 @@ val _ = Context.>> (Context.map_theory (ML_Context.add_antiq (Binding.name "attributes") - (fn _ => Scan.lift Parse_Spec.attribs >> (fn raw_srcs => fn background => + (Scan.depend (fn context => Parse_Spec.attribs >> (fn raw_srcs => let - val thy = Proof_Context.theory_of background; + val ctxt = Context.the_proof context; + val thy = Proof_Context.theory_of ctxt; val i = serial (); val srcs = map (Attrib.intern_src thy) raw_srcs; - val _ = map (Attrib.attribute background) srcs; - val (a, background') = background + val _ = map (Attrib.attribute ctxt) srcs; + val (a, ctxt') = ctxt |> ML_Antiquote.variant "attributes" ||> put_attributes (i, srcs); val ml = ("val " ^ a ^ " = ML_Thms.the_attributes ML_context " ^ string_of_int i ^ ";\n", "Isabelle." ^ a); - in (K ml, background') end)))); + in (Context.Proof ctxt', K ml) end))))); (* fact references *) -fun thm_binding kind is_single thms background = +fun thm_binding kind is_single context thms = let - val initial = null (get_thmss background); - val (name, background') = ML_Antiquote.variant kind background; - val background'' = cons_thms ((name, is_single), thms) background'; + val ctxt = Context.the_proof context; + + val initial = null (get_thmss ctxt); + val (name, ctxt') = ML_Antiquote.variant kind ctxt; + val ctxt'' = cons_thms ((name, is_single), thms) ctxt'; val ml_body = "Isabelle." ^ name; - fun decl ctxt = + fun decl final_ctxt = if initial then let - val binds = get_thmss ctxt |> map (fn ((a, b), _) => (b ? enclose "[" "]") a); + val binds = get_thmss final_ctxt |> map (fn ((a, b), _) => (b ? enclose "[" "]") a); val ml_env = "val [" ^ commas binds ^ "] = ML_Thms.the_thmss ML_context;\n"; in (ml_env, ml_body) end else ("", ml_body); - in (decl, background'') end; + in (Context.Proof ctxt'', decl) end; val _ = Context.>> (Context.map_theory - (ML_Context.add_antiq (Binding.name "thm") (K (Attrib.thm >> (thm_binding "thm" true o single))) #> - ML_Context.add_antiq (Binding.name "thms") (K (Attrib.thms >> thm_binding "thms" false)))); + (ML_Context.add_antiq (Binding.name "thm") + (Scan.depend (fn context => + Scan.pass context Attrib.thm >> (thm_binding "thm" true context o single))) #> + ML_Context.add_antiq (Binding.name "thms") + (Scan.depend (fn context => + Scan.pass context Attrib.thms >> thm_binding "thms" false context)))); (* ad-hoc goals *) @@ -85,24 +92,26 @@ val _ = Context.>> (Context.map_theory (ML_Context.add_antiq (Binding.name "lemma") - (fn _ => Args.context -- - Scan.lift (Args.mode "open" -- Parse.and_list1 (Scan.repeat1 goal) -- - (by |-- Method.parse -- Scan.option Method.parse)) >> - (fn (ctxt, ((is_open, raw_propss), methods)) => - let - val propss = burrow (map (rpair []) o Syntax.read_props ctxt) raw_propss; - val prep_result = Goal.norm_result #> not is_open ? Thm.close_derivation; - fun after_qed res goal_ctxt = - Proof_Context.put_thms false (Auto_Bind.thisN, - SOME (map prep_result (Proof_Context.export goal_ctxt ctxt (flat res)))) goal_ctxt; + (Scan.depend (fn context => + Args.mode "open" -- Parse.and_list1 (Scan.repeat1 goal) -- + (by |-- Method.parse -- Scan.option Method.parse) >> + (fn ((is_open, raw_propss), methods) => + let + val ctxt = Context.proof_of context; - val ctxt' = ctxt - |> Proof.theorem NONE after_qed propss - |> Proof.global_terminal_proof methods; - val thms = - Proof_Context.get_fact ctxt' - (Facts.named (Proof_Context.full_name ctxt' (Binding.name Auto_Bind.thisN))); - in thm_binding "lemma" (length (flat propss) = 1) thms end)))); + val propss = burrow (map (rpair []) o Syntax.read_props ctxt) raw_propss; + val prep_result = Goal.norm_result #> not is_open ? Thm.close_derivation; + fun after_qed res goal_ctxt = + Proof_Context.put_thms false (Auto_Bind.thisN, + SOME (map prep_result (Proof_Context.export goal_ctxt ctxt (flat res)))) goal_ctxt; + + val ctxt' = ctxt + |> Proof.theorem NONE after_qed propss + |> Proof.global_terminal_proof methods; + val thms = + Proof_Context.get_fact ctxt' + (Facts.named (Proof_Context.full_name ctxt' (Binding.name Auto_Bind.thisN))); + in thm_binding "lemma" (length (flat propss) = 1) context thms end))))); end; diff -r d998de7f0efc -r e2d31807cbf6 src/Tools/Code/code_runtime.ML --- a/src/Tools/Code/code_runtime.ML Fri Aug 23 17:01:12 2013 +0200 +++ b/src/Tools/Code/code_runtime.ML Fri Aug 23 19:53:27 2013 +0200 @@ -247,12 +247,15 @@ in -fun ml_code_antiq raw_const background = +fun ml_code_antiq context raw_const = let - val const = Code.check_const (Proof_Context.theory_of background) raw_const; - val is_first = is_first_occ background; - val background' = register_const const background; - in (print_code is_first const, background') end; + val ctxt = Context.the_proof context; + val thy = Proof_Context.theory_of ctxt; + + val const = Code.check_const thy raw_const; + val is_first = is_first_occ ctxt; + val ctxt' = register_const const ctxt; + in (Context.Proof ctxt', print_code is_first const) end; end; (*local*) @@ -344,7 +347,8 @@ val _ = Context.>> (Context.map_theory - (ML_Context.add_antiq @{binding code} (fn _ => Args.term >> ml_code_antiq))); + (ML_Context.add_antiq @{binding code} + (Scan.depend (fn context => Scan.pass context Args.term >> ml_code_antiq context)))); local