# HG changeset patch
# User wenzelm
# Date 1224594076 -7200
# Node ID e2ae4a6cf1664adeda4898c07382e9fc0bcf27d1
# Parent  caa1137d25dca829a87049fdb4d3f6171aad5173
ThyOutput: export some auxiliary operations;

diff -r caa1137d25dc -r e2ae4a6cf166 doc-src/antiquote_setup.ML
--- a/doc-src/antiquote_setup.ML	Mon Oct 20 23:53:17 2008 +0200
+++ b/doc-src/antiquote_setup.ML	Tue Oct 21 15:01:16 2008 +0200
@@ -30,16 +30,6 @@
   | clean_name "}" = "braceright"
   | clean_name s = s |> translate_string (fn "_" => "-" | c => c);
 
-val str_of_source = space_implode " " o map OuterLex.unparse o #2 o #1 o Args.dest_src;
-
-fun tweak_line s =
-  if ! O.display then s else Symbol.strip_blanks s;
-
-val pretty_text = Pretty.chunks o map Pretty.str o map tweak_line o Library.split_lines;
-
-fun pretty_term ctxt t = Syntax.pretty_term (Variable.auto_fixes t ctxt) t;
-fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of;
-
 
 (* verbatim text *)
 
@@ -78,7 +68,7 @@
     val _ = ML_Context.eval_in (SOME ctxt) false Position.none (ml (txt1, txt2));
   in
     "\\indexml" ^ kind ^ enclose "{" "}" (clean_string txt1) ^
-    ((if ! O.source then str_of_source src else txt')
+    ((if ! O.source then ThyOutput.str_of_source src else txt')
     |> (if ! O.quotes then quote else I)
     |> (if ! O.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
         else split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"))
@@ -112,18 +102,18 @@
 local
 
 fun output_named_thms src ctxt xs =
-  map (apfst (pretty_thm ctxt)) xs        (*always pretty in order to exhibit errors!*)
+  map (apfst (ThyOutput.pretty_thm ctxt)) xs        (*always pretty in order to exhibit errors!*)
   |> (if ! O.quotes then map (apfst Pretty.quote) else I)
   |> (if ! O.display then
     map (fn (p, name) =>
       Output.output (Pretty.string_of (Pretty.indent (! O.indent) p)) ^
-      "\\rulename{" ^ Output.output (Pretty.str_of (pretty_text name)) ^ "}")
+      "\\rulename{" ^ Output.output (Pretty.str_of (ThyOutput.pretty_text name)) ^ "}")
     #> space_implode "\\par\\smallskip%\n"
     #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
   else
     map (fn (p, name) =>
       Output.output (Pretty.str_of p) ^
-      "\\rulename{" ^ Output.output (Pretty.str_of (pretty_text name)) ^ "}")
+      "\\rulename{" ^ Output.output (Pretty.str_of (ThyOutput.pretty_text name)) ^ "}")
     #> space_implode "\\par\\smallskip%\n"
     #> enclose "\\isa{" "}");
 
diff -r caa1137d25dc -r e2ae4a6cf166 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Mon Oct 20 23:53:17 2008 +0200
+++ b/src/Pure/Thy/thy_output.ML	Tue Oct 21 15:01:16 2008 +0200
@@ -25,6 +25,10 @@
   val eval_antiquote: Scan.lexicon -> Toplevel.node option -> SymbolPos.text * Position.T -> string
   val present_thy: Scan.lexicon -> (string -> string list) -> (markup -> string -> bool) ->
     (Toplevel.transition * Toplevel.state) list -> (OuterLex.token, 'a) Source.source -> Buffer.T
+  val str_of_source: Args.src -> string
+  val pretty_text: string -> Pretty.T
+  val pretty_term: Proof.context -> term -> Pretty.T
+  val pretty_thm: Proof.context -> thm -> Pretty.T
   val output_list: (Proof.context -> 'a -> Pretty.T) -> Args.src ->
     Proof.context -> 'a list -> string
   val output: (Proof.context -> 'a -> Pretty.T) -> Args.src -> Proof.context -> 'a -> string