equal
deleted
inserted
replaced
168 |
168 |
169 fun pretty_src ctxt src = |
169 fun pretty_src ctxt src = |
170 let |
170 let |
171 val prt_thm = Pretty.backquote o ProofContext.pretty_thm ctxt; |
171 val prt_thm = Pretty.backquote o ProofContext.pretty_thm ctxt; |
172 fun prt (Arg (_, Value (SOME (Text s)))) = Pretty.str (quote s) |
172 fun prt (Arg (_, Value (SOME (Text s)))) = Pretty.str (quote s) |
173 | prt (Arg (_, Value (SOME (Typ T)))) = ProofContext.pretty_typ ctxt T |
173 | prt (Arg (_, Value (SOME (Typ T)))) = Syntax.pretty_typ ctxt T |
174 | prt (Arg (_, Value (SOME (Term t)))) = ProofContext.pretty_term ctxt t |
174 | prt (Arg (_, Value (SOME (Term t)))) = Syntax.pretty_term ctxt t |
175 | prt (Arg (_, Value (SOME (Fact ths)))) = |
175 | prt (Arg (_, Value (SOME (Fact ths)))) = |
176 Pretty.enclose "(" ")" (Pretty.breaks (map prt_thm ths)) |
176 Pretty.enclose "(" ")" (Pretty.breaks (map prt_thm ths)) |
177 | prt arg = Pretty.str (string_of arg); |
177 | prt arg = Pretty.str (string_of arg); |
178 val (s, args) = #1 (dest_src src); |
178 val (s, args) = #1 (dest_src src); |
179 in Pretty.block (Pretty.breaks (Pretty.str s :: map prt args)) end; |
179 in Pretty.block (Pretty.breaks (Pretty.str s :: map prt args)) end; |