1.1 --- a/src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy Mon Dec 21 11:55:10 2020 +0100
1.2 +++ b/src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy Mon Dec 21 15:13:49 2020 +0100
1.3 @@ -21,11 +21,20 @@
1.4 spark_vc procedure_g_c_d_4 (*..select 1st VC for proof: *)
1.5 proof -
1.6 from \<open>0 < d\<close> have "0 \<le> c mod d" by (rule pos_mod_sign)
1.7 +(*^^^^^^^^^^^^-Syntax.read_props..Output.report
1.8 + ^^^^^^^^^^^^^^^^^-Proof.gen_have..Output.report 2x
1.9 + ^^^^^^^^^^^^^^^^^^^^^^-have 0 \<le> c mod d*)
1.10 with \<open>0 \<le> c\<close> \<open>0 < d\<close> \<open>c - c sdiv d * d \<noteq> 0\<close> show ?C1
1.11 +(*^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^-Proof.gen_show....Output.report 2x
1.12 + ^^^^^^^^-Proof.gen_show..Output.report 2x*)
1.13 by (simp add: sdiv_pos_pos minus_div_mult_eq_mod [symmetric])
1.14 +(* ^^^ Successful attempt to solve goal by exported rule: 0 < c - c sdiv d * d*)
1.15 next
1.16 from \<open>0 \<le> c\<close> \<open>0 < d\<close> \<open>gcd c d = gcd m n\<close> show ?C2
1.17 +(*^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^-Syntax.read_props....Output.report 3x
1.18 + ^^^^^^^^-Proof.gen_show..Output.report 2x*)
1.19 by (simp add: sdiv_pos_pos minus_div_mult_eq_mod [symmetric] gcd_non_0_int)
1.20 +(* ^^^-Successful attempt to solve goal by exported rule: gcd d (c - c sdiv d * d) = gcd m n*)
1.21 qed
1.22
1.23 subsection \<open>observing interaction on the proof\<close>
1.24 @@ -82,12 +91,12 @@
1.25 ### Private_Output.report cartouch
1.26 ### Private_Output.report delimite
1.27 ### Private_Output.report entityo
1.28 -##### Syntax.read_props
1.29 +##### Syntax.read_props
1.30 #### Syntax_Phases.check_props
1.31 ### Syntax_Phases.check_terms
1.32 ### Syntax_Phases.check_typs
1.33 ### Syntax_Phases.check_typs
1.34 -### calling Output.report
1.35 +## calling Output.report
1.36 ### Private_Output.report typingo =====
1.37 ### Context_Position.report_generic //--- different to subsequent part below
1.38 ### Private_Output.report entityo
1.39 @@ -99,20 +108,22 @@
1.40 ### Private_Output.report cartouch
1.41 ### Private_Output.report delimite
1.42 ### Private_Output.report entityo
1.43 +####-# Proof.gen_have
1.44 ##### Syntax.read_props
1.45 #### Syntax_Phases.check_props
1.46 ### Syntax_Phases.check_terms
1.47 ### Syntax_Phases.check_typs
1.48 ### Syntax_Phases.check_typs
1.49 -### calling Output.report
1.50 +## calling Output.report
1.51 ### Private_Output.report typingo =====//--- different to previous part above
1.52 ##### Syntax.read_props
1.53 #### Syntax_Phases.check_props
1.54 ### Syntax_Phases.check_terms
1.55 ### Syntax_Phases.check_typs
1.56 -### calling Output.report\<close>
1.57 +## calling Output.report\<close>
1.58
1.59 subsection \<open>signatures of the traced callers of Private_Output.report\<close>
1.60 +declare [[ML_print_depth = 99999]]
1.61 ML \<open>
1.62 \<close> ML \<open>
1.63 Token.syntax_generic : 'a Token.context_parser -> Token.src -> Context.generic ->
1.64 @@ -123,7 +134,28 @@
1.65 (*Syntax_Phases.check_terms : Proof.context -> term list -> term list; ..local*)
1.66 Syntax.check_typs : Proof.context -> typ list -> typ list;
1.67 Syntax.check_terms : Proof.context -> term list -> term list;
1.68 - Syntax.read_props : Proof.context -> string list -> term list
1.69 + Syntax.read_props : Proof.context -> string list -> term list;
1.70 +(*Proof.gen_have:
1.71 + ('a -> 'b list -> 'b list -> context ->
1.72 + {assumes: term list list,
1.73 + fixes: (string * term) list,
1.74 + result_binds: (indexname * term option) list,
1.75 + result_text: term, shows: term list list, text: term}
1.76 + *
1.77 + context)
1.78 + ->
1.79 + (context -> 'c -> attribute) -> bool -> Method.text option ->
1.80 + (context * thm list list -> state -> state) -> 'a ->
1.81 + ((binding * 'c list) * 'b) list -> ((binding * 'c list) * 'b) list -> bool -> state ->
1.82 + thm list * state *)
1.83 + Proof.have:
1.84 + bool -> Method.text option ->
1.85 + (Proof.context * thm list list -> Proof.state -> Proof.state) ->
1.86 + (binding * typ option * mixfix) list ->
1.87 + (Thm.binding * (term * term list) list) list ->
1.88 + (Thm.binding * (term * term list) list) list ->
1.89 + bool -> Proof.state ->
1.90 + thm list * Proof.state
1.91 \<close> ML \<open>
1.92 \<close>
1.93
1.94 @@ -155,7 +187,42 @@
1.95
1.96 subsection \<open>lookup calls of Syntax.read_props\<close>
1.97 text \<open>
1.98 - TODO
1.99 + focus are "from \<open>0 < d\<close>" and have "0 \<le> c mod d".
1.100 + NO open Syntax_Phases, Syntax in src/Pure
1.101 +
1.102 + callers of Syntax.read_props:
1.103 + Syntax.read_prop
1.104 + Syntax.read_prop_global
1.105 + ML_Thms Theory.setup ML_Antiquotation.declaration
1.106 + Proof_Context.read_propp
1.107 + Expression.read_full_context_statement
1.108 +
1.109 + ??? where else might Syntax.read_props be called ???
1.110 +
1.111 + search top down
1.112 + "from" :: prf_chain % "proof" only def.in Pure.thy: "from" "with"
1.113 + "have" :: prf_goal % "proof" -"- + Proof.have
1.114 + "show" :: prf_asm_goal % "proof" -"- + Proof.show
1.115 +\<close>
1.116 +
1.117 +subsection \<open>TODO: fill gap Syntax.read_props .. Proof.gen_have\<close>
1.118 +text \<open>
1.119 + TODO: fill the gap in the trace between Syntax.read_props .. Proof.gen_have.
1.120 +\<close>
1.121 +
1.122 +subsection \<open>lookup calls of Proof.have.."have"\<close>
1.123 +text \<open>
1.124 + Proof.have
1.125 + Proof.have_cmd
1.126 + Proof.show
1.127 + Proof.show_cmd
1.128 + Obtain.gen_consider
1.129 + Obtain.gen_obtain
1.130 +
1.131 + ??? where else might Proof.have (current hd of trace) be called ???
1.132 + NO "open Proof" in src/Pure
1.133 + !!! there are new trace elements Proof.* (found in other parts of spark_vc procedure_g_c_d_4)
1.134 +
1.135 \<close>
1.136
1.137 subsubsection \<open>TODO\<close>
2.1 --- a/src/Pure/Isar/expression.ML Mon Dec 21 11:55:10 2020 +0100
2.2 +++ b/src/Pure/Isar/expression.ML Mon Dec 21 15:13:49 2020 +0100
2.3 @@ -474,8 +474,10 @@
2.4 Proof_Context.read_var make_inst Syntax.check_props (K I) Proof_Context.cert_var (K I) x);
2.5
2.6 fun read_full_context_statement x =
2.7 +((**)writeln "##### Expression.read_full_context_statement";(**)
2.8 prep_full_context_statement Syntax.parse_typ Syntax.parse_prop Obtain.parse_obtains
2.9 - Proof_Context.read_var parse_inst Syntax.read_props Attrib.check_src Proof_Context.read_var check_expr x;
2.10 + Proof_Context.read_var parse_inst Syntax.read_props Attrib.check_src
2.11 + Proof_Context.read_var check_expr x);
2.12
2.13 (*4*)end;(*4*)
2.14
3.1 --- a/src/Pure/Isar/obtain.ML Mon Dec 21 11:55:10 2020 +0100
3.2 +++ b/src/Pure/Isar/obtain.ML Mon Dec 21 15:13:49 2020 +0100
3.3 @@ -160,6 +160,7 @@
3.4
3.5 fun gen_consider prep_obtains raw_obtains int state =
3.6 let
3.7 +(**)val _ = writeln "###### Obtain.gen_consider";(**)
3.8 val _ = Proof.assert_forward_or_chain state;
3.9 val ctxt = Proof.context_of state;
3.10
3.11 @@ -199,6 +200,7 @@
3.12
3.13 fun gen_obtain prep_stmt prep_att that_binding raw_decls raw_fixes raw_prems raw_concls int state =
3.14 let
3.15 +(**)val _ = writeln "###### Obtain.gen_obtain";(**)
3.16 val _ = Proof.assert_forward_or_chain state;
3.17
3.18 val ((_, thesis), thesis_ctxt) = obtain_thesis (Proof.context_of state);
4.1 --- a/src/Pure/Isar/proof.ML Mon Dec 21 11:55:10 2020 +0100
4.2 +++ b/src/Pure/Isar/proof.ML Mon Dec 21 15:13:49 2020 +0100
4.3 @@ -366,7 +366,7 @@
4.4
4.5 (** pretty_state **)
4.6
4.7 -local
4.8 +(*1*)local(*1*)
4.9
4.10 fun pretty_facts _ _ NONE = []
4.11 | pretty_facts ctxt s (SOME ths) = [Proof_Display.pretty_goal_facts ctxt s ths];
4.12 @@ -375,7 +375,7 @@
4.13 | pretty_sep [] prts = prts
4.14 | pretty_sep prts1 prts2 = prts1 @ [Pretty.str ""] @ prts2;
4.15
4.16 -in
4.17 +(*1*)in(*1*)
4.18
4.19 fun pretty_state state =
4.20 let
4.21 @@ -407,7 +407,7 @@
4.22 else prt_goal (try find_goal state))
4.23 end;
4.24
4.25 -end;
4.26 +(*1*)end;(*1*)
4.27
4.28
4.29
4.30 @@ -415,7 +415,7 @@
4.31
4.32 (* refine via method *)
4.33
4.34 -local
4.35 +(*2*)local(*2*)
4.36
4.37 fun apply_method text ctxt state =
4.38 find_goal state |> (fn (goal_ctxt, {statement, using, goal, before_qed, after_qed}) =>
4.39 @@ -423,7 +423,7 @@
4.40 |> Seq.map_result (fn (goal_ctxt', goal') =>
4.41 state |> map_goal (K (goal_ctxt', statement, using, goal', before_qed, after_qed))));
4.42
4.43 -in
4.44 +(*2*)in(*2*)
4.45
4.46 fun refine text state = apply_method text (context_of state) state;
4.47 fun refine_end text state = apply_method text (#1 (find_goal state)) state;
4.48 @@ -436,12 +436,12 @@
4.49 fun refine_primitive r =
4.50 refine_singleton (Method.Basic (fn ctxt => fn _ => CONTEXT_TACTIC (PRIMITIVE (r ctxt))));
4.51
4.52 -end;
4.53 +(*2*)end;(*2*)
4.54
4.55
4.56 (* refine via sub-proof *)
4.57
4.58 -local
4.59 +(*3*)local(*3*)
4.60
4.61 fun finish_tac _ 0 = K all_tac
4.62 | finish_tac ctxt n =
4.63 @@ -468,7 +468,7 @@
4.64 fun protect_prems th =
4.65 fold_rev protect_prem (1 upto Thm.nprems_of th) th;
4.66
4.67 -in
4.68 +(*3*)in(*3*)
4.69
4.70 fun refine_goals print_rule result_ctxt result state =
4.71 let
4.72 @@ -482,7 +482,7 @@
4.73 |> (fn rules => Seq.lift provide_goal (EVERY (map refine rules) goal) state)
4.74 end;
4.75
4.76 -end;
4.77 +(*3*)end;(*3*)
4.78
4.79
4.80 (* conclude goal *)
4.81 @@ -557,7 +557,7 @@
4.82
4.83 (* let bindings *)
4.84
4.85 -(**)local(**)
4.86 +(*4*)local(*4*)
4.87
4.88 fun gen_bind prep_terms raw_binds =
4.89 assert_forward #> map_context (fn ctxt =>
4.90 @@ -586,7 +586,7 @@
4.91 fun read_terms ctxt T =
4.92 map (Syntax.parse_term ctxt #> Type.constraint T) #> Syntax.check_terms ctxt;
4.93
4.94 -(**)in(**)
4.95 +(*4*)in(*4*)
4.96
4.97 (*val let_bind: (term list * term) list -> state -> state*)
4.98 val let_bind =
4.99 @@ -597,12 +597,12 @@
4.100 ((** )writeln "#### Proof.let_bind_cmd";( **)
4.101 gen_bind read_terms);
4.102
4.103 -(**)end;(**)
4.104 +(*4*)end;(*4*)
4.105
4.106
4.107 (* concrete syntax *)
4.108
4.109 -local
4.110 +(*5*)local(*5*)
4.111
4.112 fun read_arg (c, mx) ctxt =
4.113 (case Proof_Context.read_const {proper = false, strict = false} ctxt c of
4.114 @@ -620,34 +620,34 @@
4.115 #> map_context (fold_map prep_arg args #-> Proof_Context.notation true mode)
4.116 #> reset_facts;
4.117
4.118 -in
4.119 +(*5*)in(*5*)
4.120
4.121 val write = gen_write pair;
4.122 val write_cmd = gen_write read_arg;
4.123
4.124 -end;
4.125 +(*5*)end;(*5*)
4.126
4.127
4.128 (* fix *)
4.129
4.130 -local
4.131 +(*6*)local(*6*)
4.132
4.133 fun gen_fix add_fixes raw_fixes =
4.134 assert_forward
4.135 #> map_context (snd o add_fixes raw_fixes)
4.136 #> reset_facts;
4.137
4.138 -in
4.139 +(*6*)in(*6*)
4.140
4.141 val fix = gen_fix Proof_Context.add_fixes;
4.142 val fix_cmd = gen_fix Proof_Context.add_fixes_cmd;
4.143
4.144 -end;
4.145 +(*6*)end;(*6*)
4.146
4.147
4.148 (* assume *)
4.149
4.150 -local
4.151 +(*7*)local(*7*)
4.152
4.153 fun gen_assume prep_statement prep_att export raw_fixes raw_prems raw_concls state =
4.154 let
4.155 @@ -670,7 +670,7 @@
4.156 |> these_factss [] |> #2
4.157 end;
4.158
4.159 -in
4.160 +(*7*)in(*7*)
4.161
4.162 val assm = gen_assume Proof_Context.cert_statement (K I);
4.163 val assm_cmd = gen_assume Proof_Context.read_statement Attrib.attribute_cmd;
4.164 @@ -681,7 +681,7 @@
4.165 val presume = assm Assumption.presume_export;
4.166 val presume_cmd = assm_cmd Assumption.presume_export;
4.167
4.168 -end;
4.169 +(*7*)end;(*7*)
4.170
4.171
4.172
4.173 @@ -703,7 +703,7 @@
4.174
4.175 fun empty_bindings args = map (pair Binding.empty_atts) args;
4.176
4.177 -local
4.178 +(*8*)local(*8*)
4.179
4.180 fun gen_thmss more_facts opt_chain opt_result prep_atts prep_fact args state =
4.181 state
4.182 @@ -714,7 +714,7 @@
4.183 ||> opt_chain
4.184 |> opt_result;
4.185
4.186 -in
4.187 +(*8*)in(*8*)
4.188
4.189 val note_thmss = gen_thmss (K []) I #2 (K I) (K I);
4.190 val note_thmss_cmd = gen_thmss (K []) I #2 Attrib.attribute_cmd Proof_Context.get_fact;
4.191 @@ -729,12 +729,12 @@
4.192
4.193 val local_results = gen_thmss (K []) I I (K I) (K I) o map (apsnd Thm.simple_fact);
4.194
4.195 -end;
4.196 +(*8*)end;(*8*)
4.197
4.198
4.199 (* facts during goal refinement *)
4.200
4.201 -local
4.202 +(*9*)local(*9*)
4.203
4.204 fun gen_supply prep_att prep_fact args state =
4.205 state
4.206 @@ -742,17 +742,17 @@
4.207 |> map_context (fn ctxt => ctxt |> Proof_Context.note_thmss ""
4.208 (Attrib.map_facts_refs (map (prep_att ctxt)) (prep_fact ctxt) args) |> snd);
4.209
4.210 -in
4.211 +(*9*)in(*9*)
4.212
4.213 val supply = gen_supply (K I) (K I);
4.214 val supply_cmd = gen_supply Attrib.attribute_cmd Proof_Context.get_fact;
4.215
4.216 -end;
4.217 +(*9*)end;(*9*)
4.218
4.219
4.220 (* using/unfolding *)
4.221
4.222 -local
4.223 +(*10*)local(*10*)
4.224
4.225 fun gen_using f g prep_att prep_fact args state =
4.226 state
4.227 @@ -771,19 +771,19 @@
4.228 fun unfold_using ctxt ths = map (Local_Defs.unfold ctxt ths);
4.229 val unfold_goals = Local_Defs.unfold_goals;
4.230
4.231 -in
4.232 +(*10*)in(*10*)
4.233
4.234 val using = gen_using append_using (K (K I)) (K I) (K I);
4.235 val using_cmd = gen_using append_using (K (K I)) Attrib.attribute_cmd Proof_Context.get_fact;
4.236 val unfolding = gen_using unfold_using unfold_goals (K I) (K I);
4.237 val unfolding_cmd = gen_using unfold_using unfold_goals Attrib.attribute_cmd Proof_Context.get_fact;
4.238
4.239 -end;
4.240 +(*10*)end;(*10*)
4.241
4.242
4.243 (* case *)
4.244
4.245 -local
4.246 +(*11*)local(*11*)
4.247
4.248 fun gen_case internal prep_att ((raw_binding, raw_atts), ((name, pos), xs)) state =
4.249 let
4.250 @@ -803,17 +803,17 @@
4.251 |> `the_facts |-> (fn thms => note_thmss [((binding, atts), [(thms, [])])])
4.252 end;
4.253
4.254 -in
4.255 +(*11*)in(*11*)
4.256
4.257 val case_ = gen_case true (K I);
4.258 val case_cmd = gen_case false Attrib.attribute_cmd;
4.259
4.260 -end;
4.261 +(*11*)end;(*11*)
4.262
4.263
4.264 (* define *)
4.265
4.266 -local
4.267 +(*12*)local(*12*)
4.268
4.269 fun gen_define prep_stmt prep_att raw_decls raw_fixes raw_defs state =
4.270 let
4.271 @@ -859,12 +859,12 @@
4.272 |> note_thmss notes
4.273 end;
4.274
4.275 -in
4.276 +(*12*)in(*12*)
4.277
4.278 val define = gen_define Proof_Context.cert_stmt (K I);
4.279 val define_cmd = gen_define Proof_Context.read_stmt Attrib.attribute_cmd;
4.280
4.281 -end;
4.282 +(*12*)end;(*12*)
4.283
4.284
4.285
4.286 @@ -988,7 +988,7 @@
4.287
4.288 (* generic goals *)
4.289
4.290 -local
4.291 +(*13*)local(*13*)
4.292
4.293 val is_var =
4.294 can (dest_TVar o Logic.dest_type o Logic.dest_term) orf
4.295 @@ -1006,7 +1006,7 @@
4.296 K (HEADGOAL (PRECISE_CONJUNCTS n
4.297 (HEADGOAL (CONJUNCTS (ALLGOALS (resolve_tac ctxt [Drule.termI]))))))));
4.298
4.299 -in
4.300 +(*13*)in(*13*)
4.301
4.302 fun generic_goal kind before_qed after_qed goal_ctxt goal_propss result_binds state =
4.303 let
4.304 @@ -1051,7 +1051,7 @@
4.305 val results = tl (conclude_goal goal_ctxt goal propss);
4.306 in state |> close_block |> pair (after_qed, (goal_ctxt, results)) end;
4.307
4.308 -end;
4.309 +(*13*)end;(*13*)
4.310
4.311
4.312 (* local goals *)
4.313 @@ -1164,7 +1164,7 @@
4.314
4.315 (* terminal proof steps *)
4.316
4.317 -local
4.318 +(*14*)local(*14*)
4.319
4.320 fun terminal_proof qeds initial terminal state =
4.321 let
4.322 @@ -1183,7 +1183,7 @@
4.323 |> Seq.maps_results (qeds (#2 (#2 initial), terminal'))
4.324 end |> Seq.the_result "";
4.325
4.326 -in
4.327 +(*14*)in(*14*)
4.328
4.329 fun local_terminal_proof (text, opt_text) = terminal_proof local_qeds text (opt_text, true);
4.330 val local_default_proof = local_terminal_proof ((Method.standard_text, Position.no_range), NONE);
4.331 @@ -1195,7 +1195,7 @@
4.332 val global_immediate_proof = global_terminal_proof ((Method.this_text, Position.no_range), NONE);
4.333 val global_done_proof = terminal_proof global_qeds (Method.done_text, Position.no_range) (NONE, false);
4.334
4.335 -end;
4.336 +(*14*)end;(*14*)
4.337
4.338
4.339 (* skip proofs *)
4.340 @@ -1215,14 +1215,16 @@
4.341 local_goal print_results
4.342 (fn a => fn b => fn c => Proof_Context.cert_statement a b c o Proof_Context.set_mode mode) (K I);
4.343
4.344 -local
4.345 +(*15*)local(*15*)
4.346
4.347 fun gen_have prep_statement prep_att strict_asm before_qed after_qed fixes assumes shows int =
4.348 +((**)writeln "####-# Proof.gen_have";(**)
4.349 local_goal (Proof_Display.print_results int (Position.thread_data ()))
4.350 - prep_statement prep_att strict_asm "have" before_qed after_qed fixes assumes shows;
4.351 + prep_statement prep_att strict_asm "have" before_qed after_qed fixes assumes shows);
4.352
4.353 fun gen_show prep_statement prep_att strict_asm before_qed after_qed fixes assumes shows int state =
4.354 let
4.355 + val _ = (**)writeln "###### Proof.gen_show";(**)
4.356 val testing = Unsynchronized.ref false;
4.357 val rule = Unsynchronized.ref (NONE: thm option);
4.358 fun fail_msg ctxt =
4.359 @@ -1260,14 +1262,22 @@
4.360 | Exn.Exn exn => raise Exn.EXCEPTIONS ([exn, ERROR (fail_msg (context_of goal_state))])))
4.361 end;
4.362
4.363 -in
4.364 +(*15*)in(*15*)
4.365
4.366 -val have = gen_have Proof_Context.cert_statement (K I);
4.367 -val have_cmd = gen_have Proof_Context.read_statement Attrib.attribute_cmd;
4.368 -val show = gen_show Proof_Context.cert_statement (K I);
4.369 -val show_cmd = gen_show Proof_Context.read_statement Attrib.attribute_cmd;
4.370 +val have =
4.371 + ((**)writeln "###### Proof.have";(**)
4.372 + gen_have Proof_Context.cert_statement (K I));
4.373 +val have_cmd =
4.374 + ((**)writeln "###### Proof.have_cmd";(**)
4.375 + gen_have Proof_Context.read_statement Attrib.attribute_cmd);
4.376 +val show =
4.377 + ((**)writeln "###### Proof.show";(**)
4.378 + gen_show Proof_Context.cert_statement (K I));
4.379 +val show_cmd =
4.380 + ((**)writeln "###### Proof.show_cmd";(**)
4.381 + gen_show Proof_Context.read_statement Attrib.attribute_cmd);
4.382
4.383 -end;
4.384 +(*15*)end;(*15*)
4.385
4.386
4.387
4.388 @@ -1275,7 +1285,7 @@
4.389
4.390 (* full proofs *)
4.391
4.392 -local
4.393 +(*16*)local(*16*)
4.394
4.395 structure Result = Proof_Data
4.396 (
4.397 @@ -1291,7 +1301,7 @@
4.398 val set_result = Result.put o SOME;
4.399 val reset_result = Result.put NONE;
4.400
4.401 -in
4.402 +(*16*)in(*16*)
4.403
4.404 fun future_proof fork_proof state =
4.405 let
4.406 @@ -1317,12 +1327,12 @@
4.407 |> map_goal (K (goal_ctxt, statement, using, finished_goal, NONE, after_qed));
4.408 in (Future.map fst result_ctxt, state') end;
4.409
4.410 -end;
4.411 +(*16*)end;(*16*)
4.412
4.413
4.414 (* terminal proofs *) (* FIXME avoid toplevel imitation -- include in PIDE/document *)
4.415
4.416 -local
4.417 +(*17*)local(*17*)
4.418
4.419 fun future_terminal_proof proof1 proof2 done state =
4.420 if Future.proofs_enabled 3 andalso
4.421 @@ -1336,7 +1346,7 @@
4.422 end) |> snd |> done
4.423 else proof1 state;
4.424
4.425 -in
4.426 +(*17*)in(*17*)
4.427
4.428 fun local_future_terminal_proof meths =
4.429 future_terminal_proof
4.430 @@ -1348,6 +1358,6 @@
4.431 (global_terminal_proof meths)
4.432 (global_terminal_proof meths) global_done_proof;
4.433
4.434 -end;
4.435 +(*17*)end;(*17*)
4.436
4.437 end;
5.1 --- a/src/Pure/Isar/proof_context.ML Mon Dec 21 11:55:10 2020 +0100
5.2 +++ b/src/Pure/Isar/proof_context.ML Mon Dec 21 15:13:49 2020 +0100
5.3 @@ -904,7 +904,7 @@
5.4 in
5.5
5.6 val cert_propp = prep_propp (map o cert_prop);
5.7 -val read_propp = prep_propp Syntax.read_props;
5.8 +val read_propp = ((**)writeln "##### Proof_Context.read_propp";(**) prep_propp Syntax.read_props);
5.9
5.10 end;
5.11
6.1 --- a/src/Pure/ML/ml_thms.ML Mon Dec 21 11:55:10 2020 +0100
6.2 +++ b/src/Pure/ML/ml_thms.ML Mon Dec 21 15:13:49 2020 +0100
6.3 @@ -85,11 +85,13 @@
6.4 (Parse.position by -- Method.parse -- Scan.option Method.parse)))
6.5 (fn _ => fn ((is_open, raw_propss), (((_, by_pos), m1), m2)) => fn ctxt =>
6.6 let
6.7 + val _ = (**)writeln "##### ML_Thms Theory.setup 1 thm_binding lemma";(**)
6.8 val reports =
6.9 (by_pos, Markup.keyword1 |> Markup.keyword_properties) ::
6.10 maps Method.reports_of (m1 :: the_list m2);
6.11 val _ = Context_Position.reports ctxt reports;
6.12
6.13 + val _ = (**)writeln "##### ML_Thms Theory.setup 2 thm_binding lemma";(**)
6.14 val propss = burrow (map (rpair []) o Syntax.read_props ctxt) raw_propss;
6.15 val prep_result = Goal.norm_result ctxt #> not is_open ? Thm.close_derivation \<^here>;
6.16 fun after_qed res goal_ctxt =
7.1 --- a/src/Pure/Syntax/syntax.ML Mon Dec 21 11:55:10 2020 +0100
7.2 +++ b/src/Pure/Syntax/syntax.ML Mon Dec 21 15:13:49 2020 +0100
7.3 @@ -308,14 +308,14 @@
7.4 val read_typ = singleton o read_typs;
7.5 val read_term = singleton o read_terms;
7.6 val read_prop =
7.7 -((** )writeln "##### Syntax.read_prop";( **)
7.8 +((**)writeln "##### Syntax.read_prop";(**)
7.9 singleton o read_props);
7.10
7.11 val read_sort_global = read_sort o Proof_Context.init_global;
7.12 val read_typ_global = read_typ o Proof_Context.init_global;
7.13 val read_term_global = read_term o Proof_Context.init_global;
7.14 val read_prop_global =
7.15 -((** )writeln "##### Syntax.read_prop_global";( **)
7.16 +((**)writeln "##### Syntax.read_prop_global";(**)
7.17 read_prop o Proof_Context.init_global);
7.18
7.19
8.1 --- a/src/Pure/Syntax/syntax_phases.ML Mon Dec 21 11:55:10 2020 +0100
8.2 +++ b/src/Pure/Syntax/syntax_phases.ML Mon Dec 21 15:13:49 2020 +0100
8.3 @@ -993,7 +993,7 @@
8.4
8.5 val _ =
8.6 if Context_Position.is_visible ctxt
8.7 - then ((*2*)writeln "### calling Output.report";(**)
8.8 + then ((*2*)writeln "## calling Output.report";(**)
8.9 Output.report (sorting_report @ typing_report)) else ();
8.10 in Term_Sharing.terms (Proof_Context.theory_of ctxt) ts' end;
8.11