Compare commits
1 Commits
main
...
sml-latex-
Author | SHA1 | Date |
---|---|---|
Nicolas Méric | 0ce9e6f2d0 |
|
@ -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\<close>
|
||||
|
||||
|
|
|
@ -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
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
|
||||
|
|
|
@ -24,9 +24,9 @@ text\<open> 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\<open>Ontological Macros\<close>
|
||||
|
||||
|
@ -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>\<open>title*\<close> "section heading" NONE;
|
||||
val _ = heading_command \<^command_keyword>\<open>subtitle*\<close> "section heading" NONE;
|
||||
val _ = heading_command \<^command_keyword>\<open>chapter*\<close> "section 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" (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>\<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
|
||||
|
|
|
@ -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;
|
||||
|
||||
|
||||
|
|
Loading…
Reference in New Issue