equal
deleted
inserted
replaced
1098 val verbose = ref false; |
1098 val verbose = ref false; |
1099 fun verb f x = if ! verbose then f (x ()) else []; |
1099 fun verb f x = if ! verbose then f (x ()) else []; |
1100 |
1100 |
1101 fun setmp_verbose f x = Library.setmp verbose true f x; |
1101 fun setmp_verbose f x = Library.setmp verbose true f x; |
1102 |
1102 |
1103 fun pretty_items prt name items = |
|
1104 let |
|
1105 fun prt_itms (name, [x]) = Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 1, prt x] |
|
1106 | prt_itms (name, xs) = Pretty.big_list (name ^ ":") (map prt xs); |
|
1107 in |
|
1108 if null items andalso not (! verbose) then [] |
|
1109 else [Pretty.big_list name (map prt_itms items)] |
|
1110 end; |
|
1111 |
|
1112 |
1103 |
1113 (* local syntax *) |
1104 (* local syntax *) |
1114 |
1105 |
1115 val print_syntax = Syntax.print_syntax o syn_of; |
1106 val print_syntax = Syntax.print_syntax o syn_of; |
1116 |
1107 |
1146 |
1137 |
1147 |
1138 |
1148 (* local theorems *) |
1139 (* local theorems *) |
1149 |
1140 |
1150 fun pretty_lthms ctxt = |
1141 fun pretty_lthms ctxt = |
1151 pretty_items (pretty_thm ctxt) "facts:" (NameSpace.extern_table (#1 (thms_of ctxt))); |
1142 let |
|
1143 val props = FactIndex.props (fact_index_of ctxt); |
|
1144 val facts = |
|
1145 (if null props then I else cons ("unnamed", props)) |
|
1146 (NameSpace.extern_table (#1 (thms_of ctxt))); |
|
1147 in |
|
1148 if null facts andalso not (! verbose) then [] |
|
1149 else [Pretty.big_list "facts:" (map (pretty_fact ctxt) facts)] |
|
1150 end; |
1152 |
1151 |
1153 val print_lthms = Pretty.writeln o Pretty.chunks o pretty_lthms; |
1152 val print_lthms = Pretty.writeln o Pretty.chunks o pretty_lthms; |
1154 |
1153 |
1155 |
1154 |
1156 (* local contexts *) |
1155 (* local contexts *) |