no message

examples/simple/Article.thy

@@ -11,7 +11,7 @@ text*[tit::title]{* Using The Isabelle Ontology Framework*}
 text*[stit::subtitle] \<open>Linking the Formal with the Informal\<close>
   
 text*[auth1::author, affiliation="''University of Sheffield''"]\<open>Achim Brucker\<close>
-text*[auth2::author, affiliation="''Centrale-Supelec''"]\<open>Idir Ait-Adune\<close>
+text*[auth2::author, affiliation="''Centrale-Supelec''"]\<open>Idir Ait-Sadoune\<close>
 text*[auth3::author, affiliation="''IRT-SystemX''"]\<open>Paolo Crizzifulli\<close>
 text*[auth4::author, affiliation="''Universit\\'e Paris-Sud''"]\<open>Burkhart Wolff\<close>
 term "\<lparr>author.tag_attribute=undefined,affiliation=undefined\<rparr>"

examples/simple/MathExam.thy

@@ -4,12 +4,12 @@ begin
 
 open_monitor*[exam::MathExam] 
 
-text*[idir::Author, affiliation="''CentraleSupelec''"]{*Idir AIT SADOUNE*}
+text*[idir::Author, affiliation="CentraleSupelec"]{*Idir AIT SADOUNE*}
 
-text*[header::Header,examGrade="A1", examSubject= "algebra", examTitle="''Exam number 1''"]
+text*[header::Header,examGrade="A1", examSubject= "algebra", examTitle="Exam number 1"]
 {* Please follow directions carefully and show all your work.*}
 
-section*[exo1 :: Exercise, content="[q1,q2,q3]"]{* Exercise 1.*}
+section*[exo1 :: Exercise, content="[q1,q2,q3]", mark="15"]{* Exercise 1.*}
 text*[q1::Question, level="twoStars", mark="5"] 
 {*
 Give an example of each of the following : 
@@ -19,24 +19,12 @@ b - a real number which is not rational.
 
 text*[q2::Question, level="oneStar", mark="5"] 
 {*
-Write in interval notation : @{term ''-3 < x < 5''}
+Write in interval notation : @{term "-3 < x"} and  @{term "x < 5"}
 *}
 
 text*[q3::Question, level="oneStar", mark="5"] 
-{* True or false : @{term ''0/8 = 0''} *}
+{* True or false : @{term "0/8 = 0"} *}
 
 close_monitor*[exam] 
 
 end
-
-(*
-
-section{* Example*}  
- 
-term "[ @{thm ''refl''}] @ [ @{thm ''sym''}, @{thm ''trans''} ] "
-  
-text{*
-      @{term "[ @{thm ''refl''}] @ [ @{thm ''sym''}, @{thm ''trans''} ]"}} are the theorems
-of the equational logic fragment of HOL.
-*}
-*)

ontologies/mathex_onto.thy

@@ -26,6 +26,7 @@ doc_class Question =
 
 doc_class Exercise= 
   content :: "(Question) list"
+  mark :: integer
 
 doc_class MathExam=
   content :: "(Header + Author + Exercise) list"