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

added macrodef - expand mechanism

This commit is contained in:
Burkhart Wolff 2020-04-10 18:30:33 +02:00
parent 0c4a5a5fea
commit e642243847
2 changed files with 14 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

17
src/DOF/Isa_DOF.thy
View File

@ -1600,13 +1600,20 @@ val docitem_antiquotation_parser = (Scan.lift (docitem_modes -- Args.text_input)
: ({define:bool,unchecked:bool} * Input.source) context_parser; : ({define:bool,unchecked:bool} * Input.source) context_parser;
fun pretty_docitem_antiquotation_generic cid_decl ctxt ({unchecked = x, define = y}, src ) = fun pretty_docitem_antiquotation_generic cid_decl ctxt ({unchecked, define}, src ) =
let (* val _ = writeln ("ZZZ" ^ Input.source_content src ^ "::2::" ^ cid_decl) *) let (* val _ = writeln ("ZZZ" ^ Input.source_content src ^ "::2::" ^ cid_decl) *)
val (str,pos) = Input.source_content src val (str,pos) = Input.source_content src
val _ = check_and_mark ctxt cid_decl ({strict_checking = not x}) pos str val _ = check_and_mark ctxt cid_decl ({strict_checking = not unchecked}) pos str
val inline = Config.get ctxt Document_Antiquotation.thy_output_display
val _ = if inline then writeln("HEUREKA") else ()
val enc = Latex.enclose_block
in in
(if y then Latex.enclose_block("\\csname isaDof.label\\endcsname[type={"^cid_decl^"}]{")"}" (case (define,inline) of
else Latex.enclose_block("\\csname isaDof.ref\\endcsname[type={"^cid_decl^"}]{") "}") (true,false) => enc("\\csname isaDof.label\\endcsname[type={"^cid_decl^"}] {")"}"
|(false,false)=> enc("\\csname isaDof.ref\\endcsname[type={"^cid_decl^"}] {")"}"
|(true,true) => enc("\\csname isaDof.macroDef\\endcsname[type={"^cid_decl^"}]{")"}"
|(false,true) => enc("\\csname isaDof.macroExp\\endcsname[type={"^cid_decl^"}]{")"}"
)
[Latex.text (Input.source_content src)] [Latex.text (Input.source_content src)]
end end
@ -1646,7 +1653,7 @@ val _ = Theory.setup
end (* struct *) end (* struct *)
\<close> \<close>
text\<open> @{thm [] refl}\<close>
ML\<open> ML\<open>
structure AttributeAccess = structure AttributeAccess =

2
src/DOF/latex/DOF-core.sty
View File

@ -154,5 +154,7 @@
% begin: label and ref % begin: label and ref
\newisadof{label}[label=,type=][1]{\label{#1}} \newisadof{label}[label=,type=][1]{\label{#1}}
\newisadof{ref}[label=,type=][1]{\autoref{#1}} \newisadof{ref}[label=,type=][1]{\autoref{#1}}
\newisadof{macroDef}[label=,type=][1]{MMM \label{#1}} %% place_holder
\newisadof{macroExp}[label=,type=][1]{MMM \autoref{#1}} %% place_holder
% end: label and ref % end: label and ref
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%