From ed65ce54ed64969116120fea909cc23a587ba395 Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Mon, 17 Jun 2019 10:10:29 +0100 Subject: [PATCH] Ported LaTeX document generation to Isabelle 2018. --- Isa_DOF.thy | 20 +++++++------------- document-generator/latex/DOF-COL.sty | 3 ++- 2 files changed, 9 insertions(+), 14 deletions(-) diff --git a/Isa_DOF.thy b/Isa_DOF.thy index f01a6b3..cb2871f 100644 --- a/Isa_DOF.thy +++ b/Isa_DOF.thy @@ -1457,10 +1457,8 @@ val _ = end (* struct *) - \ - ML\ structure ODL_LTX_Converter = struct @@ -1474,20 +1472,19 @@ fun meta_args_2_string thy ((((lab, _), cid_opt), attr_list) : ODL_Command_Parse | SOME(cid,_) => DOF_core.name2doc_class_name thy cid val cid_txt = "type = " ^ (enclose "{" "}" cid_long); - - fun (* ltx_of_term _ _ (((Const ("List.list.Cons", t1) $ (Const ("String.Char", t2 ) $ t))) $ t') - = (HOLogic.dest_string (((Const ("List.list.Cons", t1) $ (Const ("String.Char", t2 ) $ t))) $ t')) + fun ltx_of_term _ _ (Const ("List.list.Cons", @{typ "char \ char list \ char list"}) $ t1 $ t2) + = HOLogic.dest_string (Const ("List.list.Cons", @{typ "char \ char list \ char list"}) $ t1 $ t2) | ltx_of_term _ _ (Const ("List.list.Nil", _)) = "" | ltx_of_term _ _ (@{term "numeral :: _ \ _"} $ t) = Int.toString(HOLogic.dest_numeral t) | ltx_of_term ctx encl ((Const ("List.list.Cons", _) $ t1) $ t2) = let val inner = (case t2 of - Const ("List.list.Nil", _) => (ltx_of_term ctx true t1) + Const ("List.list.Nil", _) => (ltx_of_term ctx true t1) | _ => ((ltx_of_term ctx false t1)^", " ^(ltx_of_term ctx false t2)) ) in if encl then enclose "{" "}" inner else inner end | ltx_of_term _ _ (Const ("Option.option.None", _)) = "" | ltx_of_term ctxt _ (Const ("Option.option.Some", _)$t) = ltx_of_term ctxt true t - | *)ltx_of_term ctxt _ t = ""^(Sledgehammer_Util.hackish_string_of_term ctxt t) + | ltx_of_term ctxt _ t = ""^(Sledgehammer_Util.hackish_string_of_term ctxt t) fun ltx_of_term_dbg ctx encl term = let @@ -1688,13 +1685,10 @@ fun pretty_docitem_antiquotation_generic cid_decl ctxt ({unchecked = x, define = val _ = check_and_mark ctxt cid_decl ({strict_checking = not x}) (Input.pos_of src) (Input.source_content src) - in (*(if y then Latex.enclose_block "\\label{" "}" - else Latex.enclose_block "\\autoref{" "}") - [Latex.string (Input.source_content src)]*) - (if y then Latex.enclose_block ("\\labelX[type="^cid_decl^"]{") "}" - else Latex.enclose_block ("\\autorefX[type="^cid_decl^"]{") "}") + in + (if y then Latex.enclose_block ("\\csname isadof.label[type={"^cid_decl^"}]{") "}\\endcsname" + else Latex.enclose_block ("\\csname isadof.ref[type={"^cid_decl^"}]{") "}\\endcsname") [Latex.string (Input.source_content src)] - end diff --git a/document-generator/latex/DOF-COL.sty b/document-generator/latex/DOF-COL.sty index 088dbc8..2a02a04 100644 --- a/document-generator/latex/DOF-COL.sty +++ b/document-generator/latex/DOF-COL.sty @@ -1,5 +1,6 @@ %% Copyright (C) 2018 The University of Sheffield %% 2018 The University of Paris-Sud +%% 2019 The University of Exeter %% %% License: %% This program can be redistributed and/or modified under the terms @@ -50,7 +51,7 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % begin: side_by_side_figure* -\NewEnviron{isamarkupside_by_side_figure*}[1][]{\isaDof[env={side_by_side_figure},#1]{\BODY}} +\NewEnviron{isamarkupsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigure*}[1][]{\isaDof[env={side_by_side_figure},#1]{\BODY}} \newisadof{side_by_side_figure.Isa_COL.side_by_side_figure}% [label=,type=% ,Isa_COL.figure.relative_width=%