308 ("margin", Pretty.setmp_margin o integer), |
308 ("margin", Pretty.setmp_margin o integer), |
309 ("indent", Library.setmp indent o integer), |
309 ("indent", Library.setmp indent o integer), |
310 ("source", Library.setmp source o boolean), |
310 ("source", Library.setmp source o boolean), |
311 ("goals_limit", Library.setmp goals_limit o integer)]; |
311 ("goals_limit", Library.setmp goals_limit o integer)]; |
312 |
312 |
|
313 |
313 (* commands *) |
314 (* commands *) |
314 |
315 |
315 fun cond_quote prt = |
316 fun cond_quote prt = |
316 if ! quotes then Pretty.quote prt else prt; |
317 if ! quotes then Pretty.quote prt else prt; |
317 |
318 |
343 val pretty_source = |
344 val pretty_source = |
344 pretty_text o space_implode " " o map Args.string_of o #2 o #1 o Args.dest_src; |
345 pretty_text o space_implode " " o map Args.string_of o #2 o #1 o Args.dest_src; |
345 |
346 |
346 fun pretty_term ctxt = ProofContext.pretty_term ctxt o ProofContext.extern_skolem ctxt; |
347 fun pretty_term ctxt = ProofContext.pretty_term ctxt o ProofContext.extern_skolem ctxt; |
347 |
348 |
348 fun pretty_term_typ_old ctxt term = Pretty.block [ |
349 fun pretty_term_typ ctxt t = |
349 ((ProofContext.pretty_term ctxt o ProofContext.extern_skolem ctxt) term), |
350 (Syntax.const Syntax.constrainC $ |
350 (Pretty.str "\\<Colon>") (* q'n'd *), |
351 ProofContext.extern_skolem ctxt t $ |
351 ((ProofContext.pretty_typ ctxt o Term.type_of o ProofContext.extern_skolem ctxt) term) |
352 Syntax.term_of_typ (! show_sorts) (Term.fastype_of t)) |
352 ] |
353 |> ProofContext.pretty_term ctxt; |
353 |
354 |
354 fun pretty_term_typ ctxt term = let val t = (ProofContext.extern_skolem ctxt term) in |
355 fun pretty_term_typeof ctxt = ProofContext.pretty_typ ctxt o Term.fastype_of; |
355 ProofContext.pretty_term ctxt ( |
356 |
356 Syntax.const Syntax.constrainC $ t $ Syntax.term_of_typ (!show_sorts) (fastype_of t) |
357 fun pretty_term_const ctxt t = |
357 ) |
358 if Term.is_Const t then pretty_term ctxt t |
358 end; |
359 else error ("Logical constant expected: " ^ ProofContext.string_of_term ctxt t); |
359 |
|
360 fun pretty_term_typeof ctxt = ProofContext.pretty_typ ctxt o Term.fastype_of o ProofContext.extern_skolem ctxt; |
|
361 |
|
362 fun pretty_term_const ctxt (Const c) = pretty_term ctxt (Const c) |
|
363 | pretty_term_const ctxt term = |
|
364 raise (Output.ERROR_MESSAGE ("Not a defined constant: " ^ (Term.string_of_term term))) |
|
365 |
360 |
366 fun pretty_thm ctxt = pretty_term ctxt o Thm.prop_of; |
361 fun pretty_thm ctxt = pretty_term ctxt o Thm.prop_of; |
367 |
362 |
368 fun pretty_term_style ctxt (name, term) = |
363 fun pretty_term_style ctxt (name, term) = |
369 let |
364 let |