1.1 --- a/doc-src/antiquote_setup.ML	Mon Oct 20 23:53:17 2008 +0200
     1.2 +++ b/doc-src/antiquote_setup.ML	Tue Oct 21 15:01:16 2008 +0200
     1.3 @@ -30,16 +30,6 @@
     1.4    | clean_name "}" = "braceright"
     1.5    | clean_name s = s |> translate_string (fn "_" => "-" | c => c);
     1.6  
     1.7 -val str_of_source = space_implode " " o map OuterLex.unparse o #2 o #1 o Args.dest_src;
     1.8 -
     1.9 -fun tweak_line s =
    1.10 -  if ! O.display then s else Symbol.strip_blanks s;
    1.11 -
    1.12 -val pretty_text = Pretty.chunks o map Pretty.str o map tweak_line o Library.split_lines;
    1.13 -
    1.14 -fun pretty_term ctxt t = Syntax.pretty_term (Variable.auto_fixes t ctxt) t;
    1.15 -fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of;
    1.16 -
    1.17  
    1.18  (* verbatim text *)
    1.19  
    1.20 @@ -78,7 +68,7 @@
    1.21      val _ = ML_Context.eval_in (SOME ctxt) false Position.none (ml (txt1, txt2));
    1.22    in
    1.23      "\\indexml" ^ kind ^ enclose "{" "}" (clean_string txt1) ^
    1.24 -    ((if ! O.source then str_of_source src else txt')
    1.25 +    ((if ! O.source then ThyOutput.str_of_source src else txt')
    1.26      |> (if ! O.quotes then quote else I)
    1.27      |> (if ! O.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
    1.28          else split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"))
    1.29 @@ -112,18 +102,18 @@
    1.30  local
    1.31  
    1.32  fun output_named_thms src ctxt xs =
    1.33 -  map (apfst (pretty_thm ctxt)) xs        (*always pretty in order to exhibit errors!*)
    1.34 +  map (apfst (ThyOutput.pretty_thm ctxt)) xs        (*always pretty in order to exhibit errors!*)
    1.35    |> (if ! O.quotes then map (apfst Pretty.quote) else I)
    1.36    |> (if ! O.display then
    1.37      map (fn (p, name) =>
    1.38        Output.output (Pretty.string_of (Pretty.indent (! O.indent) p)) ^
    1.39 -      "\\rulename{" ^ Output.output (Pretty.str_of (pretty_text name)) ^ "}")
    1.40 +      "\\rulename{" ^ Output.output (Pretty.str_of (ThyOutput.pretty_text name)) ^ "}")
    1.41      #> space_implode "\\par\\smallskip%\n"
    1.42      #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
    1.43    else
    1.44      map (fn (p, name) =>
    1.45        Output.output (Pretty.str_of p) ^
    1.46 -      "\\rulename{" ^ Output.output (Pretty.str_of (pretty_text name)) ^ "}")
    1.47 +      "\\rulename{" ^ Output.output (Pretty.str_of (ThyOutput.pretty_text name)) ^ "}")
    1.48      #> space_implode "\\par\\smallskip%\n"
    1.49      #> enclose "\\isa{" "}");
    1.50