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

Implement chapter*, section*, etc. latex generation in SML
ci/woodpecker/push/build Pipeline failed Details

This commit is contained in:
Nicolas Méric 2023-09-22 08:38:50 +02:00
parent 7b54bf5ca5
commit 0ce9e6f2d0
4 changed files with 80 additions and 39 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
Isabelle_DOF-Ontologies/Conceptual/Conceptual.thy
View File

@ -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", "Conceptual.E", "Conceptual.F", "Conceptual.G", "Conceptual.M",
"Isa_COL.float", "Isa_COL.frame", "Isa_COL.figure", "Isa_COL.chapter", "Isa_COL.float", "Isa_COL.frame", "Isa_COL.figure", "Isa_COL.chapter",
"Isa_COL.listing", "Isa_COL.section", "Isa_COL.paragraph", "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>)); val docclass_tab = map fst (Name_Space.dest_table (DOF_core.get_onto_classes \<^context>));
in @{assert} (class_ids_so_far = docclass_tab) end\<close> in @{assert} (class_ids_so_far = docclass_tab) end\<close>

40
Isabelle_DOF/latex/styles/DOF-core.sty
View File

@ -94,31 +94,31 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% begin: chapter*-dispatcher % begin: chapter*-dispatcher
\NewEnviron{isamarkupchapter*}[1][]{\isaDof[env={IsaUNDERSCORECOLDOTchapter},#1]{\BODY}} %\NewEnviron{isamarkupchapter*}[1][]{\isaDof[env={IsaUNDERSCORECOLDOTchapter},#1]{\BODY}}
% end: chapter*-dispatcher % end: chapter*-dispatcher
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% begin: section*-dispatcher % begin: section*-dispatcher
\NewEnviron{isamarkupsection*}[1][]{\isaDof[env={IsaUNDERSCORECOLDOTsection},#1]{\BODY}} %\NewEnviron{isamarkupsection*}[1][]{\isaDof[env={IsaUNDERSCORECOLDOTsection},#1]{\BODY}}
% end: section*-dispatcher % end: section*-dispatcher
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% begin: subsection*-dispatcher % begin: subsection*-dispatcher
\NewEnviron{isamarkupsubsection*}[1][]{\isaDof[env={IsaUNDERSCORECOLDOTsubsection},#1]{\BODY}} %\NewEnviron{isamarkupsubsection*}[1][]{\isaDof[env={IsaUNDERSCORECOLDOTsubsection},#1]{\BODY}}
% end: subsection*-dispatcher % end: subsection*-dispatcher
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% begin: subsubsection*-dispatcher % begin: subsubsection*-dispatcher
\NewEnviron{isamarkupsubsubsection*}[1][]{\isaDof[env={IsaUNDERSCORECOLDOTsubsubsection},#1]{\BODY}} %\NewEnviron{isamarkupsubsubsection*}[1][]{\isaDof[env={IsaUNDERSCORECOLDOTsubsubsection},#1]{\BODY}}
% end: subsubsection*-dispatcher % end: subsubsection*-dispatcher
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% begin: paragraph*-dispatcher % begin: paragraph*-dispatcher
\NewEnviron{isamarkupparagraph*}[1][]{\isaDof[env={IsaUNDERSCORECOLDOTparagraph},#1]{\BODY}} %\NewEnviron{isamarkupparagraph*}[1][]{\isaDof[env={IsaUNDERSCORECOLDOTparagraph},#1]{\BODY}}
% end: paragraph*-dispatcher % end: paragraph*-dispatcher
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@ -135,21 +135,21 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% begin: chapter/section default implementations % begin: chapter/section default implementations
\newisadof{IsaUNDERSCORECOLDOTchapter}[label=,type=,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTlevel=, IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTreferentiable=,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTvariants=][1]{% %\newisadof{IsaUNDERSCORECOLDOTchapter}[label=,type=,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTlevel=, IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTreferentiable=,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTvariants=][1]{%
\isamarkupfalse\isamarkupchapter{#1}\label{\commandkey{label}}\isamarkuptrue% % \isamarkupfalse\isamarkupchapter{#1}\label{\commandkey{label}}\isamarkuptrue%
} %}
\newisadof{IsaUNDERSCORECOLDOTsection}[label=,type=,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTlevel=, IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTreferentiable=,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTvariants=][1]{% %\newisadof{IsaUNDERSCORECOLDOTsection}[label=,type=,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTlevel=, IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTreferentiable=,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTvariants=][1]{%
\isamarkupfalse\isamarkupsection{#1}\label{\commandkey{label}}\isamarkuptrue% % \isamarkupfalse\isamarkupsection{#1}\label{\commandkey{label}}\isamarkuptrue%
} %}
\newisadof{IsaUNDERSCORECOLDOTsubsection}[label=,type=,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTlevel=, IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTreferentiable=,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTvariants=][1]{% %\newisadof{IsaUNDERSCORECOLDOTsubsection}[label=,type=,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTlevel=, IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTreferentiable=,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTvariants=][1]{%
\isamarkupfalse\isamarkupsubsection{#1}\label{\commandkey{label}}\isamarkuptrue% % \isamarkupfalse\isamarkupsubsection{#1}\label{\commandkey{label}}\isamarkuptrue%
} %}
\newisadof{IsaUNDERSCORECOLDOTsubsubsection}[label=,type=,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTlevel=, IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTreferentiable=,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTvariants=][1]{% %\newisadof{IsaUNDERSCORECOLDOTsubsubsection}[label=,type=,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTlevel=, IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTreferentiable=,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTvariants=][1]{%
\isamarkupfalse\isamarkupsubsubsection{#1}\label{\commandkey{label}}\isamarkuptrue% % \isamarkupfalse\isamarkupsubsubsection{#1}\label{\commandkey{label}}\isamarkuptrue%
} %}
\newisadof{IsaUNDERSCORECOLDOTparagraph}[label=,type=,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTlevel=, IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTreferentiable=,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTvariants=][1]{% %\newisadof{IsaUNDERSCORECOLDOTparagraph}[label=,type=,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTlevel=, IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTreferentiable=,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTvariants=][1]{%
\isamarkupfalse\isamarkupparagraph{#1}\label{\commandkey{label}}\isamarkuptrue% % \isamarkupfalse\isamarkupparagraph{#1}\label{\commandkey{label}}\isamarkuptrue%
} %}
% end: chapter/section default implementations % end: chapter/section default implementations
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

26
Isabelle_DOF/thys/Isa_COL.thy
View File

@ -24,9 +24,9 @@ text\<open> Building a fundamental infrastructure for common document elements s
theory Isa_COL theory Isa_COL
imports Isa_DOF imports Isa_DOF
keywords "title*" "subtitle*" keywords "title*" "subtitle*"
"chapter*" "section*" "paragraph*"
"subsection*" "subsubsection*"
"figure*" "listing*" "frame*" :: document_body "figure*" "listing*" "frame*" :: document_body
and "chapter*" "section*" "subsection*"
"subsubsection*" "paragraph*" "subparagraph*" :: document_heading
begin begin
@ -58,7 +58,8 @@ doc_class "subsubsection" = text_element +
level :: "int option" <= "Some 3" level :: "int option" <= "Some 3"
doc_class "paragraph" = text_element + doc_class "paragraph" = text_element +
level :: "int option" <= "Some 4" level :: "int option" <= "Some 4"
doc_class "subparagraph" = text_element +
level :: "int option" <= "Some 5"
subsection\<open>Ontological Macros\<close> subsection\<open>Ontological Macros\<close>
@ -128,19 +129,22 @@ fun enriched_document_cmd_exp ncid (S: (string * string) list) =
end; end;
end (* local *) end (* local *)
fun heading_command (name, pos) descr level = fun heading_command (name, pos) descr level =
Monitor_Command_Parser.document_command (name, pos) descr Monitor_Command_Parser.document_command (name, pos) descr
{markdown = false, body = true} (enriched_text_element_cmd level) [] I; {markdown = false, body = true} (enriched_text_element_cmd level) [] I;
val _ = heading_command \<^command_keyword>\<open>title*\<close> "section heading" NONE; fun heading_command' (name, pos) descr level =
val _ = heading_command \<^command_keyword>\<open>subtitle*\<close> "section heading" NONE; Monitor_Command_Parser.document_command (name, pos) descr
val _ = heading_command \<^command_keyword>\<open>chapter*\<close> "section heading" (SOME (SOME 0)); {markdown = false, body = false} (enriched_text_element_cmd level) [] I;
val _ = heading_command \<^command_keyword>\<open>section*\<close> "section heading" (SOME (SOME 1));
val _ = heading_command \<^command_keyword>\<open>subsection*\<close> "subsection heading" (SOME (SOME 2));
val _ = heading_command \<^command_keyword>\<open>subsubsection*\<close> "subsubsection heading" (SOME (SOME 3));
val _ = heading_command \<^command_keyword>\<open>paragraph*\<close> "paragraph" (SOME (SOME 4));
val _ = heading_command \<^command_keyword>\<open>title*\<close> "title heading" NONE;
val _ = heading_command \<^command_keyword>\<open>subtitle*\<close> "subtitle heading" NONE;
val _ = heading_command' \<^command_keyword>\<open>chapter*\<close> "chapter heading" (SOME (SOME 0));
val _ = heading_command' \<^command_keyword>\<open>section*\<close> "section heading" (SOME (SOME 1));
val _ = heading_command' \<^command_keyword>\<open>subsection*\<close> "subsection heading" (SOME (SOME 2));
val _ = heading_command' \<^command_keyword>\<open>subsubsection*\<close> "subsubsection heading" (SOME (SOME 3));
val _ = heading_command' \<^command_keyword>\<open>paragraph*\<close> "paragraph heading" (SOME (SOME 4));
val _ = heading_command' \<^command_keyword>\<open>subparagraph*\<close> "subparagraph heading" (SOME (SOME 5));
end end
end end

50
Isabelle_DOF/thys/Isa_DOF.thy
View File

@ -2309,24 +2309,60 @@ fun gen_enriched_document_cmd' {inline} cid_transform attr_transform
(* markup reports and document output *) (* 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 = true} sets the parsing process such that in the text-core
markdown elements are accepted. *) 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 let
val thy = Proof_Context.theory_of ctxt; val thy = Proof_Context.theory_of ctxt;
val _ = Context_Position.reports ctxt (Document_Output.document_reports text); 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_meta = meta_args_2_latex thy sem_attrs transform_attr meta_args;
val output_text = Document_Output.output_document ctxt {markdown = markdown} text; 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 = fun document_output_reports name {markdown, body} sem_attrs transform_attr meta_args text ctxt =
let let
fun markup xml = val thy = Proof_Context.theory_of ctxt;
let val m = if body then Markup.latex_body else Markup.latex_heading val ((binding, cid_opt), _) = meta_args
in [XML.Elem (m (Latex.output_name name), xml)] end; fun headings_markup thy name binding m xml =
val config = {markdown = markdown, markup = markup} let val label = Binding.name_of binding
in document_output config sem_attrs transform_attr meta_args text ctxt |> (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; end;