forked from Isabelle_DOF/Isabelle_DOF
added syntax for modes of doc_class_references.
For forward-references, defining references, … Global semantics untested and undocumented -> impl paper. Preparative step for doc_class_reference generation.
This commit is contained in:
parent
9dfa14eaea
commit
f3f95fe112
83
Isa_DOF.thy
83
Isa_DOF.thy
|
@ -17,7 +17,11 @@ theory Isa_DOF (* Isabelle Document Ontology Framework *)
|
||||||
|
|
||||||
begin
|
begin
|
||||||
|
|
||||||
|
|
||||||
|
text{*
|
||||||
|
@{thm [names_long] refl}
|
||||||
|
|
||||||
|
*}
|
||||||
section{* A HomeGrown Document Type Management (the ''Model'') *}
|
section{* A HomeGrown Document Type Management (the ''Model'') *}
|
||||||
|
|
||||||
ML{*
|
ML{*
|
||||||
|
@ -411,27 +415,6 @@ val _ =
|
||||||
(Toplevel.theory (DOF_core.declare_object_global oid))));
|
(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 =
|
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)
|
else error("undefined document reference:"^name)
|
||||||
end
|
end
|
||||||
|
|
||||||
(* superfluous :
|
(* generic syntax for doc_class links. *)
|
||||||
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));
|
|
||||||
|
|
||||||
fun basic_entities name scan pretty =
|
val defineN = "define"
|
||||||
Thy_Output.antiquotation name scan (fn {source, context = ctxt, ...} =>
|
val uncheckedN = "unchecked"
|
||||||
Thy_Output.output ctxt o Thy_Output.maybe_pretty_source pretty ctxt source);
|
|
||||||
|
|
||||||
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")*)
|
(* Setup for general docrefs of the global DOF_core.default_cid - class ("text")*)
|
||||||
val _ = Theory.setup
|
val _ = Theory.setup
|
||||||
((control_antiquotation @{binding docref} DOF_core.default_cid {strict_checking=true} "\\autoref{" "}" ) #>
|
((doc_class_ref_antiquotation @{binding docref} DOF_core.default_cid )
|
||||||
(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_antiquotation @{binding docref_unchecked} DOF_core.default_cid )#>
|
||||||
|
(doc_class_antiquotation @{binding docref_define} DOF_core.default_cid ))
|
||||||
|
*) )
|
||||||
|
|
||||||
end (* struct *)
|
end (* struct *)
|
||||||
*}
|
*}
|
||||||
|
@ -536,13 +525,11 @@ val _ =
|
||||||
|
|
||||||
|
|
||||||
section{* Testing and Validation *}
|
section{* Testing and Validation *}
|
||||||
|
ML{* op >> ;
|
||||||
ML{*
|
|
||||||
Binding.print;
|
Binding.print;
|
||||||
Syntax.read_term;
|
Syntax.read_term;
|
||||||
Syntax.pretty_typ;
|
Syntax.pretty_typ;
|
||||||
try;
|
try;
|
||||||
|
|
||||||
*}
|
*}
|
||||||
|
|
||||||
|
|
||||||
|
@ -559,16 +546,16 @@ fun document_command markdown (loc, txt) =
|
||||||
|
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
text{* @{theory "Nat"}*}
|
text{* @{theory "Nat"} @{thm refl}*}
|
||||||
ML\<open>
|
ML\<open>
|
||||||
open Markup;
|
open Markup;
|
||||||
Markup.binding;
|
Markup.binding;
|
||||||
TFree;
|
|
||||||
open Position;
|
open Position;
|
||||||
Position.line;
|
Position.line;
|
||||||
Context.Theory;
|
Context.Theory;
|
||||||
Context_Position.report_generic;
|
Context_Position.report_generic;
|
||||||
Context_Position.report;
|
Context_Position.report;
|
||||||
|
Term_Style.parse;
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
end
|
end
|
|
@ -41,6 +41,7 @@ but wrong doc_class constraint. *}
|
||||||
section{* Text Antiquotation Infrastructure ... *}
|
section{* Text Antiquotation Infrastructure ... *}
|
||||||
|
|
||||||
text{* @{docref \<open>lalala\<close>} -- produces warning. *}
|
text{* @{docref \<open>lalala\<close>} -- produces warning. *}
|
||||||
|
text{* @{docref (unchecked) \<open>lalala\<close>} -- produces no warning. *}
|
||||||
|
|
||||||
text{* @{docref \<open>ass122\<close>} -- global reference to a text-item in another file. *}
|
text{* @{docref \<open>ass122\<close>} -- global reference to a text-item in another file. *}
|
||||||
|
|
||||||
|
|
|
@ -0,0 +1,17 @@
|
||||||
|
chapter \<open>An Outline of a Common Criteria Ontology\<close>
|
||||||
|
|
||||||
|
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
|
|
@ -156,7 +156,9 @@ that governs the external test-execution via, eg., a makefile or specific calls
|
||||||
to a test-environment or test-engine *}
|
to a test-environment or test-engine *}
|
||||||
|
|
||||||
|
|
||||||
text \<open> As established by @{docref \<open>t10\<close>}, the
|
text \<open> As established by @{docref (unchecked) \<open>t10\<close>},
|
||||||
|
@{docref (define) \<open>t10\<close>}
|
||||||
|
the @{docref \<open>t10\<close>}
|
||||||
assumption @{docref \<open>ass122\<close>} is validated. \<close>
|
assumption @{docref \<open>ass122\<close>} is validated. \<close>
|
||||||
|
|
||||||
|
|
||||||
|
@ -165,24 +167,24 @@ section{* Provisory Setup *}
|
||||||
(* Hack: This should be generated automatically: *)
|
(* Hack: This should be generated automatically: *)
|
||||||
ML{*
|
ML{*
|
||||||
val _ = Theory.setup
|
val _ = Theory.setup
|
||||||
((DocAttrParser.control_antiquotation @{binding srac}
|
((DocAttrParser.doc_class_ref_antiquotation @{binding srac}
|
||||||
(DOF_core.name2doc_class_name @{theory} "srac")
|
(DOF_core.name2doc_class_name @{theory} "srac")
|
||||||
{strict_checking=true}
|
) #>
|
||||||
"\\autoref{" "}" ) #>
|
(DocAttrParser.doc_class_ref_antiquotation @{binding ec}
|
||||||
(DocAttrParser.control_antiquotation @{binding ec}
|
|
||||||
(DOF_core.name2doc_class_name @{theory} "ec")
|
(DOF_core.name2doc_class_name @{theory} "ec")
|
||||||
{strict_checking=true}
|
)#>
|
||||||
"\\autoref{" "}")#>
|
(DocAttrParser.doc_class_ref_antiquotation @{binding test_specification}
|
||||||
(DocAttrParser.control_antiquotation @{binding test_specification}
|
|
||||||
(DOF_core.name2doc_class_name @{theory} "test_specification")
|
(DOF_core.name2doc_class_name @{theory} "test_specification")
|
||||||
{strict_checking=true}
|
))
|
||||||
"\\label{" "}"))
|
|
||||||
|
|
||||||
*}
|
*}
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
section{* Testing and Validation *}
|
section{* Testing and Validation *}
|
||||||
|
|
||||||
|
|
||||||
|
|
Loading…
Reference in New Issue