From a0fac2d75b3f5fce2e9214ae4b29c7444dfb4801 Mon Sep 17 00:00:00 2001 From: bu Date: Tue, 19 Jun 2018 17:37:31 +0200 Subject: [PATCH] Configuration a la chasse du LaTeX generation bug (having its origine in the Isar transaction engine). --- Isa_DOF.thy | 34 +++++++++++++++++++++--- ROOT | 3 ++- examples/math_exam/MathExam/MathExam.thy | 4 +-- examples/math_exam/MathExam/ROOT | 2 +- ontologies/mathex_onto.thy | 14 +++------- ontologies/scholarly_paper.thy | 15 ----------- 6 files changed, 39 insertions(+), 33 deletions(-) diff --git a/Isa_DOF.thy b/Isa_DOF.thy index 92b8c64..49cfd07 100644 --- a/Isa_DOF.thy +++ b/Isa_DOF.thy @@ -477,7 +477,7 @@ fun enriched_document_command markdown (((((oid,pos),cid_pos), fun check_text thy = ( let val _ = (SPY3 := Thy_Output.output_text(Toplevel.theory_toplevel thy) markdown toks) in thy end) in - Toplevel.theory(enrich_trans #> check_text) + Toplevel.theory(enrich_trans #> check_text) (* Thanks Frederic Tuong! ! ! *) end; @@ -562,7 +562,7 @@ val _ = val _ = Outer_Syntax.command ("text*", @{here}) "formal comment (primary style)" (attributes -- Parse.opt_target -- Parse.document_source - >> enriched_document_command {markdown = false}); + >> enriched_document_command {markdown = true}); val _ = @@ -619,7 +619,7 @@ ML{* AnnoTextelemParser.SPY2; text*[sdfg] {* fg @{thm refl}*} ML{* AnnoTextelemParser.SPY3; *} - + ML{* (* text is : @@ -905,8 +905,34 @@ val _ = end (* struct *) *} - + +text*[xxxy] {* dd @{docitem_ref \sdfg\} @{thm refl}}*} + ML{* AnnoTextelemParser.SPY3; *} + +section{* Library of Standard Text Ontology *} + +datatype placement = pl_h | pl_t | pl_b | pl_ht | pl_hb +doc_class figure = + relative_width :: "string" (* percent of textwidth *) + src :: "string" + placement :: placement + spawn_columns :: bool <= True + +doc_class side_by_side_figure = figure + + anchor :: "string" + caption :: "string" + relative_width2 :: "string" (* percent of textwidth *) + src2 :: "string" + anchor2 :: "string" + caption2 :: "string" + +(* dito the future monitor: figure - block *) + +(* dito the future table *) + +(* dito the future monitor: table - block *) + ML{* open Mixfix;*} section{* Testing and Validation *} diff --git a/ROOT b/ROOT index 805fea9..aec2f99 100644 --- a/ROOT +++ b/ROOT @@ -1,11 +1,12 @@ session "Isabelle_DOF" = Main + + options [document = pdf, document_output = "output"] theories [document = false] (* Foo *) (* Bar *) theories Isa_DOF "ontologies/CENELEC_50126" - "ontologies/conceptual" + "ontologies/Conceptual" "ontologies/scholarly_paper" "ontologies/mathex_onto" diff --git a/examples/math_exam/MathExam/MathExam.thy b/examples/math_exam/MathExam/MathExam.thy index 0a0f26c..f07a23f 100644 --- a/examples/math_exam/MathExam/MathExam.thy +++ b/examples/math_exam/MathExam/MathExam.thy @@ -21,10 +21,10 @@ subsection*[header::Header,examSubject= "[algebra]", examTitle="''Exam number 1 *} (* should be in DOF-core *) -(* + figure*[figure::figure, spawn_columns=False,relative_width="''80''", src="''figures/Polynomialdeg5.png''"] \ A Polynome. \ -*) + subsubsection*[exo1 :: Exercise, Exercise.content="[q1::Task,q2::Task]"]\Exercise 1\ text{* Here are the first four lines of a number pattern. diff --git a/examples/math_exam/MathExam/ROOT b/examples/math_exam/MathExam/ROOT index 5128b22..9ee9356 100644 --- a/examples/math_exam/MathExam/ROOT +++ b/examples/math_exam/MathExam/ROOT @@ -2,8 +2,8 @@ session "MathExam" = "HOL" + options [document = pdf, document_output = "output"] theories [document = false] (* Foo *) - "../../../ontologies/mathex_onto" theories + "../../../ontologies/mathex_onto" MathExam document_files "preamble.tex" diff --git a/ontologies/mathex_onto.thy b/ontologies/mathex_onto.thy index b92b95b..c472812 100644 --- a/ontologies/mathex_onto.thy +++ b/ontologies/mathex_onto.thy @@ -2,11 +2,12 @@ theory mathex_onto imports "../Isa_DOF" begin +(*<<*) text{* In our scenario, content has four different types of addressees: \<^item> the @{emph \setter\}, i.e. the author of the exam, \<^item> the @{emph \student\}, i.e. the addressee of the exam, \<^item> the @{emph \checker\}, i.e. a person that checks the exam for -\<^item> the @{emph \external_examiner\}, i.e. a person that checks the exam for +\<^item> the @{emph \external\_examiner\}, i.e. a person that checks the exam for feasibility and non-ambiguity. Note that the latter quality assurance mechanism is used in many universities, @@ -47,14 +48,6 @@ doc_class Header = doc_class Exam_item = concerns :: "ContentClass set" -(* should go into something more fundamental on texts. *) -datatype placement = h | t | b | ht | hb -doc_class figure = Exam_item + - relative_width :: "string" (* percent of textwidth *) - src :: "string" - placement :: placement - spawn_columns :: bool <= True - type_synonym SubQuestion = string @@ -102,5 +95,6 @@ doc_class MathExam= content :: "(Header + Author + Exercise) list" global_grade :: Grade where "\Author\\<^sup>+ ~~ Header ~~ \Exercise ~~ Solution\\<^sup>+ " - + +(*>>*) end \ No newline at end of file diff --git a/ontologies/scholarly_paper.thy b/ontologies/scholarly_paper.thy index 41cd56c..59a5d1f 100644 --- a/ontologies/scholarly_paper.thy +++ b/ontologies/scholarly_paper.thy @@ -35,21 +35,6 @@ doc_class technical = text_section + text{* A very rough formatting style could be modeled as follows:*} - -datatype placement = h | t | b | ht | hb -doc_class figure = text_section + - relative_width :: "string" (* percent of textwidth *) - src :: "string" - placement :: placement - spawn_columns :: bool <= True - -doc_class side_by_side_figure = figure + - anchor :: "string" - caption :: "string" - relative_width2 :: "string" (* percent of textwidth *) - src2 :: "string" - anchor2 :: "string" - caption2 :: "string" doc_class example = text_section + comment :: "string"