Exported output_with.
--- a/src/Pure/Isar/isar_output.ML Wed Oct 10 18:37:52 2001 +0200
+++ b/src/Pure/Isar/isar_output.ML Wed Oct 10 18:38:21 2001 +0200
@@ -25,6 +25,8 @@
val quotes: bool ref
val indent: int ref
val source: bool ref
+ val output_with: (Proof.context -> 'a -> Pretty.T) -> Args.src ->
+ Proof.context -> 'a -> string
end;
structure IsarOutput: ISAR_OUTPUT =
@@ -269,8 +271,6 @@
(* commands *)
-local
-
fun cond_quote prt =
if ! quotes then Pretty.quote prt else prt;
@@ -312,8 +312,6 @@
Pretty.chunks (Proof.pretty_goals main_goal (Toplevel.proof_of state
handle Toplevel.UNDEF => error "No proof state")))) src state;
-in
-
val _ = add_commands
[("text", args (Scan.lift Args.name) (output_with (K pretty_text))),
("thm", args Attrib.local_thmss (output_with pretty_thm)),
@@ -326,5 +324,3 @@
("subgoals", output_goals false)];
end;
-
-end;