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

Figure group.

This commit is contained in:
Achim D. Brucker 2018-12-04 06:05:49 +00:00
parent 0f2dc58f5a
commit 459538a1b7
2 changed files with 20 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
Isa_COL.thy
View File

@ -13,7 +13,9 @@ begin
section\<open> Library of Standard Text Ontology \<close>
datatype placement = pl_h | pl_t | pl_b | pl_ht | pl_hb
datatype placement = pl_h | pl_t | pl_b | pl_ht | pl_hb
doc_class figure =
relative_width :: "int" (* percent of textwidth *)
src :: "string"
@ -32,9 +34,8 @@ doc_class side_by_side_figure = figure +
ML\<open>DOF_core.SPY;\<close>
doc_class figure_group =
(* trace :: "doc_class rexp list" <= "[]" automatically generated since monitor clause *)
anchor :: "string"
caption :: "string"
rejects figure, figure_group (* this forbids recursive figure-groups *)
rejects figure_group (* this forbids recursive figure-groups *)
accepts "\<lbrace>figure\<rbrace>\<^sup>+"
ML\<open>@{term "side_by_side_figure"};

22
examples/technical_report/IsaDof_Manual/03_IsaDof.thy
View File

@ -429,12 +429,22 @@ Clicking on a document class identifier permits to hyperlink into the correspond
class definition (\autoref{fig:Dogfood-IV-jumpInDocCLass}); hovering over an attribute-definition
(which is qualified in order to disambiguate; \autoref{fig:Dogfood-V-attribute}).
\<close>
side_by_side_figure*["text-elements"::side_by_side_figure,anchor="''fig-Dogfood-II-bgnd1''",
caption="''Exploring a Reference of a Text-Element.''",relative_width="48",
src="''figures/Dogfood-II-bgnd1''",anchor2="''fig-bgnd-text_section''",
caption2="''Exploring the class of a text element.''",relative_width2="47",
src2="''figures/Dogfood-III-bgnd-text_section''"]\<open> Exploring text elements. \<close>
open_monitor*["text-elements"::figure_group,
caption="''Exploring text elements.''"]
figure*["fig-Dogfood-II-bgnd1"::figure, spawn_columns=False,
relative_width="48",
src="''figures/Dogfood-II-bgnd1''"]
\<open>Exploring a Reference of a Text-Element.\<close>
figure*["fig-bgnd-text_section"::figure, spawn_columns=False,
relative_width="48",
src="''figures/Dogfood-III-bgnd-text_section''"]
\<open>Exploring the class of a text element.\<close>
close_monitor*["text-elements"]
side_by_side_figure*["hyperlinks"::side_by_side_figure,anchor="''fig:Dogfood-IV-jumpInDocCLass''",
caption="''Hyperlink to Class-Definition.''",relative_width="48",