forked from Isabelle_DOF/Isabelle_DOF
Merge branch 'master' of git.logicalhacking.com:HOL-OCL/Isabelle_DOF
This commit is contained in:
commit
9a1bec2d85
149
Isa_DOF.thy
149
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
|
||||
|
@ -55,7 +56,7 @@ fun docref_markup_gen refN def name id pos =
|
|||
if id = 0 then Markup.empty
|
||||
else
|
||||
Markup.properties (Position.entity_properties_of def id pos)
|
||||
(Markup.entity refN name); (* or better store the thy-name as property ? ? ? *)
|
||||
(Markup.entity refN name); (* or better store the thy-name as property ? ? ? *)
|
||||
|
||||
val docref_markup = docref_markup_gen docrefN
|
||||
|
||||
|
@ -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
|
||||
end;
|
||||
in
|
||||
warning("LaTeX Style file generation not supported.")
|
||||
(* write_file thy ("Isa-DOF."^curr_thy_name^".template.sty") content *)
|
||||
end
|
||||
|
||||
|
||||
val _ =
|
||||
|
@ -923,6 +928,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>
|
||||
|
@ -947,7 +954,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')
|
||||
|
@ -959,9 +966,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
|
||||
val ctxt = Proof_Context.init_global thy
|
||||
val term = (Syntax.check_term ctxt o Syntax.parse_term ctxt) s
|
||||
fun ltx_of_markup ctxt s = let
|
||||
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:
|
||||
|
@ -977,12 +983,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))
|
||||
(* no normalization on lhs (could be long-name)
|
||||
no paraphrasing on rhs (could be fully paranthesized
|
||||
pretty-printed formula in LaTeX notation ... *)
|
||||
in
|
||||
(enclose "[" "]" (String.concat [ cid_txt, ", args={", (commas ([cid_txt,l] @ (map str attr_list ))), "}"]))
|
||||
val ctxt = Proof_Context.init_global thy
|
||||
val actual_args = map (fn ((lhs,_),rhs) => (toLong lhs, ltx_of_markup ctxt rhs))
|
||||
attr_list
|
||||
val default_args = map (fn (b,_,t) => (toLong (Long_Name.base_name ( Sign.full_name thy b)), ltx_of_term ctxt t))
|
||||
(DOF_core.get_attribute_defaults cid_long thy)
|
||||
|
||||
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.$$$ ";");
|
||||
|
@ -1513,7 +1525,7 @@ val docitem_modes = Scan.optional (Args.parens (Args.$$$ defineN || Args.$$$ unc
|
|||
else {unchecked = true, define= false}))
|
||||
{unchecked = false, define= false} (* default *);
|
||||
|
||||
val docitem_antiquotation_parser = (Scan.lift (docitem_modes -- Args.cartouche_input))
|
||||
val docitem_antiquotation_parser = (Scan.lift (docitem_modes -- Args.text_input))
|
||||
|
||||
fun docitem_antiquotation_generic cid_decl
|
||||
{context = ctxt, source = src:Token.src, state}
|
||||
|
@ -1775,31 +1787,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
|
||||
|
|
|
@ -16,63 +16,4 @@
|
|||
[0000/00/00 Unreleased v0.0.0+%
|
||||
Document-Type Support Framework for Isabelle (CENELEC 50128).]
|
||||
|
||||
\RequirePackage{DOF-core}
|
||||
|
||||
|
||||
\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}%
|
||||
}
|
||||
\RequirePackage{DOF-COL}
|
||||
|
|
|
@ -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*
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
@ -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]{%
|
||||
\csname isaDof.\commandkey{env}.\commandkey{type}\endcsname[label=\commandkey{label},\commandkey{args}]{#1}%
|
||||
}
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
% begin: newcommand wrapper
|
||||
\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
|
||||
\expandafter\newkeycommand\csname isaDof.text.text\endcsname%
|
||||
[label=,type=%
|
||||
][1]{%
|
||||
% begin: generic dispatcher
|
||||
\newkeycommand+[\|]\isaDof[env={UNKNOWN},label=,type={dummyT},args={}][1]{%
|
||||
\ifcsname isaDof.\commandkey{type}\endcsname%
|
||||
\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*
|
||||
\NewEnviron{isamarkupfigure*}[1][]{\isaDof[env={figure},#1]{\BODY}}
|
||||
\expandafter\newkeycommand\csname isaDof.figure.Isa_COL.figure\endcsname%
|
||||
[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}
|
||||
% begin: chapter/section default implementations
|
||||
\newisadof{chapter}[label=,type=][1]{%
|
||||
\isamarkupfalse\isamarkupchapter{#1}\label{\commandkey{label}}\isamarkuptrue%
|
||||
}
|
||||
% end: figure*
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
|
||||
|
||||
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
% 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}
|
||||
\newisadof{section}[label=,type=][1]{%
|
||||
\isamarkupfalse\isamarkupsection{#1}\label{\commandkey{label}}\isamarkuptrue%
|
||||
}
|
||||
% 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*
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
|
|
|
@ -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}
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
|
||||
|
|
|
@ -14,7 +14,7 @@ section*[a::A, x = "3"] \<open> Lorem ipsum dolor sit amet, ... \<close>
|
|||
text*[c1::C, x = "''beta''"] \<open> ... suspendisse non arcu malesuada mollis, nibh morbi, ... \<close>
|
||||
|
||||
text*[d::D, a1 = "X3"] \<open> ... phasellus amet id massa nunc, pede suscipit repellendus,
|
||||
... @{docitem \<open>c1\<close>} @{thm "refl"}\<close>
|
||||
... @{docitem c1} @{thm "refl"}\<close>
|
||||
|
||||
|
||||
update_instance*[d::D, a1 := X2]
|
||||
|
@ -35,12 +35,13 @@ text\<open> ..., mauris amet, id elit aliquam aptent id, ... @{docitem \<open>a
|
|||
text\<open>Here we add and maintain a link that is actually modeled as m-to-n relation ...\<close>
|
||||
update_instance*[f::F,b:="{(@{docitem ''a''}::A,@{docitem ''c1''}::C),
|
||||
(@{docitem ''a''}, @{docitem ''c2''})}"]
|
||||
|
||||
|
||||
close_monitor*[struct]
|
||||
|
||||
text\<open>And the trace of the monitor is:\<close>
|
||||
ML\<open>@{trace_attribute struct}\<close>
|
||||
|
||||
|
||||
print_doc_classes
|
||||
print_doc_items
|
||||
|
||||
|
|
|
@ -9,7 +9,7 @@ open_monitor*[this::report]
|
|||
|
||||
title*[tit::title]\<open>An Account with my Personal, Ecclectic Comments on the Isabelle Architecture\<close>
|
||||
subtitle*[stit::subtitle]\<open>Version : Isabelle 2017\<close>
|
||||
text*[bu::author,
|
||||
text*[bu::author,
|
||||
email = "''wolff@lri.fr''",
|
||||
affiliation = "''Universit\\'e Paris-Saclay, Paris, France''"]\<open>Burkhart Wolff\<close>
|
||||
|
||||
|
@ -845,6 +845,8 @@ end;
|
|||
*)
|
||||
\<close>
|
||||
|
||||
|
||||
|
||||
|
||||
ML\<open> Thy_Output.document_command {markdown = true} \<close>
|
||||
(* Structures related to LaTeX Generation *)
|
||||
|
@ -1158,15 +1160,68 @@ ML\<open> fun dark_matter x = XML.content_of (YXML.parse_body x)\<close>
|
|||
|
||||
(* MORE TO COME *)
|
||||
|
||||
section\<open>Positions\<close>
|
||||
text\<open>A basic data-structure relevant for PIDE are \<^emph>\<open>positions\<close>; beyond the usual line- and column
|
||||
information they can represent ranges, list of ranges, and the name of the atomic sub-document
|
||||
in which they are contained. In the command:\<close>
|
||||
ML\<open>
|
||||
val pos = @{here};
|
||||
val markup = Position.here pos;
|
||||
writeln ("And a link to the declaration of 'here' is "^markup)
|
||||
\<close>
|
||||
(* \<^here> *)
|
||||
text\<open> ... uses the antiquotation @{ML "@{here}"} to infer from the system lexer the actual position
|
||||
of itself in the global document, converts it to markup (a string-representation of it) and sends
|
||||
it via the usual @{ML "writeln"} to the interface. \<close>
|
||||
|
||||
figure*[hyplinkout::figure,relative_width="40",src="''figures/markup-demo''"]
|
||||
\<open>Output with hyperlinked position.\<close>
|
||||
|
||||
text\<open>@{docitem \<open>hyplinkout\<close>} shows the produced output where the little house-like symbol in the
|
||||
display is hyperlinked to the position of @{ML "@{here}"} in the ML sample above.\<close>
|
||||
|
||||
section\<open>Markup and Low-level Markup Reporting\<close>
|
||||
text\<open>The structures @{ML_structure Markup} and @{ML_structure Properties} represent the basic
|
||||
annotation data which is part of the protocol sent from Isabelle to the frontend.
|
||||
They are qualified as "quasi-abstract", which means they are intended to be an abstraction of
|
||||
the serialized, textual presentation of the protocol. Markups are structurally a pair of a key
|
||||
and properties; @{ML_structure Markup} provides a number of of such \<^emph>\<open>key\<close>s for annotation classes
|
||||
such as "constant", "fixed", "cartouche", some of them quite obscure. Here is a code sample
|
||||
from \<^theory_text>\<open>Isabelle_DOF\<close>. A markup must be tagged with an id; this is done by the @{ML serial}-function
|
||||
discussed earlier.\<close>
|
||||
ML\<open>
|
||||
local
|
||||
|
||||
val docclassN = "doc_class";
|
||||
|
||||
(* derived from: theory_markup; def for "defining occurrence" (true) in contrast to
|
||||
"referring occurence" (false). *)
|
||||
fun docclass_markup def name id pos =
|
||||
if id = 0 then Markup.empty
|
||||
else Markup.properties (Position.entity_properties_of def id pos)
|
||||
(Markup.entity docclassN name);
|
||||
|
||||
in
|
||||
|
||||
fun report_defining_occurrence pos cid =
|
||||
let val id = serial ()
|
||||
val markup_of_cid = docclass_markup true cid id pos
|
||||
in Position.report pos markup_of_cid end;
|
||||
|
||||
end
|
||||
\<close>
|
||||
|
||||
text\<open>The @\<open>ML report_defining_occurrence\<close>-function above takes a position and a "cid" parsed
|
||||
in the Front-End, converts this into markup together with a unique number identifying this
|
||||
markup, and sends this as a report to the Front-End. \<close>
|
||||
|
||||
section\<open>Low-level Markup Reporting\<close>
|
||||
|
||||
section\<open>Environment Structured Reporting\<close>
|
||||
|
||||
text\<open> @{ML_type "'a Name_Space.table"} \<close>
|
||||
|
||||
section\<open> Parsing issues \<close>
|
||||
|
||||
|
||||
text\<open> Parsing combinators represent the ground building blocks of both generic input engines
|
||||
as well as the specific Isar framework. They are implemented in the structure \verb+Token+
|
||||
providing core type \verb+Token.T+.
|
||||
|
|
|
@ -7,6 +7,7 @@ session "TR_mycommentedisabelle" = "Isabelle_DOF" +
|
|||
"preamble.tex"
|
||||
"prooftree.sty"
|
||||
"build"
|
||||
"figures/markup-demo"
|
||||
"figures/text-element.pdf"
|
||||
"figures/isabelle-architecture.pdf"
|
||||
"figures/pure-inferences-I.pdf"
|
||||
|
|
Binary file not shown.
After Width: | Height: | Size: 13 KiB |
|
@ -239,7 +239,7 @@ datatype role = PM (* Program Manager *)
|
|||
| DES (* Designer *)
|
||||
| IMP (* Implementer *)
|
||||
| ASR (* Assessor *)
|
||||
| INT (* Integrator *)
|
||||
| INT (* Integrator *)
|
||||
| TST (* Tester *)
|
||||
| VER (* Verifier *)
|
||||
| VnV (* Verification and Validation *)
|
||||
|
|
|
@ -99,7 +99,7 @@ text \<open>underlying idea: a monitor class automatically receives a
|
|||
|
||||
doc_class article =
|
||||
style_id :: string <= "''LNCS''"
|
||||
accepts "(title ~~ \<lbrace>author\<rbrace>\<^sup>+ ~~ abstract ~~
|
||||
accepts "(title ~~ \<lbrace>author\<rbrace>\<^sup>+ ~~ abstract ~~
|
||||
\<lbrace>introduction\<rbrace>\<^sup>+ ~~ \<lbrace>technical || example\<rbrace>\<^sup>+ ~~ \<lbrace>conclusion\<rbrace>\<^sup>+)"
|
||||
|
||||
|
||||
|
@ -158,7 +158,6 @@ setup\<open> let val cidS = ["small_math.introduction","small_math.technical", "
|
|||
|
||||
|
||||
|
||||
|
||||
gen_sty_template
|
||||
|
||||
|
||||
|
|
Loading…
Reference in New Issue