--- a/NEWS Tue Nov 24 23:17:03 2015 +0100
+++ b/NEWS Wed Nov 25 15:58:22 2015 +0100
@@ -92,7 +92,9 @@
* Antiquotation @{theory_text} prints uninterpreted theory source text
(outer syntax with command keywords etc.). This may be used in the short
-form \<^theory_text>\<open>...\<close>.
+form \<^theory_text>\<open>...\<close>. @{theory_text [display]} supports option "indent".
+
+* @{verbatim [display]} supports option "indent".
* Antiquotation @{doc ENTRY} provides a reference to the given
documentation, with a hyperlink in the Prover IDE.
--- a/src/Pure/Thy/document_antiquotations.ML Tue Nov 24 23:17:03 2015 +0100
+++ b/src/Pure/Thy/document_antiquotations.ML Wed Nov 25 15:58:22 2015 +0100
@@ -76,10 +76,13 @@
|> Token.source' true keywords
|> Source.exhaust;
val _ = Context_Position.reports_text ctxt (maps (Token.reports keywords) toks);
+ val indentation =
+ Latex.output_symbols (replicate (Config.get ctxt Thy_Output.indent) Symbol.space);
in
implode (map Latex.output_token toks) |>
- (if Config.get ctxt Thy_Output.display
- then Latex.environment "isabelle"
+ (if Config.get ctxt Thy_Output.display then
+ split_lines #> map (prefix indentation) #> cat_lines #>
+ Latex.environment "isabelle"
else enclose "\\isa{" "}")
end));
--- a/src/Pure/Thy/thy_output.ML Tue Nov 24 23:17:03 2015 +0100
+++ b/src/Pure/Thy/thy_output.ML Wed Nov 25 15:58:22 2015 +0100
@@ -601,6 +601,7 @@
fun verbatim_text ctxt =
if Config.get ctxt display then
+ split_lines #> map (prefix (Pretty.spaces (Config.get ctxt indent))) #> cat_lines #>
Latex.output_ascii #> Latex.environment "isabellett"
else
split_lines #>