pierre.derathe
/
Isabelle_DOF
Archived
forked from Isabelle_DOF/Isabelle_DOF
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Bug fix: fixed label/ref generation.

This commit is contained in:
Achim D. Brucker 2019-07-02 05:30:24 +01:00
parent db83359f88
commit 15993c6536
1 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
Isa_DOF.thy
View File

@ -1688,8 +1688,8 @@ fun pretty_docitem_antiquotation_generic cid_decl ctxt ({unchecked = x, define =
val _ = check_and_mark ctxt cid_decl
({strict_checking = not x}) pos str
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")
(if y then Latex.enclose_block ("\\csname isaDof.label\\endcsname[type={"^cid_decl^"}]{") "}"
else Latex.enclose_block ("\\csname isaDof.ref\\endcsname[type={"^cid_decl^"}]{") "}")
[Latex.text (Input.source_content src)]
end