ThyOutput: export some auxiliary operations;
authorwenzelm
Tue Oct 21 15:01:16 2008 +0200 (2008-10-21)
changeset 28644e2ae4a6cf166
parent 28643 caa1137d25dc
child 28645 605a3b1ef6ba
ThyOutput: export some auxiliary operations;
doc-src/antiquote_setup.ML
src/Pure/Thy/thy_output.ML
     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  
     2.1 --- a/src/Pure/Thy/thy_output.ML	Mon Oct 20 23:53:17 2008 +0200
     2.2 +++ b/src/Pure/Thy/thy_output.ML	Tue Oct 21 15:01:16 2008 +0200
     2.3 @@ -25,6 +25,10 @@
     2.4    val eval_antiquote: Scan.lexicon -> Toplevel.node option -> SymbolPos.text * Position.T -> string
     2.5    val present_thy: Scan.lexicon -> (string -> string list) -> (markup -> string -> bool) ->
     2.6      (Toplevel.transition * Toplevel.state) list -> (OuterLex.token, 'a) Source.source -> Buffer.T
     2.7 +  val str_of_source: Args.src -> string
     2.8 +  val pretty_text: string -> Pretty.T
     2.9 +  val pretty_term: Proof.context -> term -> Pretty.T
    2.10 +  val pretty_thm: Proof.context -> thm -> Pretty.T
    2.11    val output_list: (Proof.context -> 'a -> Pretty.T) -> Args.src ->
    2.12      Proof.context -> 'a list -> string
    2.13    val output: (Proof.context -> 'a -> Pretty.T) -> Args.src -> Proof.context -> 'a -> string