forked from Isabelle_DOF/Isabelle_DOF
Some intermediate Hack to find a solution of the text* problem.
textbis does both interactive and basically correct LaTeX generation with antiquotation expansion. At least a thing to study. bu
This commit is contained in:
parent
21cd7bbcfd
commit
a07900bfab
|
@ -19,6 +19,7 @@ theory Isa_DOF (* Isabelle Document Ontology Framework *)
|
||||||
"figure*" "side_by_side_figure*"
|
"figure*" "side_by_side_figure*"
|
||||||
"paragraph*" "subparagraph*"
|
"paragraph*" "subparagraph*"
|
||||||
"text*" :: thy_decl
|
"text*" :: thy_decl
|
||||||
|
and "textbis" :: document_body
|
||||||
|
|
||||||
and "open_monitor*" "close_monitor*" "declare_reference*"
|
and "open_monitor*" "close_monitor*" "declare_reference*"
|
||||||
"update_instance*" "doc_class" ::thy_decl
|
"update_instance*" "doc_class" ::thy_decl
|
||||||
|
@ -563,6 +564,10 @@ val _ =
|
||||||
Outer_Syntax.command ("text*", @{here}) "formal comment (primary style)"
|
Outer_Syntax.command ("text*", @{here}) "formal comment (primary style)"
|
||||||
(attributes -- Parse.opt_target -- Parse.document_source
|
(attributes -- Parse.opt_target -- Parse.document_source
|
||||||
>> enriched_document_command {markdown = true});
|
>> enriched_document_command {markdown = true});
|
||||||
|
val _ =
|
||||||
|
Outer_Syntax.command ("textbis", @{here}) "formal comment (primary style)"
|
||||||
|
(attributes -- Parse.opt_target -- Parse.document_source
|
||||||
|
>> enriched_document_command {markdown = true});
|
||||||
|
|
||||||
|
|
||||||
val _ =
|
val _ =
|
||||||
|
|
|
@ -292,6 +292,8 @@ figure*[fig1::figure, spawn_columns=False,relative_width="''95''",
|
||||||
src="''figures/Dogfood-Intro''"]
|
src="''figures/Dogfood-Intro''"]
|
||||||
\<open> Ouroboros I: This paper from inside \ldots \<close>
|
\<open> Ouroboros I: This paper from inside \ldots \<close>
|
||||||
|
|
||||||
|
textbis[ctest]\<open>This is a crucial test : @{docitem_ref \<open>fig1\<close>} @{thm "refl"}\<close>
|
||||||
|
|
||||||
text\<open> @{docitem_ref \<open>fig1\<close>} shows the corresponding view in the Isabelle/PIDE of the present paper.
|
text\<open> @{docitem_ref \<open>fig1\<close>} shows the corresponding view in the Isabelle/PIDE of the present paper.
|
||||||
Note that the text uses \isadof's own text-commands containing the meta-information provided by
|
Note that the text uses \isadof's own text-commands containing the meta-information provided by
|
||||||
the underlying ontology.
|
the underlying ontology.
|
||||||
|
|
|
@ -8,9 +8,11 @@ section*[a::A, x = "''alpha''"] \<open> Lorem ipsum dolor sit amet, ... \<close>
|
||||||
|
|
||||||
text*[c1::C, x = "''beta''"]
|
text*[c1::C, x = "''beta''"]
|
||||||
\<open> ... suspendisse non arcu malesuada mollis, nibh morbi, ... \<close>
|
\<open> ... suspendisse non arcu malesuada mollis, nibh morbi, ... \<close>
|
||||||
|
|
||||||
|
|
||||||
text*[d::D, a1 = "X3"]
|
text*[d::D, a1 = "X3"]
|
||||||
\<open> ... phasellus amet id massa nunc, pede suscipit repellendus, ... \<close>
|
\<open> ... phasellus amet id massa nunc, pede suscipit repellendus, ... @{docitem_ref \<open>c1\<close>} @{thm "refl"}\<close>
|
||||||
|
|
||||||
|
|
||||||
update_instance*[d::D, a1 := X2]
|
update_instance*[d::D, a1 := X2]
|
||||||
|
|
||||||
|
|
Reference in New Issue