Enabled passing of default arguments to LaTeX backend.
HOL-OCL/Isabelle_DOF/master This commit looks good
Details
HOL-OCL/Isabelle_DOF/master This commit looks good
Details
This commit is contained in:
parent
c3409d1f10
commit
9d7ebc4a4f
21
Isa_DOF.thy
21
Isa_DOF.thy
|
@ -849,6 +849,8 @@ fun property_list_dest ctxt X = (map (fn Const ("Isa_DOF.ISA_term", _) $ s => HO
|
||||||
end; (* struct *)
|
end; (* struct *)
|
||||||
|
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
|
|
||||||
subsection\<open> Isar - Setup\<close>
|
subsection\<open> Isar - Setup\<close>
|
||||||
|
|
||||||
setup\<open>DOF_core.update_isa_global("typ" ,ISA_core.ML_isa_check_typ) \<close>
|
setup\<open>DOF_core.update_isa_global("typ" ,ISA_core.ML_isa_check_typ) \<close>
|
||||||
|
@ -885,8 +887,7 @@ fun meta_args_2_string thy ((((lab, _), cid_opt), attr_list) : meta_args_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 markup2string s = String.concat (List.filter (fn c => c <> Symbol.DEL) (Symbol.explode (YXML.content_of s)))
|
fun markup2string s = String.concat (List.filter (fn c => c <> Symbol.DEL) (Symbol.explode (YXML.content_of s)))
|
||||||
fun ltx_of_markup s = let
|
fun ltx_of_markup ctxt s = let
|
||||||
val ctxt = Proof_Context.init_global thy
|
|
||||||
val term = (Syntax.check_term ctxt o Syntax.parse_term ctxt) s
|
val term = (Syntax.check_term ctxt o Syntax.parse_term ctxt) s
|
||||||
val str_of_term = ltx_of_term ctxt term
|
val str_of_term = ltx_of_term ctxt term
|
||||||
handle _ => "Exception in ltx_of_term"
|
handle _ => "Exception in ltx_of_term"
|
||||||
|
@ -903,12 +904,18 @@ fun meta_args_2_string thy ((((lab, _), cid_opt), attr_list) : meta_args_t) =
|
||||||
end
|
end
|
||||||
fun toLong n = #long_name(the(DOF_core.get_attribute_info cid_long (markup2string n) thy))
|
fun toLong n = #long_name(the(DOF_core.get_attribute_info cid_long (markup2string n) thy))
|
||||||
|
|
||||||
fun str ((lhs,_),rhs) = (toLong lhs)^" = "^(enclose "{" "}" (ltx_of_markup rhs))
|
val ctxt = Proof_Context.init_global thy
|
||||||
(* no normalization on lhs (could be long-name)
|
val actual_args = map (fn ((lhs,_),rhs) => (toLong lhs, ltx_of_markup ctxt rhs))
|
||||||
no paraphrasing on rhs (could be fully paranthesized
|
attr_list
|
||||||
pretty-printed formula in LaTeX notation ... *)
|
val default_args = map (fn (b,_,t) => (toLong (Long_Name.base_name ( Sign.full_name thy b)), ltx_of_term ctxt t))
|
||||||
|
(DOF_core.get_attribute_defaults cid_long thy)
|
||||||
|
|
||||||
|
val default_args_filtered = filter (fn (a,_) => not (exists (fn b => b = a)
|
||||||
|
(map (fn (c,_) => c) actual_args))) default_args
|
||||||
|
val str_args = map (fn (lhs,rhs) => lhs^" = "^(enclose "{" "}" rhs))
|
||||||
|
(actual_args@default_args_filtered)
|
||||||
in
|
in
|
||||||
(enclose "[" "]" (String.concat [ cid_txt, ", args={", (commas ([cid_txt,l] @ (map str attr_list ))), "}"]))
|
(enclose "[" "]" (String.concat [ cid_txt, ", args={", (commas str_args), "}"]))
|
||||||
end
|
end
|
||||||
|
|
||||||
val semi = Scan.option (Parse.$$$ ";");
|
val semi = Scan.option (Parse.$$$ ";");
|
||||||
|
|
|
@ -62,7 +62,7 @@
|
||||||
,Isa_COL.side_by_side_figure.anchor2=%
|
,Isa_COL.side_by_side_figure.anchor2=%
|
||||||
,Isa_COL.side_by_side_figure.caption2=%
|
,Isa_COL.side_by_side_figure.caption2=%
|
||||||
,Isa_COL.side_by_side_figure.placement=%
|
,Isa_COL.side_by_side_figure.placement=%
|
||||||
,Isa_COL.side_by_side_figure.spawn_columns=enum False True%
|
,Isa_COL.figure.spawn_columns=enum False True%
|
||||||
][1]{%
|
][1]{%
|
||||||
\begin{figure}[]
|
\begin{figure}[]
|
||||||
\subfloat[\label{\commandkey{Isa_COL.side_by_side_figure.anchor}}\commandkey{Isa_COL.side_by_side_figure.caption}]%
|
\subfloat[\label{\commandkey{Isa_COL.side_by_side_figure.anchor}}\commandkey{Isa_COL.side_by_side_figure.caption}]%
|
||||||
|
|
|
@ -54,7 +54,7 @@
|
||||||
\NewEnviron{isamarkuptitle*}[1][]{\isaDof[env={title},#1]{\BODY}}
|
\NewEnviron{isamarkuptitle*}[1][]{\isaDof[env={title},#1]{\BODY}}
|
||||||
\newisadof{title.scholarly_paper.title}%
|
\newisadof{title.scholarly_paper.title}%
|
||||||
[label=,type=%
|
[label=,type=%
|
||||||
,keywordlist=%
|
,scholarly_paper.title.short_title=%
|
||||||
][1]{%
|
][1]{%
|
||||||
\immediate\write\@auxout{\noexpand\title{#1}}%
|
\immediate\write\@auxout{\noexpand\title{#1}}%
|
||||||
}
|
}
|
||||||
|
@ -66,7 +66,7 @@
|
||||||
\NewEnviron{isamarkupsubtitle*}[1][]{\isaDof[env={subtitle},#1]{\BODY}}
|
\NewEnviron{isamarkupsubtitle*}[1][]{\isaDof[env={subtitle},#1]{\BODY}}
|
||||||
\newisadof{subtitle.scholarly_paper.subtitle}%
|
\newisadof{subtitle.scholarly_paper.subtitle}%
|
||||||
[label=,type=%
|
[label=,type=%
|
||||||
,keywordlist=%
|
,scholarly_paper.subtitle.abbrev=%
|
||||||
][1]{%
|
][1]{%
|
||||||
\immediate\write\@auxout{\noexpand\subtitle{#1}}%
|
\immediate\write\@auxout{\noexpand\subtitle{#1}}%
|
||||||
}
|
}
|
||||||
|
@ -111,6 +111,7 @@
|
||||||
,scholarly_paper.author.email=%
|
,scholarly_paper.author.email=%
|
||||||
,scholarly_paper.author.affiliation=%
|
,scholarly_paper.author.affiliation=%
|
||||||
,scholarly_paper.author.orcid=%
|
,scholarly_paper.author.orcid=%
|
||||||
|
,scholarly_paper.author.http_site=%
|
||||||
][1]{%
|
][1]{%
|
||||||
\stepcounter{dof@cnt@author}
|
\stepcounter{dof@cnt@author}
|
||||||
\def\dof@a{\commandkey{scholarly_paper.author.affiliation}}
|
\def\dof@a{\commandkey{scholarly_paper.author.affiliation}}
|
||||||
|
|
Loading…
Reference in New Issue