From 338bb7d4a4699d4e9ff3ff575cb5a091bf9b6759 Mon Sep 17 00:00:00 2001 From: bu Date: Tue, 25 Aug 2020 11:59:10 +0200 Subject: [PATCH] Code cleanup. --- examples/CC_ISO15408/PikeOS_study/PikeOS_ST.thy | 6 +++--- src/DOF/Isa_DOF.thy | 13 +++++++------ src/ontologies/CC_v3.1_R5/CC_terminology.thy | 5 +++-- src/tests/OutOfOrderPresntn.thy | 4 ++-- 4 files changed, 15 insertions(+), 13 deletions(-) diff --git a/examples/CC_ISO15408/PikeOS_study/PikeOS_ST.thy b/examples/CC_ISO15408/PikeOS_study/PikeOS_ST.thy index 83d3f4b..7355571 100644 --- a/examples/CC_ISO15408/PikeOS_study/PikeOS_ST.thy +++ b/examples/CC_ISO15408/PikeOS_study/PikeOS_ST.thy @@ -12,7 +12,6 @@ section*[pkosstintrosec::st_ref_cls]\ ST Introduction \ open_monitor*[PikosIntro::ST_INTRO_MNT] subsection*[pkosstrefsubsec::st_ref_cls]\ ST Reference \ -text"@{docitem st_def}" text*[pkosstref::st_ref_cls, title="''PikeOS Security Target''", st_version ="(0,4,5)", authors= "[]", st_date= "''29072020''"] \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.\ subsection*[pkossttoeovrvwsubsec::st_ref_cls]\ TOE Overview \ -text*[pkosovrw1::toe_ovrw_cls]\The @{definition TOE} is a special kind of operating system, -that allows to effectively separate +text*[pkosovrw1::toe_ovrw_cls]\The @{definition \toe\ } is a special kind of operating +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 diff --git a/src/DOF/Isa_DOF.thy b/src/DOF/Isa_DOF.thy index f0a24b6..c85556f 100755 --- a/src/DOF/Isa_DOF.thy +++ b/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_command2 {inline=is_inline} cid_transform attr_transform +fun gen_enriched_document_command {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 diff --git a/src/ontologies/CC_v3.1_R5/CC_terminology.thy b/src/ontologies/CC_v3.1_R5/CC_terminology.thy index 77389e8..c894472 100644 --- a/src/ontologies/CC_v3.1_R5/CC_terminology.thy +++ b/src/ontologies/CC_v3.1_R5/CC_terminology.thy @@ -10,17 +10,18 @@ begin text\We re-use the class @\typ math_content\, which provides also a framework for semi-formal terminology, which we re-use by this definition.\ -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 \Terminology\ + subsection \Terms and definitions common in the CC\ Definition* [aas_def::concept, tag= "''adverse actions''"] diff --git a/src/tests/OutOfOrderPresntn.thy b/src/tests/OutOfOrderPresntn.thy index cfc9943..7d2894a 100644 --- a/src/tests/OutOfOrderPresntn.thy +++ b/src/tests/OutOfOrderPresntn.thy @@ -63,7 +63,7 @@ fun gen_enriched_document_command2 cid_transform attr_transform pos = @{here}, content = Latex.output_text text} - val _ = Generated_Files.write_file (Path.make ["latex_test"]) + val _ = Generated_Files.write_file (Path.make ["latex_test"]) file val _ = writeln (Latex.output_text text) in thy end @@ -122,7 +122,7 @@ Tool: Sphinx. \ text*[aaa::B]\dfg @{thm [display] refl}\ - + text-[dfgdfg::B] \ Lorem ipsum ... @{thm [display] refl} _ Frédéric \textbf{TEST} \verb+sdf+ \dfgdfg\ \