From af9e399f50d4efe4a6fe69a1c98bd2addcb5775f Mon Sep 17 00:00:00 2001 From: bu Date: Tue, 23 Jun 2020 11:22:33 +0200 Subject: [PATCH] some experiments with OoOP and the code support presentations. --- .../Isabelle_DOF-Manual/05_Implementation.thy | 17 +- .../technical_report/Isabelle_DOF-Manual/ROOT | 2 +- .../scholarly_paper/scholarly_paper.thy | 26 -- .../technical_report/DOF-technical_report.sty | 5 + .../technical_report/technical_report.thy | 279 ++++++++++++++++++ src/tests/OutOfOrderPresntn.thy | 24 +- 6 files changed, 320 insertions(+), 33 deletions(-) diff --git a/examples/technical_report/Isabelle_DOF-Manual/05_Implementation.thy b/examples/technical_report/Isabelle_DOF-Manual/05_Implementation.thy index 26106081..af2f6be1 100644 --- a/examples/technical_report/Isabelle_DOF-Manual/05_Implementation.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/05_Implementation.thy @@ -41,8 +41,23 @@ text\ IDE support. \ +(* should be text* *) +text +\ + +\begin{sml} +structure Data = Generic_Data +( type T = docobj_tab * docclass_tab * ... + val empty = (initial_docobj_tab, initial_docclass_tab, ...) + val extend = I + fun merge((d1,c1,...),(d2,c2,...)) = (merge_docobj_tab (d1,d2,...), + merge_docclass_tab(c1,c2,...)) +); +\end{sml} +\ + section\\isadof: A User-Defined Plugin in Isabelle/Isar\ -text\ +text\ A plugin in Isabelle starts with defining the local data and registering it in the framework. As mentioned before, contexts are structures with independent cells/compartments having three primitives \inlinesml+init+, \inlinesml+extend+ and \inlinesml+merge+. Technically this is done by diff --git a/examples/technical_report/Isabelle_DOF-Manual/ROOT b/examples/technical_report/Isabelle_DOF-Manual/ROOT index 23fdf8d1..999c6c3e 100644 --- a/examples/technical_report/Isabelle_DOF-Manual/ROOT +++ b/examples/technical_report/Isabelle_DOF-Manual/ROOT @@ -8,7 +8,7 @@ session "Isabelle_DOF-Manual" = "Isabelle_DOF" + "root.mst" "preamble.tex" "build" - "lstisadof-manual.sty" + "lstisadof-manual.sty" "figures/antiquotations-PIDE.png" "figures/cicm2018-combined.png" "figures/cicm2018-dof.png" diff --git a/src/ontologies/scholarly_paper/scholarly_paper.thy b/src/ontologies/scholarly_paper/scholarly_paper.thy index 92aa2534..36fea4ad 100644 --- a/src/ontologies/scholarly_paper/scholarly_paper.thy +++ b/src/ontologies/scholarly_paper/scholarly_paper.thy @@ -267,32 +267,6 @@ doc_class tech_example = technical + referentiable :: bool <= True tag :: "string" <= "''''" -subsection\Code Statement Elements\ - -doc_class "code" = technical + - checked :: bool <= "False" - tag :: "string" <= "''''" - -text\The @{doc_class "code"} is a general stub for free-form and type-checked code-fragments -such as: -\<^enum> SML code -\<^enum> bash code -\<^enum> isar code (although this might be an unwanted concurrence to the Isabelle standard cartouche) -\<^enum> C code. - -it is intended that later refinements of this "stub" as done in \<^verbatim>\Isabelle_C\ which come with their -own content checking and, of course, presentation styles. -\ - - -doc_class "SML" = code + - checked :: bool <= "False" - -doc_class "ISAR" = code + - checked :: bool <= "False" - -doc_class "LATEX" = code + - checked :: bool <= "False" diff --git a/src/ontologies/technical_report/DOF-technical_report.sty b/src/ontologies/technical_report/DOF-technical_report.sty index 84b9420b..0a5838b2 100644 --- a/src/ontologies/technical_report/DOF-technical_report.sty +++ b/src/ontologies/technical_report/DOF-technical_report.sty @@ -28,3 +28,8 @@ }{% {\PackageError{DOF-technical_report}{Technical Report only supports scrreprt as document class.}{}\stop}% } + +% Code-Setups : or RequirePackage ? +% \usepackage{xcolor} +% \usepackage{lstisadof-manual} + diff --git a/src/ontologies/technical_report/technical_report.thy b/src/ontologies/technical_report/technical_report.thy index 4af8900c..61e801f2 100644 --- a/src/ontologies/technical_report/technical_report.thy +++ b/src/ontologies/technical_report/technical_report.thy @@ -19,6 +19,8 @@ begin (* for reports paper: invariant: level \ -1 *) +section\More Global Text Elements for Reports\ + doc_class table_of_contents = bookmark_depth :: int <= 3 depth :: int <= 3 @@ -30,6 +32,35 @@ doc_class index = kind :: "doc_class" level :: "int option" +section\Code Statement Elements\ + +doc_class "code" = technical + + checked :: bool <= "False" + caption :: "string" <= "''''" + + +text\The @{doc_class "code"} is a general stub for free-form and type-checked code-fragments +such as: +\<^enum> SML code +\<^enum> bash code +\<^enum> isar code (although this might be an unwanted concurrence to the Isabelle standard cartouche) +\<^enum> C code. + +it is intended that later refinements of this "stub" as done in \<^verbatim>\Isabelle_C\ which come with their +own content checking and, of course, presentation styles. +\ + +doc_class "SML" = code + + checked :: bool <= "False" + +doc_class "ISAR" = code + + checked :: bool <= "False" + +doc_class "LATEX" = code + + checked :: bool <= "False" + + + doc_class report = style_id :: string <= "''LNCS''" version :: "(int \ int \ int)" <= "(0,0,0)" @@ -45,5 +76,253 @@ doc_class report = \index\\<^sup>* ~~ bibliography)" + end +(* +===================================== +docclass: Isa_COL.thms + name: "thms" + origin: Isa_COL + attrs: "properties" + invs: +docclass: Isa_COL.figure + name: "figure" + origin: Isa_COL + attrs: "relative_width", "src", "placement", "spawn_columns"(True) + invs: +docclass: Isa_COL.chapter = Isa_COL.text_element + + name: "chapter" + origin: Isa_COL + attrs: "level"(Some 0) + invs: +docclass: Isa_COL.concept + name: "concept" + origin: Isa_COL + attrs: "tag"([]), "properties"([]) + invs: +docclass: Isa_COL.section = Isa_COL.text_element + + name: "section" + origin: Isa_COL + attrs: "level"(Some 1) + invs: +docclass: Isa_COL.assertions + name: "assertions" + origin: Isa_COL + attrs: "properties" + invs: +docclass: Isa_COL.subsection = Isa_COL.text_element + + name: "subsection" + origin: Isa_COL + attrs: "level"(Some 2) + invs: +docclass: Isa_COL.definitions + name: "definitions" + origin: Isa_COL + attrs: "requires", "establishes" + invs: +docclass: Isa_COL.formal_item + name: "formal_item" + origin: Isa_COL + attrs: "item" + invs: +docclass: Isa_COL.figure_group + name: "figure_group" + origin: Isa_COL + attrs: "trace"([]), "caption" + invs: +docclass: Isa_COL.text_element + name: "text_element" + origin: Isa_COL + attrs: "level"(None), "referentiable"(False), "variants"({STR ''outline'', STR ''document''}) + invs: +docclass: scholarly_paper.data = scholarly_paper.engineering_content + + name: "data" + origin: scholarly_paper + attrs: "tag"([]) + invs: +docclass: technical_report.SML = technical_report.code + + name: "SML" + origin: technical_report + attrs: "checked"(False) + invs: +docclass: Isa_COL.subsubsection = Isa_COL.text_element + + name: "subsubsection" + origin: Isa_COL + attrs: "level"(Some 3) + invs: +docclass: scholarly_paper.annex = scholarly_paper.text_section + + name: "annex" + origin: scholarly_paper + attrs: "main_author"(None) + invs: +docclass: scholarly_paper.lemma = scholarly_paper.math_content + + name: "lemma" + origin: scholarly_paper + attrs: "referentiable"(True), "mcc"(lem) + invs: d3::\\. lemma.mcc \ = lem +docclass: scholarly_paper.title + name: "title" + origin: scholarly_paper + attrs: "short_title"(None) + invs: +docclass: technical_report.ISAR = technical_report.code + + name: "ISAR" + origin: technical_report + attrs: "checked"(False) + invs: +docclass: technical_report.code = scholarly_paper.technical + + name: "code" + origin: technical_report + attrs: "checked"(False), "label"([]) + invs: +docclass: Isa_COL.formal_content + name: "formal_content" + origin: Isa_COL + attrs: "trace"([]), "style" + invs: +docclass: scholarly_paper.author + name: "author" + origin: scholarly_paper + attrs: "email"([]), "http_site"([]), "orcid"([]), "affiliation" + invs: +docclass: technical_report.LATEX = technical_report.code + + name: "LATEX" + origin: technical_report + attrs: "checked"(False) + invs: +docclass: technical_report.index + name: "index" + origin: technical_report + attrs: "kind", "level" + invs: +docclass: scholarly_paper.article + name: "article" + origin: scholarly_paper + attrs: "trace"([]), "style_id"(''LNCS''), "version"((0, 0, 0)) + invs: +docclass: scholarly_paper.example = scholarly_paper.text_section + + name: "example" + origin: scholarly_paper + attrs: "referentiable"(True), "status"(description), "short_name"([]) + invs: +docclass: scholarly_paper.theorem = scholarly_paper.math_content + + name: "theorem" + origin: scholarly_paper + attrs: "referentiable"(True), "mcc"(thm) + invs: d2::\\. theorem.mcc \ = thm +docclass: scholarly_paper.abstract + name: "abstract" + origin: scholarly_paper + attrs: "keywordlist"([]), "principal_theorems" + invs: +docclass: scholarly_paper.subtitle + name: "subtitle" + origin: scholarly_paper + attrs: "abbrev"(None) + invs: +docclass: scholarly_paper.corollary = scholarly_paper.math_content + + name: "corollary" + origin: scholarly_paper + attrs: "referentiable"(True), "mcc"(cor) + invs: d4::\\. corollary.mcc \ = thm +docclass: scholarly_paper.technical = scholarly_paper.text_section + + name: "technical" + origin: scholarly_paper + attrs: "definition_list"([]), "status"(description), "formal_results" + invs: L1::\\. 0 < the (text_section.level \) +docclass: scholarly_paper.conclusion = scholarly_paper.text_section + + name: "conclusion" + origin: scholarly_paper + attrs: "main_author"(None) + invs: +docclass: scholarly_paper.definition = scholarly_paper.math_content + + name: "definition" + origin: scholarly_paper + attrs: "referentiable"(True), "mcc"(defn) + invs: d1::\\. definition.mcc \ = defn +docclass: scholarly_paper.evaluation = scholarly_paper.engineering_content + + name: "evaluation" + origin: scholarly_paper + attrs: "tag"([]) + invs: +docclass: scholarly_paper.experiment = scholarly_paper.engineering_content + + name: "experiment" + origin: scholarly_paper + attrs: "tag"([]) + invs: +docclass: Isa_COL.side_by_side_figure = Isa_COL.figure + + name: "side_by_side_figure" + origin: Isa_COL + attrs: "anchor", "caption", "relative_width2", "src2", "anchor2", "caption2" + invs: +docclass: scholarly_paper.bibliography = scholarly_paper.text_section + + name: "bibliography" + origin: scholarly_paper + attrs: "style"(Some ''LNCS'') + invs: +docclass: scholarly_paper.introduction = scholarly_paper.text_section + + name: "introduction" + origin: scholarly_paper + attrs: "comment", "claims" + invs: +docclass: scholarly_paper.math_content = scholarly_paper.technical + + name: "math_content" + origin: scholarly_paper + attrs: "referentiable"(True), "short_name"([]), "status"(semiformal), "mcc"(thm) + invs: s1::\\. \ math_content.referentiable \ \ + math_content.short_name \ = [], s2::\\. math_content.status \ = semiformal +docclass: scholarly_paper.math_example = scholarly_paper.math_content + + name: "math_example" + origin: scholarly_paper + attrs: "referentiable"(True), "mcc"(expl) + invs: d5::\\. math_example.mcc \ = expl +docclass: scholarly_paper.related_work = scholarly_paper.conclusion + + name: "related_work" + origin: scholarly_paper + attrs: "main_author"(None) + invs: +docclass: scholarly_paper.tech_example = scholarly_paper.technical + + name: "tech_example" + origin: scholarly_paper + attrs: "referentiable"(True), "tag"([]) + invs: +docclass: scholarly_paper.text_section = Isa_COL.text_element + + name: "text_section" + origin: scholarly_paper + attrs: "main_author"(None), "fixme_list"([]), "level"(None) + invs: +docclass: technical_report.front_matter + name: "front_matter" + origin: technical_report + attrs: "front_matter_style" + invs: +docclass: scholarly_paper.math_motivation = scholarly_paper.technical + + name: "math_motivation" + origin: scholarly_paper + attrs: "referentiable"(False) + invs: +docclass: scholarly_paper.math_semiformal = scholarly_paper.math_content + + name: "math_semiformal" + origin: scholarly_paper + attrs: "referentiable"(True) + invs: +docclass: scholarly_paper.math_explanation = scholarly_paper.technical + + name: "math_explanation" + origin: scholarly_paper + attrs: "referentiable"(False) + invs: +docclass: technical_report.table_of_contents + name: "table_of_contents" + origin: technical_report + attrs: "bookmark_depth"(3), "depth"(3) + invs: +docclass: scholarly_paper.engineering_content = scholarly_paper.technical + + name: "engineering_content" + origin: scholarly_paper + attrs: "short_name"([]), "status" + invs: +===================================== + + +*) diff --git a/src/tests/OutOfOrderPresntn.thy b/src/tests/OutOfOrderPresntn.thy index 3335a4f7..0238223c 100644 --- a/src/tests/OutOfOrderPresntn.thy +++ b/src/tests/OutOfOrderPresntn.thy @@ -62,8 +62,9 @@ fun gen_enriched_document_command2 cid_transform attr_transform fun check_n_tex_text thy = let val text = output_document (toplvl thy) markdown toks val file = {path = Path.make [oid ^ "_snippet.tex"], pos = @{here}, - content = Latex.output_text text} - val _ = Generated_Files.write_file (Path.make ["latex_test"]) file + content = Latex.output_text text} + val _ = Generated_Files.write_file (Path.make ["latex_test"]) + file val _ = writeln (Latex.output_text text) in thy end @@ -84,11 +85,24 @@ val _ = text\And here a tex - text macro.\ +text\Pythons reStructuredText (RST). @{url \https://de.wikipedia.org/wiki/ReStructuredText\}. +Tool: Sphinx. -text-[dfgdfg::B]\ Lorem ipsum ... @{thm refl} \ +\ -text\... and here is its application /macro expansion: - @{B [display] "dfgdfg"}\ +text*[aaa::B]\dfg\ + +text-[dfgdfg::B] +\ Lorem ipsum ... @{thm [display] refl} _ Frédéric \textbf{TEST} \verb+sdf+ \dfgdfg\ \ + +text-[asd::B] +\... and here is its application macro expansion: + @{B [display] "dfgdfg"} + @{cartouche [display] + \text*[dfgdfg::B] + \ Lorem ipsum ... @{thm refl} _ Frédéric \textbf{TEST} \verb+sdf+ \dfgdfg\ \ + \} +\