diff --git a/Isa_DOF.thy b/Isa_DOF.thy index 7e9e4bee..9c256ed9 100644 --- a/Isa_DOF.thy +++ b/Isa_DOF.thy @@ -19,6 +19,7 @@ theory Isa_DOF (* Isabelle Document Ontology Framework *) "figure*" "side_by_side_figure*" "paragraph*" "subparagraph*" "text*" :: thy_decl + and "textbis" :: document_body and "open_monitor*" "close_monitor*" "declare_reference*" "update_instance*" "doc_class" ::thy_decl @@ -563,6 +564,10 @@ val _ = Outer_Syntax.command ("text*", @{here}) "formal comment (primary style)" (attributes -- Parse.opt_target -- Parse.document_source >> 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 _ = diff --git a/examples/scholarly/IsaDofApplications.thy b/examples/scholarly/IsaDofApplications.thy index b0981479..0c1b0c9c 100644 --- a/examples/scholarly/IsaDofApplications.thy +++ b/examples/scholarly/IsaDofApplications.thy @@ -292,6 +292,8 @@ figure*[fig1::figure, spawn_columns=False,relative_width="''95''", src="''figures/Dogfood-Intro''"] \ Ouroboros I: This paper from inside \ldots \ +textbis[ctest]\This is a crucial test : @{docitem_ref \fig1\} @{thm "refl"}\ + text\ @{docitem_ref \fig1\} 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 the underlying ontology. diff --git a/examples/simple/Concept_Example.thy b/examples/simple/Concept_Example.thy index dbf8054d..054e3f42 100644 --- a/examples/simple/Concept_Example.thy +++ b/examples/simple/Concept_Example.thy @@ -8,9 +8,11 @@ section*[a::A, x = "''alpha''"] \ Lorem ipsum dolor sit amet, ... \ text*[c1::C, x = "''beta''"] \ ... suspendisse non arcu malesuada mollis, nibh morbi, ... \ - + + text*[d::D, a1 = "X3"] -\ ... phasellus amet id massa nunc, pede suscipit repellendus, ... \ +\ ... phasellus amet id massa nunc, pede suscipit repellendus, ... @{docitem_ref \c1\} @{thm "refl"}\ + update_instance*[d::D, a1 := X2]