diff --git a/Isabelle_DOF-Ontologies/Conceptual/Conceptual.thy b/Isabelle_DOF-Ontologies/Conceptual/Conceptual.thy index c3ed081..f718a97 100644 --- a/Isabelle_DOF-Ontologies/Conceptual/Conceptual.thy +++ b/Isabelle_DOF-Ontologies/Conceptual/Conceptual.thy @@ -209,7 +209,8 @@ let val class_ids_so_far = ["Conceptual.A", "Conceptual.B", "Conceptual.C", "Co "Conceptual.E", "Conceptual.F", "Conceptual.G", "Conceptual.M", "Isa_COL.float", "Isa_COL.frame", "Isa_COL.figure", "Isa_COL.chapter", "Isa_COL.listing", "Isa_COL.section", "Isa_COL.paragraph", - "Isa_COL.subsection", "Isa_COL.text_element", "Isa_COL.subsubsection"] + "Isa_COL.subsection", "Isa_COL.subparagraph", + "Isa_COL.text_element", "Isa_COL.subsubsection"] val docclass_tab = map fst (Name_Space.dest_table (DOF_core.get_onto_classes \<^context>)); in @{assert} (class_ids_so_far = docclass_tab) end\ diff --git a/Isabelle_DOF/latex/styles/DOF-core.sty b/Isabelle_DOF/latex/styles/DOF-core.sty index bd5a2be..ae807d9 100644 --- a/Isabelle_DOF/latex/styles/DOF-core.sty +++ b/Isabelle_DOF/latex/styles/DOF-core.sty @@ -94,31 +94,31 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % begin: chapter*-dispatcher -\NewEnviron{isamarkupchapter*}[1][]{\isaDof[env={IsaUNDERSCORECOLDOTchapter},#1]{\BODY}} +%\NewEnviron{isamarkupchapter*}[1][]{\isaDof[env={IsaUNDERSCORECOLDOTchapter},#1]{\BODY}} % end: chapter*-dispatcher %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % begin: section*-dispatcher -\NewEnviron{isamarkupsection*}[1][]{\isaDof[env={IsaUNDERSCORECOLDOTsection},#1]{\BODY}} +%\NewEnviron{isamarkupsection*}[1][]{\isaDof[env={IsaUNDERSCORECOLDOTsection},#1]{\BODY}} % end: section*-dispatcher %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % begin: subsection*-dispatcher -\NewEnviron{isamarkupsubsection*}[1][]{\isaDof[env={IsaUNDERSCORECOLDOTsubsection},#1]{\BODY}} +%\NewEnviron{isamarkupsubsection*}[1][]{\isaDof[env={IsaUNDERSCORECOLDOTsubsection},#1]{\BODY}} % end: subsection*-dispatcher %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % begin: subsubsection*-dispatcher -\NewEnviron{isamarkupsubsubsection*}[1][]{\isaDof[env={IsaUNDERSCORECOLDOTsubsubsection},#1]{\BODY}} +%\NewEnviron{isamarkupsubsubsection*}[1][]{\isaDof[env={IsaUNDERSCORECOLDOTsubsubsection},#1]{\BODY}} % end: subsubsection*-dispatcher %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % begin: paragraph*-dispatcher -\NewEnviron{isamarkupparagraph*}[1][]{\isaDof[env={IsaUNDERSCORECOLDOTparagraph},#1]{\BODY}} +%\NewEnviron{isamarkupparagraph*}[1][]{\isaDof[env={IsaUNDERSCORECOLDOTparagraph},#1]{\BODY}} % end: paragraph*-dispatcher %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @@ -135,21 +135,21 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % begin: chapter/section default implementations -\newisadof{IsaUNDERSCORECOLDOTchapter}[label=,type=,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTlevel=, IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTreferentiable=,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTvariants=][1]{% - \isamarkupfalse\isamarkupchapter{#1}\label{\commandkey{label}}\isamarkuptrue% -} -\newisadof{IsaUNDERSCORECOLDOTsection}[label=,type=,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTlevel=, IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTreferentiable=,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTvariants=][1]{% - \isamarkupfalse\isamarkupsection{#1}\label{\commandkey{label}}\isamarkuptrue% -} -\newisadof{IsaUNDERSCORECOLDOTsubsection}[label=,type=,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTlevel=, IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTreferentiable=,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTvariants=][1]{% - \isamarkupfalse\isamarkupsubsection{#1}\label{\commandkey{label}}\isamarkuptrue% -} -\newisadof{IsaUNDERSCORECOLDOTsubsubsection}[label=,type=,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTlevel=, IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTreferentiable=,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTvariants=][1]{% - \isamarkupfalse\isamarkupsubsubsection{#1}\label{\commandkey{label}}\isamarkuptrue% -} -\newisadof{IsaUNDERSCORECOLDOTparagraph}[label=,type=,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTlevel=, IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTreferentiable=,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTvariants=][1]{% - \isamarkupfalse\isamarkupparagraph{#1}\label{\commandkey{label}}\isamarkuptrue% -} +%\newisadof{IsaUNDERSCORECOLDOTchapter}[label=,type=,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTlevel=, IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTreferentiable=,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTvariants=][1]{% +% \isamarkupfalse\isamarkupchapter{#1}\label{\commandkey{label}}\isamarkuptrue% +%} +%\newisadof{IsaUNDERSCORECOLDOTsection}[label=,type=,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTlevel=, IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTreferentiable=,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTvariants=][1]{% +% \isamarkupfalse\isamarkupsection{#1}\label{\commandkey{label}}\isamarkuptrue% +%} +%\newisadof{IsaUNDERSCORECOLDOTsubsection}[label=,type=,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTlevel=, IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTreferentiable=,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTvariants=][1]{% +% \isamarkupfalse\isamarkupsubsection{#1}\label{\commandkey{label}}\isamarkuptrue% +%} +%\newisadof{IsaUNDERSCORECOLDOTsubsubsection}[label=,type=,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTlevel=, IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTreferentiable=,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTvariants=][1]{% +% \isamarkupfalse\isamarkupsubsubsection{#1}\label{\commandkey{label}}\isamarkuptrue% +%} +%\newisadof{IsaUNDERSCORECOLDOTparagraph}[label=,type=,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTlevel=, IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTreferentiable=,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTvariants=][1]{% +% \isamarkupfalse\isamarkupparagraph{#1}\label{\commandkey{label}}\isamarkuptrue% +%} % end: chapter/section default implementations %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% diff --git a/Isabelle_DOF/thys/Isa_COL.thy b/Isabelle_DOF/thys/Isa_COL.thy index 522f991..efceb50 100644 --- a/Isabelle_DOF/thys/Isa_COL.thy +++ b/Isabelle_DOF/thys/Isa_COL.thy @@ -24,9 +24,9 @@ text\ Building a fundamental infrastructure for common document elements s theory Isa_COL imports Isa_DOF keywords "title*" "subtitle*" - "chapter*" "section*" "paragraph*" - "subsection*" "subsubsection*" "figure*" "listing*" "frame*" :: document_body + and "chapter*" "section*" "subsection*" + "subsubsection*" "paragraph*" "subparagraph*" :: document_heading begin @@ -58,7 +58,8 @@ doc_class "subsubsection" = text_element + level :: "int option" <= "Some 3" doc_class "paragraph" = text_element + level :: "int option" <= "Some 4" - +doc_class "subparagraph" = text_element + + level :: "int option" <= "Some 5" subsection\Ontological Macros\ @@ -128,19 +129,22 @@ fun enriched_document_cmd_exp ncid (S: (string * string) list) = end; end (* local *) - fun heading_command (name, pos) descr level = Monitor_Command_Parser.document_command (name, pos) descr {markdown = false, body = true} (enriched_text_element_cmd level) [] I; -val _ = heading_command \<^command_keyword>\title*\ "section heading" NONE; -val _ = heading_command \<^command_keyword>\subtitle*\ "section heading" NONE; -val _ = heading_command \<^command_keyword>\chapter*\ "section heading" (SOME (SOME 0)); -val _ = heading_command \<^command_keyword>\section*\ "section heading" (SOME (SOME 1)); -val _ = heading_command \<^command_keyword>\subsection*\ "subsection heading" (SOME (SOME 2)); -val _ = heading_command \<^command_keyword>\subsubsection*\ "subsubsection heading" (SOME (SOME 3)); -val _ = heading_command \<^command_keyword>\paragraph*\ "paragraph" (SOME (SOME 4)); +fun heading_command' (name, pos) descr level = + Monitor_Command_Parser.document_command (name, pos) descr + {markdown = false, body = false} (enriched_text_element_cmd level) [] I; +val _ = heading_command \<^command_keyword>\title*\ "title heading" NONE; +val _ = heading_command \<^command_keyword>\subtitle*\ "subtitle heading" NONE; +val _ = heading_command' \<^command_keyword>\chapter*\ "chapter heading" (SOME (SOME 0)); +val _ = heading_command' \<^command_keyword>\section*\ "section heading" (SOME (SOME 1)); +val _ = heading_command' \<^command_keyword>\subsection*\ "subsection heading" (SOME (SOME 2)); +val _ = heading_command' \<^command_keyword>\subsubsection*\ "subsubsection heading" (SOME (SOME 3)); +val _ = heading_command' \<^command_keyword>\paragraph*\ "paragraph heading" (SOME (SOME 4)); +val _ = heading_command' \<^command_keyword>\subparagraph*\ "subparagraph heading" (SOME (SOME 5)); end end diff --git a/Isabelle_DOF/thys/Isa_DOF.thy b/Isabelle_DOF/thys/Isa_DOF.thy index cbbe561..30a4975 100644 --- a/Isabelle_DOF/thys/Isa_DOF.thy +++ b/Isabelle_DOF/thys/Isa_DOF.thy @@ -2309,24 +2309,60 @@ fun gen_enriched_document_cmd' {inline} cid_transform attr_transform (* markup reports and document output *) +val headings = + ["chapter", + "section", + "subsection", + "subsubsection", + "paragraph", + "subparagraph"] + +val headings_star = headings |> map (suffix "*") + (* {markdown = true} sets the parsing process such that in the text-core markdown elements are accepted. *) -fun document_output {markdown: bool, markup: Latex.text -> Latex.text} sem_attrs transform_attr meta_args text ctxt = +(*fun document_output body {markdown: bool, markup: Latex.text -> Latex.text} sem_attrs transform_attr meta_args text ctxt = let val thy = Proof_Context.theory_of ctxt; val _ = Context_Position.reports ctxt (Document_Output.document_reports text); val output_meta = meta_args_2_latex thy sem_attrs transform_attr meta_args; val output_text = Document_Output.output_document ctxt {markdown = markdown} text; - in markup (output_meta @ output_text) end; + in if body + then markup (output_meta @ output_text) + else markup output_text + end*) fun document_output_reports name {markdown, body} sem_attrs transform_attr meta_args text ctxt = let - fun markup xml = - let val m = if body then Markup.latex_body else Markup.latex_heading - in [XML.Elem (m (Latex.output_name name), xml)] end; - val config = {markdown = markdown, markup = markup} - in document_output config sem_attrs transform_attr meta_args text ctxt + val thy = Proof_Context.theory_of ctxt; + val ((binding, cid_opt), _) = meta_args + fun headings_markup thy name binding m xml = + let val label = Binding.name_of binding + |> (fn n => DOF_core.get_instance_name_global n thy) + |> DOF_core.output_name + |> Latex.string + |> Latex.macro "label" + in [XML.Elem (m (Latex.output_name name), label @ xml)] end + val _ = Context_Position.reports ctxt (Document_Output.document_reports text); + val output_meta = meta_args_2_latex thy sem_attrs transform_attr meta_args; + val output_text = Document_Output.output_document ctxt {markdown = markdown} text; + in if body + then (case cid_opt of + NONE => let fun markup xml = [XML.Elem (Markup.latex_body name, xml)] + in markup (output_meta @ output_text) end + | SOME x => let val cid = fst x + in if headings |> map (Syntax.read_typ ctxt) + |> exists (Syntax.read_typ ctxt cid |> equal) + then headings_markup thy cid binding Markup.latex_heading output_text + else + let fun markup xml = [XML.Elem (Markup.latex_body name, xml)] + in markup (output_meta @ output_text) end + end) + else if headings_star |> exists (equal name) + then headings_markup thy (name |> translate_string (fn "*" => "" | s => s)) binding + Markup.latex_heading output_text + else headings_markup thy name binding Markup.latex_heading output_text end;