forked from Isabelle_DOF/Isabelle_DOF
Configuration a la chasse du LaTeX generation bug (having its origine in the
Isar transaction engine).
This commit is contained in:
parent
bafc2405e9
commit
a0fac2d75b
28
Isa_DOF.thy
28
Isa_DOF.thy
|
@ -562,7 +562,7 @@ val _ =
|
||||||
val _ =
|
val _ =
|
||||||
Outer_Syntax.command ("text*", @{here}) "formal comment (primary style)"
|
Outer_Syntax.command ("text*", @{here}) "formal comment (primary style)"
|
||||||
(attributes -- Parse.opt_target -- Parse.document_source
|
(attributes -- Parse.opt_target -- Parse.document_source
|
||||||
>> enriched_document_command {markdown = false});
|
>> enriched_document_command {markdown = true});
|
||||||
|
|
||||||
|
|
||||||
val _ =
|
val _ =
|
||||||
|
@ -906,6 +906,32 @@ end (* struct *)
|
||||||
|
|
||||||
*}
|
*}
|
||||||
|
|
||||||
|
text*[xxxy] {* dd @{docitem_ref \<open>sdfg\<close>} @{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;*}
|
ML{* open Mixfix;*}
|
||||||
section{* Testing and Validation *}
|
section{* Testing and Validation *}
|
||||||
|
|
3
ROOT
3
ROOT
|
@ -1,11 +1,12 @@
|
||||||
session "Isabelle_DOF" = Main +
|
session "Isabelle_DOF" = Main +
|
||||||
|
options [document = pdf, document_output = "output"]
|
||||||
theories [document = false]
|
theories [document = false]
|
||||||
(* Foo *)
|
(* Foo *)
|
||||||
(* Bar *)
|
(* Bar *)
|
||||||
theories
|
theories
|
||||||
Isa_DOF
|
Isa_DOF
|
||||||
"ontologies/CENELEC_50126"
|
"ontologies/CENELEC_50126"
|
||||||
"ontologies/conceptual"
|
"ontologies/Conceptual"
|
||||||
"ontologies/scholarly_paper"
|
"ontologies/scholarly_paper"
|
||||||
"ontologies/mathex_onto"
|
"ontologies/mathex_onto"
|
||||||
|
|
||||||
|
|
|
@ -21,10 +21,10 @@ subsection*[header::Header,examSubject= "[algebra]", examTitle="''Exam number 1
|
||||||
*}
|
*}
|
||||||
|
|
||||||
(* should be in DOF-core *)
|
(* should be in DOF-core *)
|
||||||
(*
|
|
||||||
figure*[figure::figure, spawn_columns=False,relative_width="''80''",
|
figure*[figure::figure, spawn_columns=False,relative_width="''80''",
|
||||||
src="''figures/Polynomialdeg5.png''"] \<open> A Polynome. \<close>
|
src="''figures/Polynomialdeg5.png''"] \<open> A Polynome. \<close>
|
||||||
*)
|
|
||||||
subsubsection*[exo1 :: Exercise, Exercise.content="[q1::Task,q2::Task]"]\<open>Exercise 1\<close>
|
subsubsection*[exo1 :: Exercise, Exercise.content="[q1::Task,q2::Task]"]\<open>Exercise 1\<close>
|
||||||
text{*
|
text{*
|
||||||
Here are the first four lines of a number pattern.
|
Here are the first four lines of a number pattern.
|
||||||
|
|
|
@ -2,8 +2,8 @@ session "MathExam" = "HOL" +
|
||||||
options [document = pdf, document_output = "output"]
|
options [document = pdf, document_output = "output"]
|
||||||
theories [document = false]
|
theories [document = false]
|
||||||
(* Foo *)
|
(* Foo *)
|
||||||
"../../../ontologies/mathex_onto"
|
|
||||||
theories
|
theories
|
||||||
|
"../../../ontologies/mathex_onto"
|
||||||
MathExam
|
MathExam
|
||||||
document_files
|
document_files
|
||||||
"preamble.tex"
|
"preamble.tex"
|
||||||
|
|
|
@ -2,11 +2,12 @@ theory mathex_onto
|
||||||
imports "../Isa_DOF"
|
imports "../Isa_DOF"
|
||||||
begin
|
begin
|
||||||
|
|
||||||
|
(*<<*)
|
||||||
text{* In our scenario, content has four different types of addressees:
|
text{* In our scenario, content has four different types of addressees:
|
||||||
\<^item> the @{emph \<open>setter\<close>}, i.e. the author of the exam,
|
\<^item> the @{emph \<open>setter\<close>}, i.e. the author of the exam,
|
||||||
\<^item> the @{emph \<open>student\<close>}, i.e. the addressee of the exam,
|
\<^item> the @{emph \<open>student\<close>}, i.e. the addressee of the exam,
|
||||||
\<^item> the @{emph \<open>checker\<close>}, i.e. a person that checks the exam for
|
\<^item> the @{emph \<open>checker\<close>}, i.e. a person that checks the exam for
|
||||||
\<^item> the @{emph \<open>external_examiner\<close>}, i.e. a person that checks the exam for
|
\<^item> the @{emph \<open>external\_examiner\<close>}, i.e. a person that checks the exam for
|
||||||
feasibility and non-ambiguity.
|
feasibility and non-ambiguity.
|
||||||
|
|
||||||
Note that the latter quality assurance mechanism is used in many universities,
|
Note that the latter quality assurance mechanism is used in many universities,
|
||||||
|
@ -47,14 +48,6 @@ doc_class Header =
|
||||||
doc_class Exam_item =
|
doc_class Exam_item =
|
||||||
concerns :: "ContentClass set"
|
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
|
type_synonym SubQuestion = string
|
||||||
|
|
||||||
|
@ -103,4 +96,5 @@ doc_class MathExam=
|
||||||
global_grade :: Grade
|
global_grade :: Grade
|
||||||
where "\<lbrace>Author\<rbrace>\<^sup>+ ~~ Header ~~ \<lbrace>Exercise ~~ Solution\<rbrace>\<^sup>+ "
|
where "\<lbrace>Author\<rbrace>\<^sup>+ ~~ Header ~~ \<lbrace>Exercise ~~ Solution\<rbrace>\<^sup>+ "
|
||||||
|
|
||||||
|
(*>>*)
|
||||||
end
|
end
|
|
@ -36,21 +36,6 @@ doc_class technical = text_section +
|
||||||
text{* A very rough formatting style could be modeled as follows:*}
|
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 +
|
doc_class example = text_section +
|
||||||
comment :: "string"
|
comment :: "string"
|
||||||
|
|
||||||
|
|
Loading…
Reference in New Issue