Merge branch 'master' of https://git.logicalhacking.com/HOL-OCL/Isabelle_DOF

Isa_DOF.thy

@@ -13,7 +13,8 @@ text\<open> Offering
 \<^item> LaTeX support. \<close> 
   
 text\<open> In this section, we develop on the basis of a management of references Isar-markups
-that provide direct support in the PIDE framework. \<close>  
+that provide direct support in the PIDE framework. \<close> 
+
   
 theory Isa_DOF                (* Isabelle Document Ontology Framework *)
   imports  Main  
@@ -636,46 +637,6 @@ val _ =
       Toplevel.keep (check_doc_global b o Toplevel.context_of)));
 
 
-fun toStringLaTeXNewKeyCommand env long_name =
-    "\\expandafter\\newkeycommand\\csname"^" "^"isaDof."^env^"."^long_name^"\\endcsname%\n" 
-
-fun toStringMetaArgs true attr_long_names = 
-       enclose "[" "][1]" (commas ("label=,type=%\n" :: attr_long_names))
-   |toStringMetaArgs false attr_long_names = 
-       enclose "[" "][1]" (commas attr_long_names) 
-
-fun toStringDocItemBody env =
-    enclose "{%\n\\isamarkupfalse\\isamarkup" 
-            "{#1}\\label{\\commandkey{label}}\\isamarkuptrue%\n}\n"
-            env
-            
-fun toStringDocItemCommand env long_name attr_long_names = 
-    toStringLaTeXNewKeyCommand env long_name ^
-    toStringMetaArgs true attr_long_names ^
-    toStringDocItemBody env ^"\n"
-
-fun toStringDocItemLabel long_name attr_long_names = 
-    toStringLaTeXNewKeyCommand "Label" long_name ^
-    toStringMetaArgs false attr_long_names ^
-    "{%\n\\autoref{#1}\n}\n"
-
-fun toStringDocItemRef long_name label attr_long_namesNvalues = 
-    "\\isaDof.Label." ^ long_name ^
-    enclose "[" "]" (commas attr_long_namesNvalues) ^
-    enclose "{" "}" label
-
-fun write_file thy filename content =
-    let 
-       val filename = Path.explode filename
-       val master_dir = Resources.master_directory thy
-       val abs_filename = if (Path.is_absolute filename) 
-                          then filename 
-                          else Path.append master_dir filename
-    in
-      File.write (abs_filename) content
-      handle (IO.Io{name=name,...}) 
-             => warning ("Could not write \""^(name)^"\".")
-    end
 
 fun write_ontology_latex_sty_template thy = 
     let 
@@ -688,6 +649,48 @@ fun write_ontology_latex_sty_template thy =
         *)
         val curr_thy_name = Context.theory_name thy
         val {docobj_tab={tab = x, ...},docclass_tab,...}= get_data_global thy;
+
+        fun toStringLaTeXNewKeyCommand env long_name =
+            "\\expandafter\\newkeycommand\\csname"^" "^"isaDof."^env^"."^long_name^"\\endcsname%\n" 
+        
+        fun toStringMetaArgs true attr_long_names = 
+               enclose "[" "][1]" (commas ("label=,type=%\n" :: attr_long_names))
+           |toStringMetaArgs false attr_long_names = 
+               enclose "[" "][1]" (commas attr_long_names) 
+        
+        fun toStringDocItemBody env =
+            enclose "{%\n\\isamarkupfalse\\isamarkup" 
+                    "{#1}\\label{\\commandkey{label}}\\isamarkuptrue%\n}\n"
+                    env
+                    
+        fun toStringDocItemCommand env long_name attr_long_names = 
+            toStringLaTeXNewKeyCommand env long_name ^
+            toStringMetaArgs true attr_long_names ^
+            toStringDocItemBody env ^"\n"
+        
+        fun toStringDocItemLabel long_name attr_long_names = 
+            toStringLaTeXNewKeyCommand "Label" long_name ^
+            toStringMetaArgs false attr_long_names ^
+            "{%\n\\autoref{#1}\n}\n"
+        
+        fun toStringDocItemRef long_name label attr_long_namesNvalues = 
+            "\\isaDof.Label." ^ long_name ^
+            enclose "[" "]" (commas attr_long_namesNvalues) ^
+            enclose "{" "}" label
+        
+        fun write_file thy filename content =
+            let 
+               val filename = Path.explode filename
+               val master_dir = Resources.master_directory thy
+               val abs_filename = if (Path.is_absolute filename) 
+                                  then filename 
+                                  else Path.append master_dir filename
+            in
+              File.write (abs_filename) content
+              handle (IO.Io{name=name,...}) 
+                     => warning ("Could not write \""^(name)^"\".")
+            end
+
         fun  write_attr (n, ty, _) = YXML.content_of(Binding.print n)^ "=\n"
 
         fun write_class (n, {attribute_decl,id,inherits_from,name,params,thy_name,rex,rejectS}) =
@@ -699,8 +702,10 @@ fun write_ontology_latex_sty_template thy =
             else ""
         val content = String.concat(map write_class (Symtab.dest docclass_tab))
         (* val _ = writeln content  -- for interactive testing only, breaks LaTeX compilation *) 
-    in  write_file thy ("Isa-DOF."^curr_thy_name^".template.sty") content
+    in 
-    end;
+        warning("LaTeX Style file  generation not supported.")
+        (*  write_file thy ("Isa-DOF."^curr_thy_name^".template.sty") content *)
+    end
 
 
 val _ =
@@ -844,6 +849,8 @@ fun property_list_dest ctxt X = (map (fn Const ("Isa_DOF.ISA_term", _) $ s => HO
 end; (* struct *)
                                                             
 \<close>
+
+
 subsection\<open> Isar - Setup\<close>
 
 setup\<open>DOF_core.update_isa_global("typ"      ,ISA_core.ML_isa_check_typ) \<close>     
@@ -868,7 +875,7 @@ fun meta_args_2_string thy ((((lab, _), cid_opt), attr_list) : meta_args_t) =
     let val l   = "label = "^ (enclose "{" "}" lab)
         val cid_long = case cid_opt of
                                 NONE => DOF_core.default_cid
-                              | SOME(cid,_) => DOF_core.name2doc_class_name thy cid
+                              | SOME(cid,_) => DOF_core.name2doc_class_name thy cid        
         val cid_txt  = "type = " ^ (enclose "{" "}" cid_long);
 
         fun ltx_of_term _ (((Const ("List.list.Cons", t1) $  (Const ("String.Char", t2 ) $ t))) $ t') 
@@ -880,9 +887,8 @@ fun meta_args_2_string thy ((((lab, _), cid_opt), attr_list) : meta_args_t) =
                                                                          )
           | ltx_of_term ctxt t = ""^(Sledgehammer_Util.hackish_string_of_term ctxt t)
         fun markup2string s = String.concat (List.filter (fn c => c <> Symbol.DEL) (Symbol.explode (YXML.content_of s))) 
-        fun ltx_of_markup s = let
+        fun ltx_of_markup ctxt s = let
-                                val ctxt = Proof_Context.init_global thy
+  	                            val term = (Syntax.check_term ctxt o Syntax.parse_term ctxt) s
-		                            val term = (Syntax.check_term ctxt o Syntax.parse_term ctxt) s
                                 val str_of_term = ltx_of_term  ctxt term 
                                     handle _ => "Exception in ltx_of_term"
                                 (* For debugging: 
@@ -898,12 +904,18 @@ fun meta_args_2_string thy ((((lab, _), cid_opt), attr_list) : meta_args_t) =
                               end 
         fun toLong n =  #long_name(the(DOF_core.get_attribute_info cid_long (markup2string n) thy))
 
-        fun str ((lhs,_),rhs) = (toLong lhs)^" = "^(enclose "{" "}" (ltx_of_markup rhs))  
+        val ctxt = Proof_Context.init_global thy
-                                (* no normalization on lhs (could be long-name)
+        val actual_args =  map (fn ((lhs,_),rhs) => (toLong lhs, ltx_of_markup ctxt rhs))
-                                   no paraphrasing on rhs (could be fully paranthesized
+                               attr_list  
-                                   pretty-printed formula in LaTeX notation ... *)
+	      val default_args = map (fn (b,_,t) => (toLong (Long_Name.base_name ( Sign.full_name thy b)), ltx_of_term ctxt t))
-    in  
+                               (DOF_core.get_attribute_defaults cid_long thy)
-      (enclose "[" "]" (String.concat [ cid_txt, ", args={", (commas ([cid_txt,l] @ (map str  attr_list ))), "}"])) 
+
+        val default_args_filtered = filter (fn (a,_) => not (exists (fn b => b = a) 
+                                    (map (fn (c,_) => c) actual_args))) default_args
+        val str_args = map (fn (lhs,rhs) => lhs^" = "^(enclose "{" "}" rhs)) 
+                      (actual_args@default_args_filtered)
+    in
+      (enclose "[" "]" (String.concat [ cid_txt, ", args={", (commas str_args), "}"])) 
 end
 
 val semi = Scan.option (Parse.$$$ ";");
@@ -1696,31 +1708,4 @@ val _ =
 end (* struct *)
 \<close>  
 
-
-section\<open> Testing and Validation \<close>
-  
-(* the f ollowing test crashes the LaTeX generation - however, without the latter this output is 
-   instructive 
-ML\<open>
-writeln (DOF_core.toStringDocItemCommand "section" "scholarly_paper.introduction" []);
-writeln (DOF_core.toStringDocItemLabel "scholarly_paper.introduction" []);
-writeln (DOF_core.toStringDocItemRef "scholarly_paper.introduction" "XX" []);
-
-(DOF_core.write_ontology_latex_sty_template @{theory})
-\<close>
-*)
-
-
-ML\<open>
-
-\<close>
-(*
-ML\<open>
-val h = bstring_to_holstring @{context} (Syntax.string_of_term @{context} @{term "A \<longrightarrow> A"});
-holstring_to_bstring @{context} h
-\<close>
-*)
-
-
-
 end

document-generator/latex/DOF-CENELEC_50128.sty

@@ -16,63 +16,4 @@
   [0000/00/00 Unreleased v0.0.0+%
   Document-Type Support Framework for Isabelle (CENELEC 50128).]
 
-\RequirePackage{DOF-core}
+\RequirePackage{DOF-COL}
-
-
-\newkeycommand\isaDofSectionRequirement[label=,type=,main_author=,long_name=][1]{%
-  \isamarkupfalse\isamarkupsection{#1}\label{\commandkey{label}}\isamarkuptrue%
-}
-
-\newkeycommand\isaDofSubSectionRequirement[label=,type=,main_author=,long_name=][1]{%
-  \isamarkupfalse\isamarkupsection{#1}\label{\commandkey{label}}\isamarkuptrue%
-}
-
-\newkeycommand\isaDofSectionInterface[label=,type=,main_author=,kind=][1]{%
-  \isamarkupfalse\isamarkupsection{#1}\label{\commandkey{label}}\isamarkuptrue%
-}
-
-
-\newkeycommand\isaDofTextEc[label=,type=,assumption=][1]{%
-  \begin{isamarkuptext}%
-      #1
-  \end{isamarkuptext}%
-}
-
-\newkeycommand\isaDofTextSrac[label=,type=,assumption=][1]{%
-  \begin{isamarkuptext}%
-      #1
-  \end{isamarkuptext}%
-}
-
-\expandafter\newkeycommand\csname isaDof.text.CENELEC_50128.assumption\endcsname%
-[label=,type=,assumption=][1]{%
-  \begin{isamarkuptext}%
-      #1
-  \end{isamarkuptext}%
-}
-
-\expandafter\newkeycommand\csname isaDof.text.CENELEC_50128.hypothesis\endcsname%
-[label=,type=,assumption=][1]{%
-  \begin{isamarkuptext}%
-      #1
-  \end{isamarkuptext}%
-}
-
-\expandafter\newkeycommand\csname isaDof.text.CENELEC_50128.srac\endcsname%
-[label=,type=,assumption=][1]{%
-  \begin{isamarkuptext}%
-      #1
-  \end{isamarkuptext}%
-}
-\expandafter\newkeycommand\csname isaDof.text.CENELEC_50128.ec\endcsname%
-[label=,type=,assumption=][1]{%
-  \begin{isamarkuptext}%
-      #1
-  \end{isamarkuptext}%
-}
-\expandafter\newkeycommand\csname isaDof.text.CENELEC_50128.test_result\endcsname%
-[label=,type=,assumption=][1]{%
-  \begin{isamarkuptext}%
-      #1
-  \end{isamarkuptext}%
-}

document-generator/latex/DOF-COL.sty

@@ -0,0 +1,97 @@
+%% Copyright (C) 2018 The University of Sheffield
+%%               2018 The University of Paris-Sud
+%%
+%% License:
+%%   This program can be redistributed and/or modified under the terms
+%%   of the LaTeX Project Public License Distributed from CTAN
+%%   archives in directory macros/latex/base/lppl.txt; either
+%%   version 1 of the License, or any later version.
+%%   OR
+%%   The 2-clause BSD-style license.
+%%  
+%%   SPDX-License-Identifier: LPPL-1.0+ OR BSD-2-Clause
+
+\NeedsTeXFormat{LaTeX2e}\relax
+\ProvidesPackage{DOF-COL}
+  [0000/00/00 Unreleased v0.0.0+%
+  Document-Type Support Framework for Isabelle.]
+
+\RequirePackage{DOF-core}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% begin: figure*
+\NewEnviron{isamarkupfigure*}[1][]{\isaDof[env={figure},#1]{\BODY}}
+\newisadof{figure.Isa_COL.figure}%
+[label=,type=%
+,Isa_COL.figure.relative_width=%
+,Isa_COL.figure.placement=%
+,Isa_COL.figure.src=%
+,Isa_COL.figure.spawn_columns=enum False True%
+][1]{%
+  \begin{figure}[]
+    \centering
+    \ifcommandkey{Isa_COL.figure.relative_width}
+    {%
+      \gdef\dof@width{\commandkey{Isa_COL.figure.relative_width}}
+      \gdef\dof@src{\commandkey{Isa_COL.figure.src}}
+      \FPdiv\scale{\dof@width}{100}%
+      \includegraphics[width=\scale\textwidth]{\dof@src}%
+    }{%
+      \gdef\dof@src{\commandkey{Isa_COL.figure.src}}
+      \includegraphics[]{\dof@src}%
+    } 
+    \caption{#1}\label{\commandkey{label}}%
+  \end{figure}
+}
+% end: figure*
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% begin: side_by_side_figure*
+\NewEnviron{isamarkupside_by_side_figure*}[1][]{\isaDof[env={side_by_side_figure},#1]{\BODY}}
+\newisadof{side_by_side_figure.Isa_COL.side_by_side_figure}%
+[label=,type=%
+,Isa_COL.figure.relative_width=%
+,Isa_COL.figure.src=%
+,Isa_COL.side_by_side_figure.anchor=%
+,Isa_COL.side_by_side_figure.caption=%
+,Isa_COL.side_by_side_figure.relative_width2=%
+,Isa_COL.side_by_side_figure.src2=%
+,Isa_COL.side_by_side_figure.anchor2=%
+,Isa_COL.side_by_side_figure.caption2=%
+,Isa_COL.side_by_side_figure.placement=%
+,Isa_COL.figure.spawn_columns=enum False True%
+][1]{%
+  \begin{figure}[]
+    \subfloat[\label{\commandkey{Isa_COL.side_by_side_figure.anchor}}\commandkey{Isa_COL.side_by_side_figure.caption}]%
+      {\ifcommandkey{Isa_COL.figure.relative_width}%
+       {%
+          \gdef\dof@width{\commandkey{Isa_COL.figure.relative_width}}
+          \gdef\dof@src{\commandkey{Isa_COL.figure.src}}
+          \FPdiv\scale{\dof@width}{100}%
+          \includegraphics[width=\scale\textwidth]{\dof@src}%
+        }{%
+          \gdef\dof@src{\commandkey{Isa_COL.figure.src}}
+          \includegraphics[]{\dof@src}%
+        }% 
+      }%
+      \hfill%
+      \subfloat[\label{\commandkey{Isa_COL.side_by_side_figure.anchor2}}\commandkey{Isa_COL.side_by_side_figure.caption2}]%
+      {\ifcommandkey{Isa_COL.side_by_side_figure.relative_width2}%
+        {%
+          \gdef\dof@width{\commandkey{Isa_COL.side_by_side_figure.relative_width2}}
+          \gdef\dof@src{\commandkey{Isa_COL.side_by_side_figure.src2}}
+          \FPdiv\scale{\dof@width}{100}%
+          \includegraphics[width=\scale\textwidth]{\dof@src}%
+        }{%
+          \gdef\dof@src{\commandkey{Isa_COL.side_by_side_figure.src2}}
+          \includegraphics[]{\dof@src}%
+        }% 
+      }%
+    \caption{#1}\label{\commandkey{label}}%
+  \end{figure}
+}
+% end: side_by_side_figure*
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

document-generator/latex/DOF-core.sty

@@ -20,137 +20,109 @@
 \RequirePackage{environ}
 \RequirePackage{graphicx}
 \RequirePackage{xspace}
+\RequirePackage{etoolbox}
 \RequirePackage{fp}
 
 \newcommand{\isadof}{Isabelle/DOF\xspace}
 
-% Generic dispatcher
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\newkeycommand+[\|]\isaDof[env={UNKNOWN},label=,type={dummyT},args={}][1]{%
+% begin: newcommand wrapper
-\csname isaDof.\commandkey{env}.\commandkey{type}\endcsname[label=\commandkey{label},\commandkey{args}]{#1}%
+\newcommand\newisadof[1]{\expandafter\newkeycommand\csname isaDof.#1\endcsname}%
-}
+\newcommand\renewisadof[1]{\expandafter\renewkeycommand\csname isaDof.#1\endcsname}%
+\newcommand\provideisadof[1]{\expandafter\providekeycommand\csname isaDof.#1\endcsname}%
+% end: newcommand wrapper
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% begin: text.text
+% begin: generic dispatcher
-\expandafter\newkeycommand\csname isaDof.text.text\endcsname%
+\newkeycommand+[\|]\isaDof[env={UNKNOWN},label=,type={dummyT},args={}][1]{%
-[label=,type=%
+  \ifcsname isaDof.\commandkey{type}\endcsname%
-][1]{%
+      \csname isaDof.\commandkey{type}\endcsname%
+              [label=\commandkey{label},\commandkey{args}]{#1}%
+  \else\relax\fi%
+  \ifcsname isaDof.\commandkey{env}.\commandkey{type}\endcsname%
+      \csname isaDof.\commandkey{env}.\commandkey{type}\endcsname%
+              [label=\commandkey{label},\commandkey{args}]{#1}%
+  \else%
+      \message{Isabelle/DOF: Using default LaTeX representation for concept %
+        "\commandkey{env}.\commandkey{type}".}%
+      \ifcsname isaDof.\commandkey{env}\endcsname%
+         \csname isaDof.\commandkey{env}\endcsname%
+                [label=\commandkey{label}]{#1}%
+      \else%
+      \errmessage{Isabelle/DOF: No LaTeX representation for concept %
+        "\commandkey{env}.\commandkey{type}" defined and no default %
+        definition for "\commandkey{env}" available either.}%
+      \fi%
+  \fi%
+}
+% end: generic dispatcher
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% begin: text*-dispatcher
+\NewEnviron{isamarkuptext*}[1][]{\isaDof[env={text},#1]{\BODY}}
+% end: text*-dispatcher
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% begin: chapter*-dispatcher
+\NewEnviron{isamarkupchapter*}[1][]{\isaDof[env={chapter},#1]{\BODY}}
+% end: chapter*-dispatcher
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% begin: section*-dispatcher
+\NewEnviron{isamarkupsection*}[1][]{\isaDof[env={section},#1]{\BODY}}
+% end: section*-dispatcher
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% begin: subsection*-dispatcher
+\NewEnviron{isamarkupsubsection*}[1][]{\isaDof[env={subsection},#1]{\BODY}}
+% end: subsection*-dispatcher
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% begin: subsubsection*-dispatcher
+\NewEnviron{isamarkupsubsubsection*}[1][]{\isaDof[env={subsubsection},#1]{\BODY}}
+% end: subsubsection*-dispatcher
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% begin: paragraph*-dispatcher
+\NewEnviron{isamarkupparagraph*}[1][]{\isaDof[env={paragraph},#1]{\BODY}}
+% end: paragraph*-dispatcher
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% begin: text default implementation
+\newisadof{text}[label=,type=][1]{%
   \begin{isamarkuptext}%
     #1
   \end{isamarkuptext}%
 }
-% begin: text.text
+% end: text default implementation
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% begin: figure*
+% begin: chapter/section default implementations
-\NewEnviron{isamarkupfigure*}[1][]{\isaDof[env={figure},#1]{\BODY}}
+\newisadof{chapter}[label=,type=][1]{%
-\expandafter\newkeycommand\csname isaDof.figure.Isa_COL.figure\endcsname%
+  \isamarkupfalse\isamarkupchapter{#1}\label{\commandkey{label}}\isamarkuptrue%
-[label=,type=%
-,Isa_COL.figure.relative_width=%
-,Isa_COL.figure.placement=%
-,Isa_COL.figure.src=%
-,Isa_COL.figure.spawn_columns=enum False True%
-][1]{%
-  \begin{figure}[]
-    \centering
-    \ifcommandkey{Isa_COL.figure.relative_width}
-    {%
-      \gdef\dof@width{\commandkey{Isa_COL.figure.relative_width}}
-      \gdef\dof@src{\commandkey{Isa_COL.figure.src}}
-      \FPdiv\scale{\dof@width}{100}%
-      \includegraphics[width=\scale\textwidth]{\dof@src}%
-    }{%
-      \gdef\dof@src{\commandkey{Isa_COL.figure.src}}
-      \includegraphics[]{\dof@src}%
-    } 
-    \caption{#1}\label{\commandkey{label}}%
-  \end{figure}
 }
-% end: figure*
+\newisadof{section}[label=,type=][1]{%
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \isamarkupfalse\isamarkupsection{#1}\label{\commandkey{label}}\isamarkuptrue%
-
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% begin: side_by_side_figure*
-\NewEnviron{isamarkupside_by_side_figure*}[1][]{\isaDof[env={side_by_side_figure},#1]{\BODY}}
-\expandafter\newkeycommand\csname isaDof.side_by_side_figure.Isa_COL.side_by_side_figure\endcsname%
-[label=,type=%
-,Isa_COL.figure.relative_width=%
-,Isa_COL.figure.src=%
-,Isa_COL.side_by_side_figure.anchor=%
-,Isa_COL.side_by_side_figure.caption=%
-,Isa_COL.side_by_side_figure.relative_width2=%
-,Isa_COL.side_by_side_figure.src2=%
-,Isa_COL.side_by_side_figure.anchor2=%
-,Isa_COL.side_by_side_figure.caption2=%
-,Isa_COL.side_by_side_figure.placement=%
-,Isa_COL.side_by_side_figure.spawn_columns=enum False True%
-][1]{%
-  \begin{figure}[]
-    \subfloat[\label{\commandkey{Isa_COL.side_by_side_figure.anchor}}\commandkey{Isa_COL.side_by_side_figure.caption}]%
-      {\ifcommandkey{Isa_COL.figure.relative_width}%
-       {%
-          \gdef\dof@width{\commandkey{Isa_COL.figure.relative_width}}
-          \gdef\dof@src{\commandkey{Isa_COL.figure.src}}
-          \FPdiv\scale{\dof@width}{100}%
-          \includegraphics[width=\scale\textwidth]{\dof@src}%
-        }{%
-          \gdef\dof@src{\commandkey{Isa_COL.figure.src}}
-          \includegraphics[]{\dof@src}%
-        }% 
-      }%
-      \hfill%
-      \subfloat[\label{\commandkey{Isa_COL.side_by_side_figure.anchor2}}\commandkey{Isa_COL.side_by_side_figure.caption2}]%
-      {\ifcommandkey{Isa_COL.side_by_side_figure.relative_width2}%
-        {%
-          \gdef\dof@width{\commandkey{Isa_COL.side_by_side_figure.relative_width2}}
-          \gdef\dof@src{\commandkey{Isa_COL.side_by_side_figure.src2}}
-          \FPdiv\scale{\dof@width}{100}%
-          \includegraphics[width=\scale\textwidth]{\dof@src}%
-        }{%
-          \gdef\dof@src{\commandkey{Isa_COL.side_by_side_figure.src2}}
-          \includegraphics[]{\dof@src}%
-        }% 
-      }%
-    \caption{#1}\label{\commandkey{label}}%
-  \end{figure}
 }
-% end: side_by_side_figure*
+\newisadof{subsection}[label=,type=][1]{%
+  \isamarkupfalse\isamarkupsubsection{#1}\label{\commandkey{label}}\isamarkuptrue%
+}
+\newisadof{subsubsection}[label=,type=][1]{%
+  \isamarkupfalse\isamarkupsubsubsection{#1}\label{\commandkey{label}}\isamarkuptrue%
+}
+\newisadof{paragraph}[label=,type=][1]{%
+  \isamarkupfalse\isamarkupparagraph{#1}\label{\commandkey{label}}\isamarkuptrue%
+}
+% end: chapter/section default implementations
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% begin: Text*
-\NewEnviron{isamarkupText*}[1][]{\isaDof[env={Text},#1]{\BODY}}
-% end: Text*
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% begin: text*
-\NewEnviron{isamarkuptext*}[1][]{\isaDof[env={text},#1]{\BODY}}
-% end: text*
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-\newkeycommand\isaDofOpenMonitor[label=,type=]{}
-\newkeycommand\isaDofCloseMonitor[label=,type=]{}
-
-\newkeycommand\isaDofDeclareReferenceTextSection[label=,type=]{}
-\newkeycommand\isaDofDeclareReferenceFigure[label=,type=]{}
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% begin: chapter*
-\NewEnviron{isamarkupchapter*}[1][]{\isaDof[env={chapter},#1]{\BODY}}
-% end: chapter*
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% begin: section*
-\NewEnviron{isamarkupsection*}[1][]{\isaDof[env={section},#1]{\BODY}}
-% end: section*
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% begin: subsection*
-\NewEnviron{isamarkupsubsection*}[1][]{\isaDof[env={subsection},#1]{\BODY}}
-% end: subsection*
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

document-generator/latex/DOF-mathex.sty

@@ -16,7 +16,7 @@
   [0000/00/00 Unreleased v0.0.0+%
   Document-Type Support Framework for math classes.]
 
-\RequirePackage{DOF-core}
+\RequirePackage{DOF-COL}
 \usepackage{sfmath}
 \usepackage{amsmath}
 \usepackage{lastpage}

document-generator/latex/DOF-scholarly_paper.sty

@@ -16,7 +16,7 @@
   [0000/00/00 Unreleased v0.0.0+%
   Document-Type Support Framework for Isabelle (LNCS).]
 
-\RequirePackage{DOF-core}
+\RequirePackage{DOF-COL}
 \RequirePackage{ifthen}
 
 \RequirePackage{ifthen}
@@ -52,9 +52,9 @@
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % begin: title*
 \NewEnviron{isamarkuptitle*}[1][]{\isaDof[env={title},#1]{\BODY}}
-\expandafter\newkeycommand\csname isaDof.title.scholarly_paper.title\endcsname%
+\newisadof{title.scholarly_paper.title}%
 [label=,type=%
-,keywordlist=%
+,scholarly_paper.title.short_title=%
 ][1]{%
   \immediate\write\@auxout{\noexpand\title{#1}}%
 }
@@ -64,9 +64,9 @@
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % begin: subtitle*
 \NewEnviron{isamarkupsubtitle*}[1][]{\isaDof[env={subtitle},#1]{\BODY}}
-\expandafter\newkeycommand\csname isaDof.subtitle.scholarly_paper.subtitle\endcsname%
+\newisadof{subtitle.scholarly_paper.subtitle}%
 [label=,type=%
-,keywordlist=%
+,scholarly_paper.subtitle.abbrev=%
 ][1]{%
   \immediate\write\@auxout{\noexpand\subtitle{#1}}%
 }
@@ -106,11 +106,12 @@
   }
 }
 
-\expandafter\providekeycommand\csname isaDof.text.scholarly_paper.author\endcsname%
+\provideisadof{text.scholarly_paper.author}%
 [label=,type=%
 ,scholarly_paper.author.email=%
 ,scholarly_paper.author.affiliation=%
 ,scholarly_paper.author.orcid=%
+,scholarly_paper.author.http_site=%
 ][1]{%
   \stepcounter{dof@cnt@author}
   \def\dof@a{\commandkey{scholarly_paper.author.affiliation}}
@@ -127,7 +128,7 @@
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % begin: scholarly_paper.abstract
 \providecommand{\keywords}[1]{\mbox{}\\\medskip\noindent{\textbf{Keywords:}} #1}
-\expandafter\newkeycommand\csname isaDof.text.scholarly_paper.abstract\endcsname%
+\newisadof{text.scholarly_paper.abstract}%
 [label=,type=%
 ,scholarly_paper.abstract.keywordlist=%
 ][1]{%
@@ -142,124 +143,3 @@
 }
 % end: scholarly_paper.abstract
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% begin: scholarly_paper.introduction
-\expandafter\newkeycommand\csname isaDof.section.scholarly_paper.introduction\endcsname%
-[label=,type=%
-,scholarly_paper.introduction.main_author=%
-,scholarly_paper.introduction.fixme_list=%
-][1]{%
-  \isamarkupfalse\isamarkupsection{#1}\label{\commandkey{label}}\isamarkuptrue%
-}
-\expandafter\newkeycommand\csname isaDof.subsection.scholarly_paper.introduction\endcsname%
-[label=,type=%
-,scholarly_paper.introduction.main_author=%
-,scholarly_paper.introduction.fixme_list=%
-][1]{%
-  \isamarkupfalse\isamarkupsubsection{#1}\label{\commandkey{label}}\isamarkuptrue%
-}
-\expandafter\newkeycommand\csname isaDof.text.scholarly_paper.introduction_elem\endcsname%
-[label=,type=%
-,scholarly_paper.introduction.main_author=%
-,scholarly_paper.introduction.fixme_list=%
-][1]{%
-  \begin{isamarkuptext}%
-    #1
-  \end{isamarkuptext}%
-}
-\expandafter\newkeycommand\csname isaDof.text.scholarly_paper.introduction\endcsname%
-[label=,type=%
-,scholarly_paper.introduction.main_author=%
-,scholarly_paper.introduction.fixme_list=%
-][1]{%
-  \begin{isamarkuptext}%
-    #1
-  \end{isamarkuptext}%
-}
-% end: scholarly_paper.introduction
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% begin: scholarly_paper.introduction
-\expandafter\newkeycommand\csname isaDof.section.scholarly_paper.text_section\endcsname%
-[label=,type=%
-,scholarly_paper.text_section.main_author=%
-,scholarly_paper.text_section.fixme_list=%
-][1]{%
-  \isamarkupfalse\isamarkupsection{#1}\label{\commandkey{label}}\isamarkuptrue%
-}
-% end: scholarly_paper.introduction
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% begin: scholarly_paper.technical
-\expandafter\newkeycommand\csname isaDof.section.scholarly_paper.technical\endcsname%
-[label=,type=%
-,scholarly_paper.text_section.main_author=%
-,scholarly_paper.text_section.fixme_list=%
-][1]{%
-  \isamarkupfalse\isamarkupsection{#1}\label{\commandkey{label}}\isamarkuptrue%
-}
-\expandafter\newkeycommand\csname isaDof.subsection.scholarly_paper.technical\endcsname%
-[label=,type=%
-,scholarly_paper.text_section.main_author=%
-,scholarly_paper.text_section.fixme_list=%
-][1]{%
-  \isamarkupfalse\isamarkupsubsection{#1}\label{\commandkey{label}}\isamarkuptrue%
-}
-% end: scholarly_paper.technical
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% begin: scholarly_paper.example
-\expandafter\newkeycommand\csname isaDof.section.scholarly_paper.example\endcsname%
-[label=,type=%
-,scholarly_paper.text_section.main_author=%
-,scholarly_paper.text_section.fixme_list=%
-][1]{%
-  \isamarkupfalse\isamarkupsection{#1}\label{\commandkey{label}}\isamarkuptrue%
-}
-\expandafter\newkeycommand\csname isaDof.subsection.scholarly_paper.example\endcsname%
-[label=,type=%
-,scholarly_paper.text_section.main_author=%
-,scholarly_paper.text_section.fixme_list=%
-][1]{%
-  \isamarkupfalse\isamarkupsubsection{#1}\label{\commandkey{label}}\isamarkuptrue%
-}
-% end: scholarly_paper.example
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% begin: scholarly_paper.conclusion
-\expandafter\newkeycommand\csname isaDof.section.scholarly_paper.conclusion\endcsname%
-[label=,type=%
-,scholarly_paper.text_section.main_author=%
-,scholarly_paper.text_section.fixme_list=%
-][1]{%
-  \isamarkupfalse\isamarkupsection{#1}\label{\commandkey{label}}\isamarkuptrue%
-}
-% end: scholarly_paper.conclusion
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% begin: scholarly_paper.conclusion
-\expandafter\newkeycommand\csname isaDof.subsection.scholarly_paper.conclusion\endcsname%
-[label=,type=%
-,scholarly_paper.text_section.main_author=%
-,scholarly_paper.text_section.fixme_list=%
-][1]{%
-  \isamarkupfalse\isamarkupsection{#1}\label{\commandkey{label}}\isamarkuptrue%
-}
-% end: scholarly_paper.conclusion
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% begin: scholarly_paper.bibliography
-\expandafter\newkeycommand\csname isaDof.section.scholarly_paper.bibliography\endcsname%
-[label=,type=%
-,scholarly_paper.text_section.main_author=%
-,scholarly_paper.text_section.fixme_list=%
-][1]{%
-  \isamarkupfalse\isamarkupsection{#1}\label{\commandkey{label}}\isamarkuptrue%
-}
-% end: scholarly_paper.bibliography

document-generator/latex/DOF-technical_report.sty

@@ -28,65 +28,3 @@
   }{%
     {\PackageError{DOF-scholarly_paper}{Scholarly Paper only supports LNCS or scrartcl as document class.}{}\stop}%
   }
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% begin: scholarly_paper.introduction
-\expandafter\newkeycommand\csname isaDof.chapter.scholarly_paper.introduction\endcsname%
-[label=,type=%
-,scholarly_paper.introduction.main_author=%
-,scholarly_paper.introduction.fixme_list=%
-][1]{%
-  \isamarkupfalse\isamarkupchapter{#1}\label{\commandkey{label}}\isamarkuptrue%
-}
-% end: scholarly_paper.introduction
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% begin: scholarly_paper.introduction
-\expandafter\newkeycommand\csname isaDof.chapter.scholarly_paper.text_section\endcsname%
-[label=,type=%
-,scholarly_paper.text_section.main_author=%
-,scholarly_paper.text_section.fixme_list=%
-][1]{%
-  \isamarkupfalse\isamarkupchapter{#1}\label{\commandkey{label}}\isamarkuptrue%
-}
-% end: scholarly_paper.introduction
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% begin: scholarly_paper.technical
-\expandafter\newkeycommand\csname isaDof.chapter.scholarly_paper.technical\endcsname%
-[label=,type=%
-,scholarly_paper.text_section.main_author=%
-,scholarly_paper.text_section.fixme_list=%
-][1]{%
-  \isamarkupfalse\isamarkupchapter{#1}\label{\commandkey{label}}\isamarkuptrue%
-}
-% end: scholarly_paper.technical
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% begin: scholarly_paper.example
-\expandafter\newkeycommand\csname isaDof.chapter.scholarly_paper.example\endcsname%
-[label=,type=%
-,scholarly_paper.text_section.main_author=%
-,scholarly_paper.text_section.fixme_list=%
-][1]{%
-  \isamarkupfalse\isamarkupchapter{#1}\label{\commandkey{label}}\isamarkuptrue%
-}
-% end: scholarly_paper.example
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% begin: scholarly_paper.conclusion
-\expandafter\newkeycommand\csname isaDof.chapter.scholarly_paper.conclusion\endcsname%
-[label=,type=%
-,scholarly_paper.text_section.main_author=%
-,scholarly_paper.text_section.fixme_list=%
-][1]{%
-  \isamarkupfalse\isamarkupchapter{#1}\label{\commandkey{label}}\isamarkuptrue%
-}
-% end: scholarly_paper.conclusion
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-