diff --git a/Isa_DOF.thy b/Isa_DOF.thy index 381a0011..16f9435a 100644 --- a/Isa_DOF.thy +++ b/Isa_DOF.thy @@ -17,7 +17,11 @@ theory Isa_DOF (* Isabelle Document Ontology Framework *) begin - + +text{* + @{thm [names_long] refl} + +*} section{* A HomeGrown Document Type Management (the ''Model'') *} ML{* @@ -411,27 +415,6 @@ val _ = (Toplevel.theory (DOF_core.declare_object_global oid)))); -(* Proof.context -> Symtab.key * Position.T -> Pretty.T ; dead code: -fun pretty_docref ctxt (name, pos) = - let - (* val _ = DOF_core.writeln_keys ctxt *) - val thy = Proof_Context.theory_of ctxt; - fun pretty_docref str = let val tok = Pretty.enclose "\\autoref{" "}" (Pretty.text (str)) - (* val _ = writeln (Pretty.string_of tok) *) - in tok end - in - if DOF_core.is_defined_oid_global name thy - then let val {pos=pos_decl,id,...} = the(DOF_core.get_object_global name thy) - val markup = docref_markup false name id pos_decl; - val _ = Context_Position.report ctxt pos markup; - (* this sends a report to the PIDE interface ... *) - in pretty_docref name end - else if DOF_core.is_declared_oid_global name thy - then (warning("declared but undefined document reference:"^name); - pretty_docref name) - else error("undefined document reference:"^name) - end -*) fun check_and_mark ctxt cid_decl (str:{strict_checking: bool}) pos name = @@ -454,34 +437,40 @@ fun check_and_mark ctxt cid_decl (str:{strict_checking: bool}) pos name = else error("undefined document reference:"^name) end -(* superfluous : -fun basic_entities_style name scan pretty = - Thy_Output.antiquotation name scan (fn {source, context = ctxt, ...} => fn (style, xs) => - Thy_Output.output ctxt - (Thy_Output.maybe_pretty_source (fn ctxt => fn x => pretty ctxt (style, x)) ctxt source xs)); +(* generic syntax for doc_class links. *) -fun basic_entities name scan pretty = - Thy_Output.antiquotation name scan (fn {source, context = ctxt, ...} => - Thy_Output.output ctxt o Thy_Output.maybe_pretty_source pretty ctxt source); +val defineN = "define" +val uncheckedN = "unchecked" -fun basic_entity name scan = basic_entities name (scan >> single); -*) +val doc_ref_modes = Scan.optional (Args.parens (Args.$$$ defineN || Args.$$$ uncheckedN) + >> (fn str => if str = defineN + then {unchecked = false, define= true} + else {unchecked = true, define= false})) + {unchecked = false, define= false}; -fun control_antiquotation name cid_decl (str:{strict_checking: bool}) s1 s2 = - Thy_Output.antiquotation name (Scan.lift (Args.cartouche_input)) - (fn {context =ctxt, source = src:Token.src, state} => - fn source:Input.source => - (Thy_Output.output_text state {markdown=false} #> - check_and_mark ctxt cid_decl (str:{strict_checking: bool})(Input.pos_of source) #> - enclose s1 s2) - source); +fun doc_class_ref_antiquotation name cid_decl = + let fun open_par x = if x then (writeln "ctr_anti true"; "\\label{" ) + else (writeln "ctr_anti false"; "\\autoref{" ) + val close = "}" + in +(* Thy_Output.antiquotation name (Scan.lift (args_alt -- Args.cartouche_input)) *) + Thy_Output.antiquotation name (Scan.lift (doc_ref_modes -- Args.cartouche_input)) + (fn {context =ctxt, source = src:Token.src, state} => + fn ({unchecked = x, define= y}, source:Input.source) => + (Thy_Output.output_text state {markdown=false} #> + check_and_mark ctxt cid_decl ({strict_checking = not x})(Input.pos_of source) #> + enclose (open_par y) close) + source) + end (* Setup for general docrefs of the global DOF_core.default_cid - class ("text")*) val _ = Theory.setup - ((control_antiquotation @{binding docref} DOF_core.default_cid {strict_checking=true} "\\autoref{" "}" ) #> - (control_antiquotation @{binding docref_unchecked} DOF_core.default_cid {strict_checking=false} "\\autoref{" "}")#> - (control_antiquotation @{binding docref_define} DOF_core.default_cid {strict_checking=false} "\\label{" "}")) + ((doc_class_ref_antiquotation @{binding docref} DOF_core.default_cid ) +(* #> + (doc_class_antiquotation @{binding docref_unchecked} DOF_core.default_cid )#> + (doc_class_antiquotation @{binding docref_define} DOF_core.default_cid )) +*) ) end (* struct *) *} @@ -536,13 +525,11 @@ val _ = section{* Testing and Validation *} - -ML{* +ML{* op >> ; Binding.print; Syntax.read_term; Syntax.pretty_typ; try; - *} @@ -559,16 +546,16 @@ fun document_command markdown (loc, txt) = \ -text{* @{theory "Nat"}*} +text{* @{theory "Nat"} @{thm refl}*} ML\ open Markup; Markup.binding; -TFree; open Position; Position.line; Context.Theory; Context_Position.report_generic; Context_Position.report; +Term_Style.parse; \ end \ No newline at end of file diff --git a/examples/simple/Example.thy b/examples/simple/Example.thy index 7d7e2421..5429760b 100644 --- a/examples/simple/Example.thy +++ b/examples/simple/Example.thy @@ -41,6 +41,7 @@ but wrong doc_class constraint. *} section{* Text Antiquotation Infrastructure ... *} text{* @{docref \lalala\} -- produces warning. *} +text{* @{docref (unchecked) \lalala\} -- produces no warning. *} text{* @{docref \ass122\} -- global reference to a text-item in another file. *} diff --git a/ontologies/CC_ISO15408.thy b/ontologies/CC_ISO15408.thy index e69de29b..8598fa2c 100644 --- a/ontologies/CC_ISO15408.thy +++ b/ontologies/CC_ISO15408.thy @@ -0,0 +1,17 @@ +chapter \An Outline of a Common Criteria Ontology\ + +text{* NOTE: An Ontology-Model of a certification standard such as Comon Criteria or +Common Criteria (ISO15408) identifies: +- notions (conceptual \emph{categories}) having \emph{instances} + (similar to classes and objects), +- their subtype relation (eg., a "security target" is a "requirement definition"), +- their syntactical structure + (for the moment: defined by regular expressions describing the + order of category instances in the overall document as a regular language) + *} + +theory CC_ISO15408 + imports "../Isa_DOF" +begin + +end \ No newline at end of file diff --git a/ontologies/CENELEC_50126.thy b/ontologies/CENELEC_50126.thy index d4df3d57..4589962a 100644 --- a/ontologies/CENELEC_50126.thy +++ b/ontologies/CENELEC_50126.thy @@ -156,7 +156,9 @@ that governs the external test-execution via, eg., a makefile or specific calls to a test-environment or test-engine *} -text \ As established by @{docref \t10\}, the +text \ As established by @{docref (unchecked) \t10\}, + @{docref (define) \t10\} + the @{docref \t10\} assumption @{docref \ass122\} is validated. \ @@ -165,24 +167,24 @@ section{* Provisory Setup *} (* Hack: This should be generated automatically: *) ML{* val _ = Theory.setup - ((DocAttrParser.control_antiquotation @{binding srac} + ((DocAttrParser.doc_class_ref_antiquotation @{binding srac} (DOF_core.name2doc_class_name @{theory} "srac") - {strict_checking=true} - "\\autoref{" "}" ) #> - (DocAttrParser.control_antiquotation @{binding ec} + ) #> + (DocAttrParser.doc_class_ref_antiquotation @{binding ec} (DOF_core.name2doc_class_name @{theory} "ec") - {strict_checking=true} - "\\autoref{" "}")#> - (DocAttrParser.control_antiquotation @{binding test_specification} + )#> + (DocAttrParser.doc_class_ref_antiquotation @{binding test_specification} (DOF_core.name2doc_class_name @{theory} "test_specification") - {strict_checking=true} - "\\label{" "}")) + )) *} + + + section{* Testing and Validation *}