Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

Improved 'verbatim' output (removed generated %-signs).

This commit is contained in:
Achim D. Brucker 2020-09-15 07:28:32 +01:00
parent 77e3490477
commit 137262890e
2 changed files with 17 additions and 18 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

23
examples/technical_report/Isabelle_DOF-Manual/00_Frontmatter.thy
View File

@ -46,51 +46,43 @@ ML\<open>
fun boxed_text_antiquotation name (* redefined in these more abstract terms *) =
DOF_lib.gen_text_antiquotation name DOF_lib.report_text
(fn ctxt => DOF_lib.string_2_text_antiquotation ctxt
#> DOF_lib.enclose_env ctxt "isarbox")
#> DOF_lib.enclose_env false ctxt "isarbox")
val neant = K(Latex.text("",\<^here>))
fun boxed_theory_text_antiquotation name (* redefined in these more abstract terms *) =
DOF_lib.gen_text_antiquotation name DOF_lib.report_theory_text
(fn ctxt => DOF_lib.string_2_theory_text_antiquotation ctxt
#> DOF_lib.enclose_env ctxt "isarbox"
#> DOF_lib.enclose_env false ctxt "isarbox"
(* #> neant *)) (*debugging *)
fun boxed_sml_text_antiquotation name =
DOF_lib.gen_text_antiquotation name (K(K()))
(fn ctxt => Input.source_content
#> Latex.text
#> DOF_lib.enclose_env ctxt "sml")
#> DOF_lib.enclose_env true ctxt "sml")
(* the simplest conversion possible *)
fun boxed_pdf_antiquotation name =
DOF_lib.gen_text_antiquotation name (K(K()))
(fn ctxt => Input.source_content
#> Latex.text
#> DOF_lib.enclose_env ctxt "out")
#> DOF_lib.enclose_env true ctxt "out")
(* the simplest conversion possible *)
fun boxed_latex_antiquotation name =
DOF_lib.gen_text_antiquotation name (K(K()))
(fn ctxt => Input.source_content
#> Latex.text
#> DOF_lib.enclose_env ctxt "ltx")
#> DOF_lib.enclose_env true ctxt "ltx")
(* the simplest conversion possible *)
fun boxed_bash_antiquotation name =
DOF_lib.gen_text_antiquotation name (K(K()))
(fn ctxt => Input.source_content
#> Latex.text
#> DOF_lib.enclose_env ctxt "bash")
#> DOF_lib.enclose_env true ctxt "bash")
(* the simplest conversion possible *)
fun boxed_isar_antiquotation name =
DOF_lib.gen_text_antiquotation name (K(K()))
(fn ctxt => Input.source_content
#> Latex.text
#> DOF_lib.enclose_env ctxt "isar")
(* the simplest conversion possible *)
\<close>
setup\<open>(* std_text_antiquotation \<^binding>\<open>my_text\<close> #> *)
@ -103,8 +95,7 @@ setup\<open>(* std_text_antiquotation \<^binding>\<open>my_text\<close> #
boxed_sml_text_antiquotation \<^binding>\<open>boxed_sml\<close> #>
boxed_pdf_antiquotation \<^binding>\<open>boxed_pdf\<close> #>
boxed_latex_antiquotation \<^binding>\<open>boxed_latex\<close>#>
boxed_bash_antiquotation \<^binding>\<open>boxed_bash\<close> #>
boxed_isar_antiquotation \<^binding>\<open>boxed_isar\<close> (* should be replaced by boxed_theory_text*)
boxed_bash_antiquotation \<^binding>\<open>boxed_bash\<close>
\<close>

12
src/DOF/Isa_COL.thy
View File

@ -371,10 +371,18 @@ fun theory_text_antiquotation name =
*)
fun environment_delim name =
("%\n\\begin{" ^ Latex.output_name name ^ "}\n",
"\n\\end{" ^ Latex.output_name name ^ "}");
fun enclose_env ctxt block_env body =
fun environment_block name = environment_delim name |-> Latex.enclose_body #> Latex.block;
fun enclose_env verbatim ctxt block_env body =
if Config.get ctxt Document_Antiquotation.thy_output_display
then Latex.environment_block block_env [body]
then if verbatim
then environment_block block_env [body]
else Latex.environment_block block_env [body]
else Latex.block ([Latex.string ("\\inline"^block_env ^"{")] @ [body] @ [ Latex.string ("}")]);
end