123 val print_lthms: context -> unit |
123 val print_lthms: context -> unit |
124 val print_cases: context -> unit |
124 val print_cases: context -> unit |
125 val prems_limit: int ref |
125 val prems_limit: int ref |
126 val pretty_asms: context -> Pretty.T list |
126 val pretty_asms: context -> Pretty.T list |
127 val pretty_context: context -> Pretty.T list |
127 val pretty_context: context -> Pretty.T list |
128 val print_thms_containing: context -> string list -> unit |
128 val thms_containing_limit: int ref |
|
129 val print_thms_containing: context -> int option -> string list -> unit |
129 val setup: (theory -> theory) list |
130 val setup: (theory -> theory) list |
130 end; |
131 end; |
131 |
132 |
132 signature PRIVATE_PROOF_CONTEXT = |
133 signature PRIVATE_PROOF_CONTEXT = |
133 sig |
134 sig |
1376 None => false |
1377 None => false |
1377 | Some ths' => Library.equal_lists Thm.eq_thm (ths, ths')); |
1378 | Some ths' => Library.equal_lists Thm.eq_thm (ths, ths')); |
1378 in gen_distinct eq_fst (filter valid (FactIndex.find idx index)) end; |
1379 in gen_distinct eq_fst (filter valid (FactIndex.find idx index)) end; |
1379 |
1380 |
1380 |
1381 |
1381 fun print_thms_containing ctxt ss = |
1382 val thms_containing_limit = ref 40; |
|
1383 |
|
1384 fun print_thms_containing ctxt opt_limit ss = |
1382 let |
1385 let |
1383 val prt_term = pretty_term ctxt; |
1386 val prt_term = pretty_term ctxt; |
1384 val prt_fact = pretty_fact ctxt; |
1387 val prt_fact = pretty_fact ctxt; |
1385 fun prt_consts [] = [] |
1388 fun prt_consts [] = [] |
1386 | prt_consts cs = [Pretty.block (Pretty.breaks (Pretty.str "constants" :: |
1389 | prt_consts cs = [Pretty.block (Pretty.breaks (Pretty.str "constants" :: |
1396 val header = |
1399 val header = |
1397 if empty_idx then [Pretty.block [Pretty.str "All known facts:", Pretty.fbrk]] |
1400 if empty_idx then [Pretty.block [Pretty.str "All known facts:", Pretty.fbrk]] |
1398 else [Pretty.block (Pretty.breaks (Pretty.str "Facts containing" :: |
1401 else [Pretty.block (Pretty.breaks (Pretty.str "Facts containing" :: |
1399 separate (Pretty.str "and") (prt_consts cs @ prt_frees xs)) @ |
1402 separate (Pretty.str "and") (prt_consts cs @ prt_frees xs)) @ |
1400 [Pretty.str ":", Pretty.fbrk])] |
1403 [Pretty.str ":", Pretty.fbrk])] |
1401 val globals = PureThy.thms_containing (theory_of ctxt) (cs, xs); |
1404 val facts = |
1402 val locals = lthms_containing ctxt (cs, xs); |
1405 PureThy.thms_containing (theory_of ctxt) (cs, xs) @ lthms_containing ctxt (cs, xs) |
|
1406 |> sort_wrt #1; |
|
1407 val len = length facts; |
|
1408 val limit = if_none opt_limit (! thms_containing_limit); |
1403 in |
1409 in |
1404 if empty_idx andalso not (Library.null ss) then |
1410 if empty_idx andalso not (Library.null ss) then |
1405 warning "thms_containing: no consts/frees in specification" |
1411 warning "thms_containing: no consts/frees in specification" |
1406 else (header @ map prt_fact (sort_wrt #1 (globals @ locals))) |
1412 else (header @ (if len <= limit then [] else [Pretty.str "..."]) @ |
1407 |> Pretty.chunks |> Pretty.writeln |
1413 map prt_fact (Library.drop (len - limit, facts))) |> Pretty.chunks |> Pretty.writeln |
1408 end; |
1414 end; |
1409 |
1415 |
1410 |
1416 |
1411 |
1417 |
1412 (** theory setup **) |
1418 (** theory setup **) |