diff --git a/Isabelle_DOF-Example-I/IsaDofApplications.thy b/Isabelle_DOF-Example-I/IsaDofApplications.thy index e354adfa..cde82e9a 100644 --- a/Isabelle_DOF-Example-I/IsaDofApplications.thy +++ b/Isabelle_DOF-Example-I/IsaDofApplications.thy @@ -634,38 +634,34 @@ section*[ontopide::technical]\ Ontology-based IDE support \ text\ We present a selection of interaction scenarios @{example \scholar_onto\} and @{example \cenelec_onto\} with Isabelle/PIDE instrumented by \<^isadof>. \ +(*<*) +declare_reference*["text-elements"::float] +declare_reference*["hyperlinks"::float] +(*>*) + subsection*[scholar_pide::example]\ A Scholarly Paper \ -text\ In \<^unchecked_label>\fig-Dogfood-II-bgnd1\ and \<^unchecked_label>\fig-bgnd-text_section\ we show how +text\ In @{float (unchecked) "text-elements"}~(a) +and @{float (unchecked) "text-elements"}~(b)we show how hovering over links permits to explore its meta-information. Clicking on a document class identifier permits to hyperlink into the corresponding -class definition (\<^unchecked_label>\fig:Dogfood-IV-jumpInDocCLass\; hovering over an attribute-definition -(which is qualified in order to disambiguate; \<^unchecked_label>\fig:Dogfood-V-attribute\). +class definition (@{float (unchecked) "hyperlinks"}~(a)); hovering over an attribute-definition +(which is qualified in order to disambiguate; @{float (unchecked) "hyperlinks"}~(b)). \ text*["text-elements"::float, main_caption="\Exploring text elements.\"] \ -@{fig_content (width=48, caption="Exploring a Reference of a Text-Element.") "figures/Dogfood-II-bgnd1.png" -}\<^hfill>@{fig_content (width=47, caption="Exploring the class of a text element.") "figures/Dogfood-III-bgnd-text_section.png"} +@{fig_content (width=53, height=5, caption="Exploring a reference of a text element.") "figures/Dogfood-II-bgnd1.png" +}\<^hfill>@{fig_content (width=47, height=5, caption="Exploring the class of a text element.") "figures/Dogfood-III-bgnd-text_section.png"} \ text*["hyperlinks"::float, main_caption="\Hyperlinks.\"] \ @{fig_content (width=48, caption="Hyperlink to Class-Definition.") "figures/Dogfood-IV-jumpInDocCLass.png" -}\<^hfill>@{fig_content (width=47, caption="Exploring an attribute.") "figures/Dogfood-III-bgnd-text_section.png"} +}\<^hfill>@{fig_content (width=47, caption="Exploring an attribute.") "figures/Dogfood-V-attribute.png"} \ - -(*<*)declare_reference*["figDogfoodVIlinkappl"::figure](*>*) -text\ An ontological reference application in \<^unchecked_label>\figDogfoodVIlinkappl\: the ontology-dependant -antiquotation \<^theory_text>\@{example ...}\ refers to the corresponding text-elements. Hovering allows -for inspection, clicking for jumping to the definition. If the link does not exist or has a -non-compatible type, the text is not validated. \ - -figure*[figDogfoodVIlinkappl::figure,relative_width="80",file_src="''figures/Dogfood-V-attribute.png''"] - \ Exploring an attribute (hyperlinked to the class). \ - subsection*[cenelec_pide::example]\ CENELEC \ (*<*)declare_reference*[figfig3::figure](*>*) text\ The corresponding view in @{figure (unchecked) \figfig3\} shows core part of a document, diff --git a/Isabelle_DOF-Unit-Tests/Concept_OntoReferencing.thy b/Isabelle_DOF-Unit-Tests/Concept_OntoReferencing.thy index 6175fc0e..31aa9af4 100644 --- a/Isabelle_DOF-Unit-Tests/Concept_OntoReferencing.thy +++ b/Isabelle_DOF-Unit-Tests/Concept_OntoReferencing.thy @@ -108,13 +108,15 @@ find_theorems name:tagged "(_::cc_assumption_test \ _ \ declare_reference-assert-error[c1::C]\Duplicate instance declaration\ \ \forward declaration\ declare_reference*[e6::E] - +(*<*) (* pdf GENERATION NEEDS TO BE IMPLEMENTED IN FRONT AND BACKEND *) text\This is the answer to the "OutOfOrder Presentation Problem": @{E (unchecked) \e6\} \ definition*[e6::E] facu :: "nat \ nat" where "facu arg = undefined" text\As shown in @{E \e5\} following from @{E \e6\}\ + +(*>*) text\As shown in @{C \c4\}\