From c752a25dd6352a796f1ae0c82a221eb287954be7 Mon Sep 17 00:00:00 2001
From: bu <wolff@lri.fr>
Date: Thu, 18 Apr 2019 17:13:32 +0200
Subject: [PATCH] no message

---
 Isa_DOF.thy                  | 16 +++++++++++++++-
 ontologies/CENELEC_50128.thy | 24 ++++++++++++++----------
 2 files changed, 29 insertions(+), 11 deletions(-)

diff --git a/Isa_DOF.thy b/Isa_DOF.thy
index 3dbf2ef..2d92ff6 100644
--- a/Isa_DOF.thy
+++ b/Isa_DOF.thy
@@ -1511,7 +1511,9 @@ end\<close>
 
  
 section\<open> Syntax for Ontological Antiquotations (the '' View'' Part II) \<close>
-  
+
+text\<open> @{theory Main}\<close>
+
 ML\<open>
 structure OntoLinkParser = 
 struct
@@ -1555,6 +1557,16 @@ fun docitem_antiquotation_generic cid_decl
              {context = ctxt, source = src:Token.src, state}  
              ({unchecked = x, define= y}, source:Input.source) =
              let fun label_latex flag = enclose (if flag then "\\label{"  else "\\autoref{") "}"
+                 val X1 = Thy_Output.output_text state {markdown=false}
+                          :  Input.source -> string
+                 val X2 = check_and_mark ctxt                   
+                                 cid_decl 
+                                 ({strict_checking = not x})
+                                 (Input.pos_of source)
+                          : string -> string
+                 val X3 = label_latex y
+                          : string -> string
+                 
              in 
                  (Thy_Output.output_text state {markdown=false} #>
                   check_and_mark ctxt                   
@@ -1811,4 +1823,6 @@ val _ =
 end (* struct *)
 \<close>  
 
+ML\<open>Thy_Output.document_command; Thy_Output.output_text\<close>
+
 end
diff --git a/ontologies/CENELEC_50128.thy b/ontologies/CENELEC_50128.thy
index 29e7692..e63ca22 100644
--- a/ontologies/CENELEC_50128.thy
+++ b/ontologies/CENELEC_50128.thy
@@ -28,6 +28,8 @@ Safety assessment is focused on but not limited to the safety properties of a sy
 Definition*[assessor::concept, tag="''assessor''"]
 \<open>entity that carries out an assessment\<close>
 
+text\<open>@{docitem \<open>assessment\<close>}\<close>
+
 Definition*[COTS::concept, tag="''commercial off-the-shelf software''"]
 \<open>software defined by market-driven need, commercially available and whose fitness for purpose 
 has been demonstrated by a broad spectrum of commercial users\<close>
@@ -71,7 +73,7 @@ from the intended performance or behaviour (cf @{concept \<open>error\<close>})\
 Definition*[failure::concept]
 \<open>unacceptable difference between required and observed performance\<close>
 
-Definition*[FT::concept, tag="''fault tolerance''"]
+Definition*[FT::concept, tag="\<open>fault tolerance\<close>"]
 \<open>built-in capability of a system to provide continued correct provision of service as specified, 
 in the presence of a limited number of hardware or software faults\<close>
 
@@ -260,6 +262,16 @@ datatype phase = SYSDEV_ext (* System Development Phase (external) *)
                | SD    (* Software Deployment       *)
                | SM    (* Software Maintenance      *)
 
+datatype sil = SIL0 | SIL1 | SIL2 | SIL3 | SIL4
+
+type_synonym saftety_integraytion_level = sil
+
+doc_class cenelec_text = text_element +
+   phase        :: "phase"
+   sil          :: sil
+   is_concerned :: "role set" <= "UNIV" 
+
+
 abbreviation software_requirement  :: "phase" where "software_requirement  \<equiv> SR"
 abbreviation software_architecture :: "phase" where "software_architecture \<equiv> SA"
 abbreviation software_design       :: "phase" where "software_design       \<equiv> SD"
@@ -276,9 +288,6 @@ term "SR" (* meta-test *)
 
 section\<open>Objectives, Conformance and Software Integrity Levels\<close>
 
-datatype sil = SIL0 | SIL1 | SIL2 | SIL3 | SIL4
-
-type_synonym saftety_integraytion_level = sil
 
 
 doc_class objectives =
@@ -286,7 +295,7 @@ doc_class objectives =
    is_concerned :: "role set"
 
 
-doc_class requirement = text_element +
+doc_class requirement = cenelec_text +
    long_name    :: "string option"
    is_concerned :: "role set"
   
@@ -450,11 +459,6 @@ doc_class judgement =
 
 section\<open> Design and Test Documents \<close> 
 
-doc_class cenelec_text = text_element +
-   phase        :: "phase"
-   is_concerned :: "role set" <= "UNIV" 
-
-
 
 doc_class SYSREQS = cenelec_text + 
    phase        :: "phase"  <= "SYSDEV_ext"