# HG changeset patch # User wenzelm # Date 1393580404 -3600 # Node ID 2d4cf0005a02741db7b3880e9394b855eacc366d # Parent 8f4c6ef220e33c80efcb18930b950ceb0b61fb6d more explicit method reports; avoid combinator parsers with observable effect -- unreliable due to backtracking (Scan.FAIL) and incremental input (Scan.MORE); diff -r 8f4c6ef220e3 -r 2d4cf0005a02 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Thu Feb 27 21:36:40 2014 +0100 +++ b/src/Pure/Isar/isar_syn.ML Fri Feb 28 10:40:04 2014 +0100 @@ -620,11 +620,12 @@ val _ = Outer_Syntax.command @{command_spec "qed"} "conclude proof" - (Scan.option Method.parse_report >> Isar_Cmd.qed); + (Scan.option Method.parse >> (fn m => (Option.map Method.report m; Isar_Cmd.qed m))); val _ = Outer_Syntax.command @{command_spec "by"} "terminal backward proof" - (Method.parse_report -- Scan.option Method.parse_report >> Isar_Cmd.terminal_proof); + (Method.parse -- Scan.option Method.parse >> (fn (m1, m2) => + (Method.report m1; Option.map Method.report m2; Isar_Cmd.terminal_proof (m1, m2)))); val _ = Outer_Syntax.command @{command_spec ".."} "default proof" @@ -659,17 +660,21 @@ val _ = Outer_Syntax.command @{command_spec "apply"} "initial refinement step (unstructured)" - (Method.parse_report >> (Toplevel.print oo (Toplevel.proofs o Proof.apply_results))); + (Method.parse >> (fn m => + (Method.report m; Toplevel.print o Toplevel.proofs (Proof.apply_results m)))); val _ = Outer_Syntax.command @{command_spec "apply_end"} "terminal refinement step (unstructured)" - (Method.parse_report >> (Toplevel.print oo (Toplevel.proofs o Proof.apply_end_results))); + (Method.parse >> (fn m => + (Method.report m; Toplevel.print o Toplevel.proofs (Proof.apply_end_results m)))); val _ = Outer_Syntax.command @{command_spec "proof"} "backward proof step" - (Scan.option Method.parse_report >> (fn m => Toplevel.print o - Toplevel.actual_proof (Proof_Node.applys (Proof.proof_results m)) o - Toplevel.skip_proof (fn i => i + 1))); + (Scan.option Method.parse >> (fn m => + (Option.map Method.report m; + Toplevel.print o + Toplevel.actual_proof (Proof_Node.applys (Proof.proof_results m)) o + Toplevel.skip_proof (fn i => i + 1)))); (* proof navigation *) diff -r 8f4c6ef220e3 -r 2d4cf0005a02 src/Pure/Isar/method.ML --- a/src/Pure/Isar/method.ML Thu Feb 27 21:36:40 2014 +0100 +++ b/src/Pure/Isar/method.ML Fri Feb 28 10:40:04 2014 +0100 @@ -76,9 +76,9 @@ type text_range = text * Position.range val text: text_range option -> text option val position: text_range option -> Position.T + val reports_of: text_range -> Position.report list + val report: text_range -> unit val parse: text_range parser - val parse_report: text_range parser - val parse_context_report: text_range context_parser end; structure Method: METHOD = @@ -298,19 +298,6 @@ Repeat1 of combinator_info * text | Select_Goals of combinator_info * int * text; -fun keyword_positions (Source _) = [] - | keyword_positions (Basic _) = [] - | keyword_positions (Then (Combinator_Info {keywords}, texts)) = - keywords @ maps keyword_positions texts - | keyword_positions (Orelse (Combinator_Info {keywords}, texts)) = - keywords @ maps keyword_positions texts - | keyword_positions (Try (Combinator_Info {keywords}, text)) = - keywords @ keyword_positions text - | keyword_positions (Repeat1 (Combinator_Info {keywords}, text)) = - keywords @ keyword_positions text - | keyword_positions (Select_Goals (Combinator_Info {keywords}, _, text)) = - keywords @ keyword_positions text; - 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)); @@ -421,9 +408,6 @@ type text_range = text * Position.range; -fun reports (text, (pos, _)) = - (pos, Markup.language_method) :: map (rpair Markup.keyword3) (keyword_positions text); - fun text NONE = NONE | text (SOME (txt, _)) = SOME txt; @@ -431,6 +415,34 @@ | position (SOME (_, (pos, _))) = pos; +(* reports *) + +local + +fun keyword_positions (Source _) = [] + | keyword_positions (Basic _) = [] + | keyword_positions (Then (Combinator_Info {keywords}, texts)) = + keywords @ maps keyword_positions texts + | keyword_positions (Orelse (Combinator_Info {keywords}, texts)) = + keywords @ maps keyword_positions texts + | keyword_positions (Try (Combinator_Info {keywords}, text)) = + keywords @ keyword_positions text + | keyword_positions (Repeat1 (Combinator_Info {keywords}, text)) = + keywords @ keyword_positions text + | keyword_positions (Select_Goals (Combinator_Info {keywords}, _, text)) = + keywords @ keyword_positions text; + +in + +fun reports_of ((text, (pos, _)): text_range) = + (pos, Markup.language_method) :: + map (rpair Markup.keyword3) (keyword_positions text); + +val report = Position.reports o reports_of; + +end; + + (* outer parser *) fun is_symid_meth s = @@ -468,12 +480,6 @@ val parse = Scan.trace meth3 >> (fn (m, toks) => (m, Token.range_of toks)); -(*parse with observable effect!*) -val parse_report = parse >> (tap (Position.reports o reports)); -val parse_context_report = - Args.context -- Scan.lift parse >> - (fn (ctxt, text_range) => (Context_Position.reports ctxt (reports text_range); text_range)); - end; diff -r 8f4c6ef220e3 -r 2d4cf0005a02 src/Pure/ML/ml_thms.ML --- a/src/Pure/ML/ml_thms.ML Thu Feb 27 21:36:40 2014 +0100 +++ b/src/Pure/ML/ml_thms.ML Fri Feb 28 10:40:04 2014 +0100 @@ -91,13 +91,15 @@ (ML_Context.add_antiq @{binding lemma} (Scan.depend (fn context => Args.mode "open" -- Parse.enum1_positions "and" (Scan.repeat1 goal) -- - (Parse.position by -- - Scan.pass context (Method.parse_context_report -- Scan.option Method.parse_context_report)) - >> (fn ((is_open, (raw_propss, and_positions)), ((_, by_pos), methods)) => + Parse.position by -- Method.parse -- Scan.option Method.parse + >> (fn ((((is_open, (raw_propss, and_positions)), (_, by_pos)), m1), m2) => let val ctxt = Context.proof_of context; - val reports = (by_pos, Markup.keyword1) :: map (rpair Markup.keyword2) and_positions; + val reports = + (by_pos, Markup.keyword1) :: + map (rpair Markup.keyword2) and_positions @ + maps Method.reports_of (m1 :: the_list m2); val _ = Context_Position.reports ctxt reports; val propss = burrow (map (rpair []) o Syntax.read_props ctxt) raw_propss; @@ -108,7 +110,7 @@ val ctxt' = ctxt |> Proof.theorem NONE after_qed propss - |> Proof.global_terminal_proof methods; + |> Proof.global_terminal_proof (m1, m2); val thms = Proof_Context.get_fact ctxt' (Facts.named (Proof_Context.full_name ctxt' (Binding.name Auto_Bind.thisN))); diff -r 8f4c6ef220e3 -r 2d4cf0005a02 src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Thu Feb 27 21:36:40 2014 +0100 +++ b/src/Pure/Thy/thy_output.ML Fri Feb 28 10:40:04 2014 +0100 @@ -616,17 +616,19 @@ val _ = Theory.setup (antiquotation (Binding.name "lemma") (Args.prop -- - Scan.lift (Parse.position (Args.$$$ "by")) -- - (Method.parse_context_report -- Scan.option Method.parse_context_report)) - (fn {source, context = ctxt, ...} => fn ((prop, (_, by_pos)), methods) => + Scan.lift (Parse.position (Args.$$$ "by") -- Method.parse -- Scan.option Method.parse)) + (fn {source, context = ctxt, ...} => fn (prop, (((_, by_pos), m1), m2)) => let val prop_src = (case Args.dest_src source of ((a, arg :: _), pos) => Args.src ((a, [arg]), pos)); - val _ = Context_Position.report ctxt by_pos Markup.keyword1; + + val reports = (by_pos, Markup.keyword1) :: maps Method.reports_of (m1 :: the_list m2); + val _ = Context_Position.reports ctxt reports; + (* FIXME check proof!? *) val _ = ctxt |> Proof.theorem NONE (K I) [[(prop, [])]] - |> Proof.global_terminal_proof methods; + |> Proof.global_terminal_proof (m1, m2); in output ctxt (maybe_pretty_source pretty_term ctxt prop_src [prop]) end));