418 (*filters return: (number of assumptions, substitution size) option, so |
418 (*filters return: (number of assumptions, substitution size) option, so |
419 sort (desc. in both cases) according to number of assumptions first, |
419 sort (desc. in both cases) according to number of assumptions first, |
420 then by the substitution size*) |
420 then by the substitution size*) |
421 fun result_ord (((p0, s0), _), ((p1, s1), _)) = |
421 fun result_ord (((p0, s0), _), ((p1, s1), _)) = |
422 prod_ord int_ord int_ord ((p1, s1), (p0, s0)); |
422 prod_ord int_ord int_ord ((p1, s1), (p0, s0)); |
423 in map_filter eval_filters theorems |> sort result_ord |> map #2 end; |
423 in |
|
424 grouped 100 Par_List.map eval_filters theorems |
|
425 |> map_filter I |> sort result_ord |> map #2 |
|
426 end; |
424 |
427 |
425 fun lazy_filter filters = |
428 fun lazy_filter filters = |
426 let |
429 let |
427 fun lazy_match thms = Seq.make (fn () => first_match thms) |
430 fun lazy_match thms = Seq.make (fn () => first_match thms) |
428 and first_match [] = NONE |
431 and first_match [] = NONE |
579 Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria) :: |
582 Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria) :: |
580 Pretty.str "" :: |
583 Pretty.str "" :: |
581 (if null theorems then [Pretty.str "nothing found"] |
584 (if null theorems then [Pretty.str "nothing found"] |
582 else |
585 else |
583 [Pretty.str (tally_msg ^ ":"), Pretty.str ""] @ |
586 [Pretty.str (tally_msg ^ ":"), Pretty.str ""] @ |
584 map (pretty_theorem ctxt) theorems) |
587 grouped 10 Par_List.map (pretty_theorem ctxt) theorems) |
585 end |> Pretty.chunks |> Pretty.writeln; |
588 end |> Pretty.chunks |> Pretty.writeln; |
586 |
589 |
587 fun print_theorems ctxt = |
590 fun print_theorems ctxt = |
588 gen_print_theorems (filter_theorems ctxt (map Internal (all_facts_of ctxt))) ctxt; |
591 gen_print_theorems (filter_theorems ctxt (map Internal (all_facts_of ctxt))) ctxt; |
589 |
592 |