Theory Isa_COL
chapter ‹The Document Ontology Common Library for the Isabelle Ontology Framework›
text‹ Building a fundamental infrastructure for common document elements such as
Structuring Text-Elements (the top classes), Figures, (Tables yet todo)
The COL provides a number of ontological "macros" like "section*" which
automatically set a number of class-attributes in particular ways without
user-interference.
›
theory Isa_COL
imports Isa_DOF
keywords "title*" "subtitle*"
"chapter*" "section*" "paragraph*"
"subsection*" "subsubsection*"
"figure*" "listing*" "frame*" :: document_body
begin
section‹Basic Text and Text-Structuring Elements›
text‹ The attribute @{term "level"} in the subsequent enables doc-notation support section* etc.
we follow LaTeX terminology on levels
▸ part = Some -1
▸ chapter = Some 0
▸ section = Some 1
▸ subsection = Some 2
▸ subsubsection = Some 3
▸ ...
for scholarly paper: invariant level > 0. ›
doc_class text_element =
level :: "int option" <= "None"
referentiable :: bool <= "False"
variants :: "String.literal set" <= "{STR ''outline'', STR ''document''}"
doc_class "chapter" = text_element +
level :: "int option" <= "Some 0"
doc_class "section" = text_element +
level :: "int option" <= "Some 1"
doc_class "subsection" = text_element +
level :: "int option" <= "Some 2"
doc_class "subsubsection" = text_element +
level :: "int option" <= "Some 3"
doc_class "paragraph" = text_element +
level :: "int option" <= "Some 4"
subsection‹Ontological Macros›
ML‹
structure Onto_Macros =
struct
local open ODL_Meta_Args_Parser in
fun enriched_text_element_cmd level =
let fun transform doc_attrs = case level of
NONE => doc_attrs
| SOME(NONE) => (("level",@{here}),"None")::doc_attrs
| SOME(SOME x) => (("level",@{here}),"Some("^ Int.toString x ^"::int)")::doc_attrs
in Monitor_Command_Parser.gen_enriched_document_cmd {inline=true} I transform end;
local
fun transform_cid _ NONE X = X
|transform_cid _ (SOME ncid) NONE = (SOME(ncid,@{here}))
|transform_cid thy (SOME cid) (SOME (sub_cid,pos)) =
let val cid_long = DOF_core.get_onto_class_name_global' cid thy
val sub_cid_long = DOF_core.get_onto_class_name_global' sub_cid thy
in if DOF_core.is_subclass_global thy sub_cid_long cid_long
then (SOME (sub_cid,pos))
else
error("class "^sub_cid_long^
" must be sub-class of "^cid_long)
end
in
fun transform_attr S doc_attrs =
let
fun transform_attr' [] doc_attrs = doc_attrs
| transform_attr' (s::S) (doc_attrs) =
let val (name', value) = s
val doc_attrs' = doc_attrs
|> map (fn (name, term) => if name = name'
then (name, value)
else (name, term))
in if doc_attrs' = doc_attrs
then transform_attr' S doc_attrs' |> cons (name', value)
else transform_attr' S doc_attrs'
end
in transform_attr' S doc_attrs end
fun enriched_formal_statement_command ncid (S: (string * string) list) =
let fun transform_attr doc_attrs = (map (fn(cat,tag) => ((cat,@{here}),tag)) S) @
(("formal_results",@{here}),"([]::thm list)")::doc_attrs
in fn margs => fn thy =>
Monitor_Command_Parser.gen_enriched_document_cmd {inline=true}
(transform_cid thy ncid) transform_attr margs thy
end;
fun enriched_document_cmd_exp ncid (S: (string * string) list) =
let fun transform_attr attrs = (map (fn(cat,tag) => ((cat,@{here}),tag)) S) @ attrs
in fn margs => fn thy =>
Monitor_Command_Parser.gen_enriched_document_cmd {inline=true} (transform_cid thy ncid)
transform_attr margs thy
end;
end
fun heading_command (name, pos) descr level =
Monitor_Command_Parser.document_command (name, pos) descr
{markdown = false, body = true} (enriched_text_element_cmd level) [] I;
val _ = heading_command \<^command_keyword>‹title*› "section heading" NONE;
val _ = heading_command \<^command_keyword>‹subtitle*› "section heading" NONE;
val _ = heading_command \<^command_keyword>‹chapter*› "section heading" (SOME (SOME 0));
val _ = heading_command \<^command_keyword>‹section*› "section heading" (SOME (SOME 1));
val _ = heading_command \<^command_keyword>‹subsection*› "subsection heading" (SOME (SOME 2));
val _ = heading_command \<^command_keyword>‹subsubsection*› "subsubsection heading" (SOME (SOME 3));
val _ = heading_command \<^command_keyword>‹paragraph*› "paragraph" (SOME (SOME 4));
end
end
›
section‹Layout Trimming Commands (with syntactic checks)›
ML‹
local
val scan_cm = Scan.ahead (Basic_Symbol_Pos.$$$ "c" |-- Basic_Symbol_Pos.$$$ "m" ) ;
val scan_pt = Scan.ahead (Basic_Symbol_Pos.$$$ "p" |-- Basic_Symbol_Pos.$$$ "t" ) ;
val scan_blank = Scan.repeat ( Basic_Symbol_Pos.$$$ " "
|| Basic_Symbol_Pos.$$$ "\t"
|| Basic_Symbol_Pos.$$$ "\n");
in
val scan_latex_measure = (scan_blank
|-- Scan.option (Basic_Symbol_Pos.$$$ "-")
|-- Symbol_Pos.scan_nat
|-- (Scan.option ((Basic_Symbol_Pos.$$$ ".") |-- Symbol_Pos.scan_nat))
|-- scan_blank
|-- (scan_cm || scan_pt)
|-- scan_blank
) ;
fun check_latex_measure _ src =
let val _ = ((Scan.catch scan_latex_measure (Symbol_Pos.explode(Input.source_content src)))
handle Fail _ => error ("syntax error in LaTeX measure") )
in () end
val parse_latex_measure = Parse.embedded_input >> (fn src => (check_latex_measure () src;
(fst o Input.source_content) src ) )
end›
setup‹ DOF_lib.define_macro \<^binding>‹vs› "\\vspace{" "}" (check_latex_measure) ›
setup‹ DOF_lib.define_macro \<^binding>‹hs› "\\hspace{" "}" (check_latex_measure) ›
define_shortcut* hfill ⇌ ‹\hfill›
text‹Tests: \<^vs>‹-0.14cm››
ML‹ check_latex_measure @{context} (Input.string "-0.14 cm") ›
define_macro* vs2 ⇌ ‹\vspace{› _ ‹}› (check_latex_measure)
define_macro* hs2 ⇌ ‹\hspace{› _ ‹}›
define_shortcut* clearpage ⇌ ‹\clearpage{}›
hf ⇌ ‹\hfill›
br ⇌ ‹\break›
section‹ Library of Standard Figure Ontology ›