observe option "indent";
authorwenzelm
Wed Nov 25 15:58:22 2015 +0100 (2015-11-25)
changeset 61748fc53fbf9fe01
parent 61747 a870098fc27e
child 61749 7f530d7e552d
child 61750 c6c2508f94b8
observe option "indent";
NEWS
src/Pure/Thy/document_antiquotations.ML
src/Pure/Thy/thy_output.ML
     1.1 --- a/NEWS	Tue Nov 24 23:17:03 2015 +0100
     1.2 +++ b/NEWS	Wed Nov 25 15:58:22 2015 +0100
     1.3 @@ -92,7 +92,9 @@
     1.4  
     1.5  * Antiquotation @{theory_text} prints uninterpreted theory source text
     1.6  (outer syntax with command keywords etc.). This may be used in the short
     1.7 -form \<^theory_text>\<open>...\<close>.
     1.8 +form \<^theory_text>\<open>...\<close>.   @{theory_text [display]} supports option "indent".
     1.9 +
    1.10 +* @{verbatim [display]} supports option "indent".
    1.11  
    1.12  * Antiquotation @{doc ENTRY} provides a reference to the given
    1.13  documentation, with a hyperlink in the Prover IDE.
     2.1 --- a/src/Pure/Thy/document_antiquotations.ML	Tue Nov 24 23:17:03 2015 +0100
     2.2 +++ b/src/Pure/Thy/document_antiquotations.ML	Wed Nov 25 15:58:22 2015 +0100
     2.3 @@ -76,10 +76,13 @@
     2.4              |> Token.source' true keywords
     2.5              |> Source.exhaust;
     2.6            val _ = Context_Position.reports_text ctxt (maps (Token.reports keywords) toks);
     2.7 +          val indentation =
     2.8 +            Latex.output_symbols (replicate (Config.get ctxt Thy_Output.indent) Symbol.space);
     2.9          in
    2.10            implode (map Latex.output_token toks) |>
    2.11 -           (if Config.get ctxt Thy_Output.display
    2.12 -            then Latex.environment "isabelle"
    2.13 +           (if Config.get ctxt Thy_Output.display then
    2.14 +              split_lines #> map (prefix indentation) #> cat_lines #>
    2.15 +              Latex.environment "isabelle"
    2.16              else enclose "\\isa{" "}")
    2.17          end));
    2.18  
     3.1 --- a/src/Pure/Thy/thy_output.ML	Tue Nov 24 23:17:03 2015 +0100
     3.2 +++ b/src/Pure/Thy/thy_output.ML	Wed Nov 25 15:58:22 2015 +0100
     3.3 @@ -601,6 +601,7 @@
     3.4  
     3.5  fun verbatim_text ctxt =
     3.6    if Config.get ctxt display then
     3.7 +    split_lines #> map (prefix (Pretty.spaces (Config.get ctxt indent))) #> cat_lines #>
     3.8      Latex.output_ascii #> Latex.environment "isabellett"
     3.9    else
    3.10      split_lines #>