# HG changeset patch
# User haftmann
# Date 1547490833 0
# Node ID 2bc2a85993693dcc98e5fdf7f20324c9ce77de9d
# Parent  07025152dd80b70e0c6f46e381edd90ad776582c
canonical operation to typeset generated code makes dedicated environment obsolete

diff -r 07025152dd80 -r 2bc2a8599369 src/Doc/Classes/Classes.thy
--- a/src/Doc/Classes/Classes.thy	Mon Jan 14 18:33:52 2019 +0000
+++ b/src/Doc/Classes/Classes.thy	Mon Jan 14 18:33:53 2019 +0000
@@ -588,14 +588,14 @@
 text \<open>
   \<^noindent> This maps to Haskell as follows:
 \<close>
-text %quotetypewriter \<open>
+text %quote \<open>
   @{code_stmts example (Haskell)}
 \<close>
 
 text \<open>
   \<^noindent> The code in SML has explicit dictionary passing:
 \<close>
-text %quotetypewriter \<open>
+text %quote \<open>
   @{code_stmts example (SML)}
 \<close>
 
@@ -603,7 +603,7 @@
 text \<open>
   \<^noindent> In Scala, implicits are used as dictionaries:
 \<close>
-text %quotetypewriter \<open>
+text %quote \<open>
   @{code_stmts example (Scala)}
 \<close>
 
diff -r 07025152dd80 -r 2bc2a8599369 src/Doc/Classes/document/style.sty
--- a/src/Doc/Classes/document/style.sty	Mon Jan 14 18:33:52 2019 +0000
+++ b/src/Doc/Classes/document/style.sty	Mon Jan 14 18:33:53 2019 +0000
@@ -27,18 +27,6 @@
 \renewcommand{\endisatagquote}{\end{quote}}
 \newcommand{\quotebreak}{\\[1.2ex]}
 
-%% typewriter text
-\newenvironment{typewriter}{\renewcommand{\isastyletext}{}%
-\renewcommand{\isadigit}[1]{{##1}}%
-\parindent0pt%
-\makeatletter\isa@parindent0pt\makeatother%
-\isabellestyle{tt}\isastyle%
-\fontsize{9pt}{9pt}\selectfont}{}
-
-\isakeeptag{quotetypewriter}
-\renewcommand{\isatagquotetypewriter}{\begin{quote}\begin{typewriter}}
-\renewcommand{\endisatagquotetypewriter}{\end{typewriter}\end{quote}}
-
 %% presentation
 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
 
@@ -50,6 +38,7 @@
 %% format
 \pagestyle{headings}
 \isabellestyle{it}
+\def\isastylett{\footnotesize\normalfont\ttfamily}
 
 
 %%% Local Variables: 
diff -r 07025152dd80 -r 2bc2a8599369 src/Doc/Codegen/Adaptation.thy
--- a/src/Doc/Codegen/Adaptation.thy	Mon Jan 14 18:33:52 2019 +0000
+++ b/src/Doc/Codegen/Adaptation.thy	Mon Jan 14 18:33:53 2019 +0000
@@ -232,7 +232,7 @@
 | constant HOL.conj \<rightharpoonup> (SML)
 | constant Not \<rightharpoonup> (SML)
 (*>*)
-text %quotetypewriter \<open>
+text %quote \<open>
   @{code_stmts in_interval (SML)}
 \<close>
 
@@ -262,7 +262,7 @@
   placeholder for the constant's or the type constructor's arguments.
 \<close>
 
-text %quotetypewriter \<open>
+text %quote \<open>
   @{code_stmts in_interval (SML)}
 \<close>
 
@@ -277,7 +277,7 @@
 code_printing %quotett
   constant HOL.conj \<rightharpoonup> (SML) infixl 1 "andalso"
 
-text %quotetypewriter \<open>
+text %quote \<open>
   @{code_stmts in_interval (SML)}
 \<close>
 
diff -r 07025152dd80 -r 2bc2a8599369 src/Doc/Codegen/Computations.thy
--- a/src/Doc/Codegen/Computations.thy	Mon Jan 14 18:33:52 2019 +0000
+++ b/src/Doc/Codegen/Computations.thy	Mon Jan 14 18:33:53 2019 +0000
@@ -16,7 +16,7 @@
 
 datatype %quote form = T | F | And form form | Or form form (*<*)
 
-(*>*) ML %quotetypewriter \<open>
+(*>*) ML %quote \<open>
   fun eval_form @{code T} = true
     | eval_form @{code F} = false
     | eval_form (@{code And} (p, q)) =
@@ -97,7 +97,7 @@
   The following example illustrates its basic usage:
 \<close>
 
-ML %quotetypewriter \<open>
+ML %quote \<open>
   local
 
   fun int_of_nat @{code "0 :: nat"} = 0
@@ -164,7 +164,7 @@
   \noindent A simple application:
 \<close>
 
-ML_val %quotetypewriter \<open>
+ML_val %quote \<open>
   comp_nat \<^context> \<^term>\<open>sum_list [Suc 0, Suc (Suc 0)] * Suc (Suc 0)\<close>
 \<close>
 
@@ -177,7 +177,7 @@
   and for all:
 \<close>
 
-ML %quotetypewriter \<open>
+ML %quote \<open>
   local
 
   fun int_of_nat @{code "0 :: nat"} = 0
@@ -269,7 +269,7 @@
   \secref{sec:literal_input}.}
 \<close>
 
-ML %quotetypewriter \<open>
+ML %quote \<open>
   local
 
   fun raw_dvd (b, ct) = Thm.mk_binop \<^cterm>\<open>Pure.eq :: bool \<Rightarrow> bool \<Rightarrow> prop\<close>
@@ -310,7 +310,7 @@
     \<^item> Partiality makes the whole conversion fall back to reflexivity.
 \<close> (*<*)
 
-(*>*) ML_val %quotetypewriter \<open>
+(*>*) ML_val %quote \<open>
   conv_dvd \<^context> \<^cterm>\<open>7 dvd ( 62437867527846782 :: int)\<close>;
   conv_dvd \<^context> \<^cterm>\<open>7 dvd (-62437867527846783 :: int)\<close>;
 \<close>
@@ -336,7 +336,7 @@
     Code_Target_Int.positive (r * s)"
   by simp
   
-ML %quotetypewriter \<open>
+ML %quote \<open>
   local
 
   fun integer_of_int (@{code int_of_integer} k) = k
@@ -365,7 +365,7 @@
   end
 \<close>
 
-ML_val %quotetypewriter \<open>
+ML_val %quote \<open>
   conv_div \<^context>
     \<^cterm>\<open>46782454343499999992777742432342242323423425 div (7 :: int)\<close>
 \<close>
@@ -393,7 +393,7 @@
   once and for all:
 \<close>
 
-ML %quotetypewriter \<open>
+ML %quote \<open>
   val check_nat = @{computation_check terms:
     Trueprop "less :: nat \<Rightarrow> nat \<Rightarrow> bool" "plus :: nat \<Rightarrow> nat \<Rightarrow> nat" 
     "times :: nat \<Rightarrow> nat \<Rightarrow> nat"
@@ -406,7 +406,7 @@
   of type \<^typ>\<open>bool\<close> into \<^typ>\<open>prop\<close>.
 \<close>
 
-ML_val %quotetypewriter \<open>
+ML_val %quote \<open>
   check_nat \<^context> \<^cprop>\<open>less (Suc (Suc 0)) (Suc (Suc (Suc 0)))\<close>
 \<close>
 
@@ -448,27 +448,27 @@
 
 paragraph \<open>An example for \<^typ>\<open>nat\<close>\<close>
 
-ML %quotetypewriter \<open>
+ML %quote \<open>
   val check_nat = @{computation_check terms:
     Trueprop "even :: nat \<Rightarrow> bool" "plus :: nat \<Rightarrow> nat \<Rightarrow> nat" 
     "0 :: nat" Suc "1 :: nat" "2 :: nat" "3 :: nat"
   }
 \<close>
 
-ML_val %quotetypewriter \<open>
+ML_val %quote \<open>
   check_nat \<^context> \<^cprop>\<open>even (Suc 0 + 1 + 2 + 3 + 4 + 5)\<close>
 \<close>
   
 paragraph \<open>An example for \<^typ>\<open>int\<close>\<close>
 
-ML %quotetypewriter \<open>
+ML %quote \<open>
   val check_int = @{computation_check terms:
     Trueprop "even :: int \<Rightarrow> bool" "plus :: int \<Rightarrow> int \<Rightarrow> int" 
     "0 :: int" "1 :: int" "2 :: int" "3 :: int" "-1 :: int"
   }
 \<close>
 
-ML_val %quotetypewriter \<open>
+ML_val %quote \<open>
   check_int \<^context> \<^cprop>\<open>even ((0::int) + 1 + 2 + 3 + -1 + -2 + -3)\<close>
 \<close>
   
@@ -478,13 +478,13 @@
   where "is_cap_letter s \<longleftrightarrow> (case String.asciis_of_literal s
     of [] \<Rightarrow> False | k # _ \<Rightarrow> 65 \<le> k \<and> k \<le> 90)" (*<*)
 
-(*>*) ML %quotetypewriter \<open>
+(*>*) ML %quote \<open>
   val check_literal = @{computation_check terms:
     Trueprop is_cap_letter datatypes: bool String.literal
   }
 \<close>
 
-ML_val %quotetypewriter \<open>
+ML_val %quote \<open>
   check_literal \<^context> \<^cprop>\<open>is_cap_letter (STR ''Q'')\<close>
 \<close>
 
@@ -523,13 +523,13 @@
   whose concrete values are given in list \<^term>\<open>vs\<close>.
 \<close>
 
-ML %quotetypewriter (*<*) \<open>\<close>
+ML %quote (*<*) \<open>\<close>
 lemma "thm": fixes x y z :: "'a::order" shows "x < y \<and> x < z \<equiv> interp (And (Less (Suc 0) (Suc (Suc 0))) (Less (Suc 0) 0)) [z, x, y]"
-ML_prf %quotetypewriter
+ML_prf %quote
 (*>*) \<open>val thm =
   Reification.conv \<^context> @{thms interp.simps} \<^cterm>\<open>x < y \<and> x < z\<close>\<close> (*<*)
 by (tactic \<open>ALLGOALS (resolve_tac \<^context> [thm])\<close>)
-(*>*) 
+(*>*)
 
 text \<open>
   \noindent By virtue of @{fact interp.simps}, \<^ML>\<open>Reification.conv\<close> provides a conversion
diff -r 07025152dd80 -r 2bc2a8599369 src/Doc/Codegen/Foundations.thy
--- a/src/Doc/Codegen/Foundations.thy	Mon Jan 14 18:33:52 2019 +0000
+++ b/src/Doc/Codegen/Foundations.thy	Mon Jan 14 18:33:53 2019 +0000
@@ -190,7 +190,7 @@
   is determined syntactically.  The resulting code:
 \<close>
 
-text %quotetypewriter \<open>
+text %quote \<open>
   @{code_stmts dequeue (consts) dequeue (Haskell)}
 \<close>
 
@@ -245,7 +245,7 @@
   equality check, as can be seen in the corresponding \<open>SML\<close> code:
 \<close>
 
-text %quotetypewriter \<open>
+text %quote \<open>
   @{code_stmts collect_duplicates (SML)}
 \<close>
 
@@ -282,7 +282,7 @@
   for the pattern \<^term>\<open>AQueue [] []\<close>:
 \<close>
 
-text %quotetypewriter \<open>
+text %quote \<open>
   @{code_stmts strict_dequeue (consts) strict_dequeue (Haskell)}
 \<close>
 
@@ -324,7 +324,7 @@
   exception at the appropriate position:
 \<close>
 
-text %quotetypewriter \<open>
+text %quote \<open>
   @{code_stmts strict_dequeue' (consts) empty_queue strict_dequeue' (Haskell)}
 \<close>
 
diff -r 07025152dd80 -r 2bc2a8599369 src/Doc/Codegen/Further.thy
--- a/src/Doc/Codegen/Further.thy	Mon Jan 14 18:33:52 2019 +0000
+++ b/src/Doc/Codegen/Further.thy	Mon Jan 14 18:33:53 2019 +0000
@@ -193,7 +193,7 @@
   After this setup procedure, code generation can continue as usual:
 \<close>
 
-text %quotetypewriter \<open>
+text %quote \<open>
   @{code_stmts funpows (consts) Nat.funpow funpows (Haskell)}
 \<close>
 
diff -r 07025152dd80 -r 2bc2a8599369 src/Doc/Codegen/Introduction.thy
--- a/src/Doc/Codegen/Introduction.thy	Mon Jan 14 18:33:52 2019 +0000
+++ b/src/Doc/Codegen/Introduction.thy	Mon Jan 14 18:33:53 2019 +0000
@@ -73,7 +73,7 @@
 
 text \<open>\noindent resulting in the following code:\<close>
 
-text %quotetypewriter \<open>
+text %quote \<open>
   @{code_stmts empty enqueue dequeue (SML)}
 \<close>
 
@@ -96,7 +96,7 @@
   \noindent This is the corresponding code:
 \<close>
 
-text %quotetypewriter \<open>
+text %quote \<open>
   @{code_stmts empty enqueue dequeue (Haskell)}
 \<close>
 
@@ -171,7 +171,7 @@
   native classes:
 \<close>
 
-text %quotetypewriter \<open>
+text %quote \<open>
   @{code_stmts bexp (Haskell)}
 \<close>
 
@@ -181,7 +181,7 @@
   \<open>SML\<close>:
 \<close>
 
-text %quotetypewriter \<open>
+text %quote \<open>
   @{code_stmts bexp (SML)}
 \<close>
 
diff -r 07025152dd80 -r 2bc2a8599369 src/Doc/Codegen/Refinement.thy
--- a/src/Doc/Codegen/Refinement.thy	Mon Jan 14 18:33:52 2019 +0000
+++ b/src/Doc/Codegen/Refinement.thy	Mon Jan 14 18:33:53 2019 +0000
@@ -31,7 +31,7 @@
   to two recursive calls:
 \<close>
 
-text %quotetypewriter \<open>
+text %quote \<open>
   @{code_stmts fib (consts) fib (Haskell)}
 \<close>
 
@@ -68,7 +68,7 @@
   \noindent The resulting code shows only linear growth of runtime:
 \<close>
 
-text %quotetypewriter \<open>
+text %quote \<open>
   @{code_stmts fib (consts) fib fib_step (Haskell)}
 \<close>
 
@@ -161,7 +161,7 @@
   \noindent The resulting code looks as expected:
 \<close>
 
-text %quotetypewriter \<open>
+text %quote \<open>
   @{code_stmts empty enqueue dequeue Queue case_queue (SML)}
 \<close>
 
@@ -260,7 +260,7 @@
   \noindent Then the corresponding code is as follows:
 \<close>
 
-text %quotetypewriter \<open>
+text %quote \<open>
   @{code_stmts Dlist.empty Dlist.insert Dlist.remove list_of_dlist (Haskell)}
 \<close>
 
diff -r 07025152dd80 -r 2bc2a8599369 src/Doc/Codegen/document/style.sty
--- a/src/Doc/Codegen/document/style.sty	Mon Jan 14 18:33:52 2019 +0000
+++ b/src/Doc/Codegen/document/style.sty	Mon Jan 14 18:33:53 2019 +0000
@@ -31,17 +31,6 @@
 \newcommand{\quotebreak}{\\[1.2ex]}
 
 %% typewriter text
-\newenvironment{typewriter}{\renewcommand{\isastyletext}{}%
-\renewcommand{\isadigit}[1]{{##1}}%
-\parindent0pt%
-\makeatletter\isa@parindent0pt\makeatother%
-\isabellestyle{tt}\isastyle%
-\fontsize{9pt}{9pt}\selectfont}{}
-
-\isakeeptag{quotetypewriter}
-\renewcommand{\isatagquotetypewriter}{\begin{quote}\begin{typewriter}}
-\renewcommand{\endisatagquotetypewriter}{\end{typewriter}\end{quote}}
-
 \isakeeptag{quotett}
 \renewcommand{\isatagquotett}{\begin{quote}\isabellestyle{tt}\isastyle}
 \renewcommand{\endisatagquotett}{\end{quote}}
@@ -70,6 +59,7 @@
 \renewcommand{\endisatagmlref}{\endgroup}
 
 \isabellestyle{it}
+\def\isastylett{\footnotesize\normalfont\ttfamily}
 
 
 %%% Local Variables: 
diff -r 07025152dd80 -r 2bc2a8599369 src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Mon Jan 14 18:33:52 2019 +0000
+++ b/src/Tools/Code/code_target.ML	Mon Jan 14 18:33:53 2019 +0000
@@ -545,10 +545,11 @@
       Scan.repeat (parse_consts || parse_types || parse_classes || parse_instances)
       -- Scan.lift (Args.parens (Args.name -- Scan.option Parse.int)))
     (fn ctxt => fn ((read_constants, reads_statements), (target_name, some_width)) =>
-      Latex.string
-        (Latex.output_ascii (present_code ctxt (read_constants ctxt)
-          (maps (fn read_statements => read_statements ctxt) reads_statements)
-          target_name "Example" some_width []))));
+       present_code ctxt (read_constants ctxt)
+         (maps (fn read_statements => read_statements ctxt) reads_statements)
+         target_name "Example" some_width []
+       |> trim_line
+       |> Thy_Output.verbatim (Config.put Document_Antiquotation.thy_output_display true ctxt)));
 
 end;