Code cleanup.

examples/CC_ISO15408/PikeOS_study/PikeOS_ST.thy

@@ -12,7 +12,6 @@ section*[pkosstintrosec::st_ref_cls]\<open> ST Introduction \<close>
 open_monitor*[PikosIntro::ST_INTRO_MNT]
 subsection*[pkosstrefsubsec::st_ref_cls]\<open> ST Reference \<close>
 
-text"@{docitem st_def}"
 text*[pkosstref::st_ref_cls, title="''PikeOS Security Target''", st_version ="(0,4,5)",
       authors= "[]", st_date= "''29072020''"]
 \<open>This document is the @{docitem st_def} for the Common Criteria evaluation of PikeOS. 
@@ -30,8 +29,8 @@ text*[pkostoeref::toe_ref_cls, dev_name="''''", toe_name="''PikeOS''",
    Certification Kit build S4250 and PikeOS 3.4 Common Criteria Kit build S4388.\<close>
 
 subsection*[pkossttoeovrvwsubsec::st_ref_cls]\<open> TOE Overview \<close>
-text*[pkosovrw1::toe_ovrw_cls]\<open>The @{definition TOE} is a special kind of operating system, 
+text*[pkosovrw1::toe_ovrw_cls]\<open>The @{definition \<open>toe\<close> } is a special kind of operating 
-that allows to effectively separate
+system, that allows to effectively separate
 different applications running on the same platform from each other. The TOE can host
 user applications that can also be operating systems. User applications can also be
 malicious, and even in that case the TOE ensures that malicious user applications are
@@ -44,6 +43,7 @@ to ensure complete separation of user applications and to prevent unexpected
 interference between user applications. The TOE enforces restrictions on the
 communication between the separated user applications as specified by the configuration
 data.
+
 The major security services provided by the TOE are:
 
 Separation in space of applications hosted in different partitions from each other

src/DOF/Isa_DOF.thy

@@ -910,7 +910,8 @@ fun ML_isa_check_docitem thy (term, req_ty, pos) =
                                        | _ => error("can not infer type for: "^ name)
                          in if cid <> DOF_core.default_cid 
                                andalso not(DOF_core.is_subclass ctxt cid req_class)
-                            then error("reference ontologically inconsistent")
+                            then error("reference ontologically inconsistent: "^ 
+                                       Position.here pos_decl)
                             else ()
                          end
            else err ("faulty reference to docitem: "^name) pos
@@ -1228,7 +1229,7 @@ fun update_instance_command  (((oid:string,pos),cid_pos),
             end
 
 
-
+(* old version :
 fun gen_enriched_document_command {inline=is_inline} cid_transform attr_transform 
                                   markdown  
                                   (((((oid,pos),cid_pos), doc_attrs) : meta_args_t,
@@ -1253,9 +1254,9 @@ fun gen_enriched_document_command {inline=is_inline} cid_transform attr_transfor
         #> check ) 
        (* Thanks Frederic Tuong for the hints concerning toplevel ! ! ! *)
   end;
+*)
 
-
+fun gen_enriched_document_command {inline=is_inline} cid_transform attr_transform 
-fun gen_enriched_document_command2 {inline=is_inline} cid_transform attr_transform 
                                   markdown  
                                   (((((oid,pos),cid_pos), doc_attrs) : meta_args_t,
                                      xstring_opt:(xstring * Position.T) option),
@@ -1368,7 +1369,7 @@ val _ =
 val _ =
   Outer_Syntax.command ("text*", @{here}) "formal comment (primary style)"
     (attributes -- Parse.opt_target -- Parse.document_source 
-      >> (Toplevel.theory o (gen_enriched_document_command2 {inline=true} 
+      >> (Toplevel.theory o (gen_enriched_document_command {inline=true} 
                                                            I I {markdown = true} )));
 
 (* This is just a stub at present *)
@@ -1538,7 +1539,7 @@ fun check_and_mark ctxt cid_decl (str:{strict_checking: bool}) {inline=inline_re
                      (* this sends a report for a ref application to the PIDE interface ... *) 
              val _ = if cid <> DOF_core.default_cid 
                         andalso not(DOF_core.is_subclass ctxt cid cid_decl)
-                     then error("reference ontologically inconsistent")
+                     then error("reference ontologically inconsistent:" ^ Position.here pos_decl)
                      else ()
          in () end
     else if   DOF_core.is_declared_oid_global name thy 

src/ontologies/CC_v3.1_R5/CC_terminology.thy

@@ -10,17 +10,18 @@ begin
 text\<open>We re-use the class @\<open>typ math_content\<close>, which provides also a framework for
 semi-formal terminology, which we re-use by this definition.\<close>
 
-doc_class semi_formal_content = math_content +
+doc_class concept_definition = "definition" +
       status        :: status <= "semiformal" 
       mcc           :: math_content_class <= "terminology"
       tag           :: string
 
-type_synonym concept = semi_formal_content  
+type_synonym concept = concept_definition  
 
 (*>>*)
 
 section \<open>Terminology\<close>
 
+
 subsection \<open>Terms and definitions common in the CC\<close>
 
 Definition* [aas_def::concept, tag= "''adverse actions''"]