forked from Isabelle_DOF/Isabelle_DOF
Simplified thy_output (cleanup) and set first LaTeX meta-args generator.
Restructuring
This commit is contained in:
parent
0f12eb2e21
commit
1358540a62
41
Isa_DOF.thy
41
Isa_DOF.thy
|
@ -387,6 +387,22 @@ ML{*
|
||||||
structure AnnoTextelemParser =
|
structure AnnoTextelemParser =
|
||||||
struct
|
struct
|
||||||
|
|
||||||
|
type meta_args_t = (((string * Position.T) *
|
||||||
|
(string * Position.T) option)
|
||||||
|
* ((string * Position.T) * string) list)
|
||||||
|
|
||||||
|
fun meta_args_2_string thy (((lab, _), cid_opt), attr_list) =
|
||||||
|
(* for the moment naive, i.e. without textual normalization of attribute names and
|
||||||
|
adapted term printing *)
|
||||||
|
let val l = "label = "^lab
|
||||||
|
val cid = "cid =" ^ (case cid_opt of
|
||||||
|
NONE => DOF_core.default_cid
|
||||||
|
| SOME(cid,_) => DOF_core.name2doc_class_name thy cid)
|
||||||
|
fun str ((lhs,_),rhs) = lhs^"="^rhs (* no normalization on lhs (could be long-name)
|
||||||
|
no paraphrasing on rhs (could be fully paranthesized
|
||||||
|
pretty-printed formula in LaTeX notation ... *)
|
||||||
|
in enclose "[" "]" (commas ([l,cid] @ (map str attr_list))) end
|
||||||
|
|
||||||
val semi = Scan.option (Parse.$$$ ";");
|
val semi = Scan.option (Parse.$$$ ";");
|
||||||
|
|
||||||
val attribute =
|
val attribute =
|
||||||
|
@ -408,7 +424,7 @@ val attributes =
|
||||||
(Parse.$$$ "["
|
(Parse.$$$ "["
|
||||||
|-- (reference --
|
|-- (reference --
|
||||||
(Scan.optional(Parse.$$$ "," |-- (Parse.enum "," attribute))) []))
|
(Scan.optional(Parse.$$$ "," |-- (Parse.enum "," attribute))) []))
|
||||||
--| Parse.$$$ "]"
|
--| Parse.$$$ "]" : meta_args_t parser
|
||||||
|
|
||||||
val attributes_upd =
|
val attributes_upd =
|
||||||
(Parse.$$$ "["
|
(Parse.$$$ "["
|
||||||
|
@ -444,8 +460,7 @@ fun check_classref (SOME(cid,pos')) thy =
|
||||||
fun generalize_typ n = Term.map_type_tfree (fn (str,sort)=> Term.TVar((str,n),sort));
|
fun generalize_typ n = Term.map_type_tfree (fn (str,sort)=> Term.TVar((str,n),sort));
|
||||||
fun infer_type thy term = hd (Type_Infer_Context.infer_types (Proof_Context.init_global thy) [term])
|
fun infer_type thy term = hd (Type_Infer_Context.infer_types (Proof_Context.init_global thy) [term])
|
||||||
|
|
||||||
fun enriched_document_command markdown (((((oid,pos),cid_pos),
|
fun enriched_document_command markdown (((((oid,pos),cid_pos), doc_attrs) : meta_args_t,
|
||||||
doc_attrs: ((string * Position.T) * string) list),
|
|
||||||
xstring_opt:(xstring * Position.T) option),
|
xstring_opt:(xstring * Position.T) option),
|
||||||
toks:Input.source)
|
toks:Input.source)
|
||||||
: Toplevel.transition -> Toplevel.transition =
|
: Toplevel.transition -> Toplevel.transition =
|
||||||
|
@ -454,11 +469,12 @@ fun enriched_document_command markdown (((((oid,pos),cid_pos),
|
||||||
val _ = Position.report pos (docref_markup true oid id pos);
|
val _ = Position.report pos (docref_markup true oid id pos);
|
||||||
(* creates a markup label for this position and reports it to the PIDE framework;
|
(* creates a markup label for this position and reports it to the PIDE framework;
|
||||||
this label is used as jump-target for point-and-click feature. *)
|
this label is used as jump-target for point-and-click feature. *)
|
||||||
|
|
||||||
fun enrich_trans thy =
|
fun enrich_trans thy =
|
||||||
let val cid_long = check_classref cid_pos thy
|
let val cid_long = check_classref cid_pos thy
|
||||||
val count = Unsynchronized.ref (0 - 1);
|
val count = Unsynchronized.ref (0 - 1);
|
||||||
fun incr () = Unsynchronized.inc count
|
fun incr () = Unsynchronized.inc count
|
||||||
|
val _ = writeln ("XXX" ^ (meta_args_2_string thy (((oid,pos),cid_pos), doc_attrs)) )
|
||||||
|
|
||||||
val generalize_term = let val n = incr () in Term.map_types (generalize_typ n) end
|
val generalize_term = let val n = incr () in Term.map_types (generalize_typ n) end
|
||||||
fun read_assn ((lhs, pos), rhs) =
|
fun read_assn ((lhs, pos), rhs) =
|
||||||
((Syntax.read_term_global thy lhs |> generalize_term,pos),
|
((Syntax.read_term_global thy lhs |> generalize_term,pos),
|
||||||
|
@ -475,8 +491,8 @@ fun enriched_document_command markdown (((((oid,pos),cid_pos),
|
||||||
id=id,
|
id=id,
|
||||||
cid=cid_long})
|
cid=cid_long})
|
||||||
end
|
end
|
||||||
fun check_text thy = ( let val _ = (SPY3 := Thy_Output.output_text(Toplevel.theory_toplevel thy) markdown toks)
|
fun check_text thy = let val _ = Thy_Output.output_text(Toplevel.theory_toplevel thy) markdown toks
|
||||||
in thy end)
|
in thy end (* as side-effect, generates markup *)
|
||||||
in
|
in
|
||||||
Toplevel.theory(enrich_trans #> check_text)
|
Toplevel.theory(enrich_trans #> check_text)
|
||||||
(* Thanks Frederic Tuong! ! ! *)
|
(* Thanks Frederic Tuong! ! ! *)
|
||||||
|
@ -609,6 +625,10 @@ val _ =
|
||||||
>> (fn ((((((oid,pos),cid),doc_attrs),some_name:string option),modes : string list),t:string) =>
|
>> (fn ((((((oid,pos),cid),doc_attrs),some_name:string option),modes : string list),t:string) =>
|
||||||
(Toplevel.keep (assert_cmd some_name modes t)))); (* dummy/fake so far *)
|
(Toplevel.keep (assert_cmd some_name modes t)))); (* dummy/fake so far *)
|
||||||
|
|
||||||
|
(* this sets parser and converter for LaTeX generation of meta-attributes.
|
||||||
|
Currently of *all* commands, no distinction between text* and text command.
|
||||||
|
*)
|
||||||
|
val _ = Thy_Output.set_meta_args_parser (fn thy => attributes >> meta_args_2_string thy)
|
||||||
|
|
||||||
end (* struct *)
|
end (* struct *)
|
||||||
|
|
||||||
|
@ -671,7 +691,6 @@ ML{*
|
||||||
structure OntoLinkParser =
|
structure OntoLinkParser =
|
||||||
struct
|
struct
|
||||||
|
|
||||||
|
|
||||||
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 =
|
||||||
let
|
let
|
||||||
val thy = Proof_Context.theory_of ctxt;
|
val thy = Proof_Context.theory_of ctxt;
|
||||||
|
@ -738,8 +757,6 @@ fun check_and_mark_term ctxt oid =
|
||||||
else error("undefined document reference:"^oid)
|
else error("undefined document reference:"^oid)
|
||||||
end
|
end
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
val X = (Scan.lift Args.cartouche_input : Input.source context_parser) >> (fn inp => "")
|
val X = (Scan.lift Args.cartouche_input : Input.source context_parser) >> (fn inp => "")
|
||||||
|
|
||||||
fun docitem_value_ML_antiquotation binding =
|
fun docitem_value_ML_antiquotation binding =
|
||||||
|
@ -909,7 +926,7 @@ end (* struct *)
|
||||||
|
|
||||||
text*[xxxy] {* dd @{docitem_ref \<open>sdfg\<close>} @{thm refl}*}
|
text*[xxxy] {* dd @{docitem_ref \<open>sdfg\<close>} @{thm refl}*}
|
||||||
|
|
||||||
ML{* AnnoTextelemParser.SPY3; *}
|
ML{* AnnoTextelemParser.SPY3; *}
|
||||||
|
|
||||||
text{* dd @{docitem_ref \<open>sdfg\<close>} @{thm refl} *}
|
text{* dd @{docitem_ref \<open>sdfg\<close>} @{thm refl} *}
|
||||||
|
|
||||||
|
@ -937,7 +954,7 @@ doc_class side_by_side_figure = figure +
|
||||||
(* dito the future monitor: table - block *)
|
(* dito the future monitor: table - block *)
|
||||||
|
|
||||||
section{* Testing and Validation *}
|
section{* Testing and Validation *}
|
||||||
|
(*
|
||||||
ML{*
|
ML{*
|
||||||
|
|
||||||
local
|
local
|
||||||
|
@ -993,5 +1010,5 @@ fun set_meta_args_parser f = (meta_args_parser_hook:= f)
|
||||||
end
|
end
|
||||||
|
|
||||||
*}
|
*}
|
||||||
|
*)
|
||||||
end
|
end
|
||||||
|
|
|
@ -9,7 +9,7 @@ section{* Some show-off's of general antiquotations. *}
|
||||||
print_attributes
|
print_attributes
|
||||||
print_antiquotations
|
print_antiquotations
|
||||||
|
|
||||||
text{* @{thm refl} of name @{thm [source] refl}
|
text\<open> @{thm refl} of name @{thm [source] refl}
|
||||||
@{thm[mode=Rule] conjI}
|
@{thm[mode=Rule] conjI}
|
||||||
@{file "../../Isa_DOF.thy"}
|
@{file "../../Isa_DOF.thy"}
|
||||||
@{value "3+4::int"}
|
@{value "3+4::int"}
|
||||||
|
@ -17,7 +17,7 @@ text{* @{thm refl} of name @{thm [source] refl}
|
||||||
@{theory List}}
|
@{theory List}}
|
||||||
@{term "3"}
|
@{term "3"}
|
||||||
@{type bool}
|
@{type bool}
|
||||||
@{term [show_types] "f x = a + x"} *}
|
@{term [show_types] "f x = a + x"} \<close>
|
||||||
|
|
||||||
section{* Example *}
|
section{* Example *}
|
||||||
|
|
||||||
|
@ -40,48 +40,20 @@ to a test-environment or test-engine *}
|
||||||
text \<open> As established by @{docref (unchecked) \<open>t10\<close>},
|
text \<open> As established by @{docref (unchecked) \<open>t10\<close>},
|
||||||
@{docref (define) \<open>t10\<close>} \<close>
|
@{docref (define) \<open>t10\<close>} \<close>
|
||||||
text \<open> the @{docref \<open>t10\<close>}
|
text \<open> the @{docref \<open>t10\<close>}
|
||||||
the @{docref \<open>ass122\<close>}
|
as well as the @{docref \<open>ass122\<close>}\<close>
|
||||||
|
text \<open> represent a justification of the safety related applicability
|
||||||
|
condition @{srac \<open>ass122\<close>} aka exported constraint @{ec \<open>ass122\<close>}.
|
||||||
\<close>
|
\<close>
|
||||||
text \<open> safety related applicability condition @{srac \<open>ass122\<close>}. \<close>
|
|
||||||
text \<open> exported constraint @{ec \<open>ass122\<close>}.
|
|
||||||
\<close>
|
|
||||||
|
|
||||||
text{* And some ontologically inconsistent reference: @{hypothesis \<open>ass1\<close>} as well as *}
|
|
||||||
-- wrong
|
|
||||||
|
|
||||||
text{* ... some more ontologically inconsistent reference: @{assumption \<open>hyp1\<close>} as well as *}
|
|
||||||
-- wrong
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
text{* And a further ontologically totally inconsistent reference:
|
|
||||||
@{test_result \<open>ass122\<close>} as well as ... *}
|
|
||||||
-- wrong
|
|
||||||
|
|
||||||
text{* the ontologically inconsistent reference: @{ec \<open>t10\<close>} *}
|
|
||||||
-- wrong
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
section{* Some Tests for Ontology Framework and its CENELEC Instance *}
|
section{* Some Tests for Ontology Framework and its CENELEC Instance *}
|
||||||
|
|
||||||
declare_reference* [lalala::requirement, alpha="main", beta=42]
|
declare_reference* [lalala::requirement, alpha="main", beta=42]
|
||||||
|
|
||||||
declare_reference* [lalala::quod] (* shouldn't work: multiple declaration *)
|
|
||||||
|
|
||||||
declare_reference* [blablabla::cid, alpha="beta sdf", beta=gamma, delta=dfg_fgh\<^sub>1]
|
declare_reference* [blablabla::cid, alpha="beta sdf", beta=gamma, delta=dfg_fgh\<^sub>1]
|
||||||
|
|
||||||
paragraph*[sdf]{* just a paragraph *}
|
|
||||||
paragraph* [sdfk] \<open> just a paragraph - lexical variant \<close>
|
paragraph* [sdfk] \<open> just a paragraph - lexical variant \<close>
|
||||||
|
|
||||||
subsection*[sdf]{* shouldn't work, multiple ref. *}
|
|
||||||
|
|
||||||
section*[sedf::requirement, alpja= refl]{* works again. One can hover over the class constraint and
|
|
||||||
jump to its definition. *}
|
|
||||||
text\<open>\label{sedf}\<close> (* Hack to make the LaTeX-ing running. Should disappear. *)
|
|
||||||
|
|
||||||
section*[seedf::test_case, dfg=34,fgdfg=zf]{* and another example with attribute setting,
|
|
||||||
but wrong doc_class constraint. *}
|
|
||||||
|
|
||||||
section{* Text Antiquotation Infrastructure ... *}
|
section{* Text Antiquotation Infrastructure ... *}
|
||||||
|
|
||||||
|
@ -94,18 +66,6 @@ text{* @{ec \<open>ass122\<close>} -- global reference to a exported constraint
|
||||||
Note that the link is actually a srac, which, according to
|
Note that the link is actually a srac, which, according to
|
||||||
the ontology, happens to be an "ec". *}
|
the ontology, happens to be an "ec". *}
|
||||||
|
|
||||||
text{* @{test_specification \<open>ass122\<close>} -- wrong: "reference ontologically inconsistent". *}
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
text{* Here is a reference to @{docref \<open>sedf\<close>} *}
|
|
||||||
(* works currently only in connection with the above label-hack.
|
|
||||||
Try to hover over the sedf - link and activate it !!! *)
|
|
||||||
|
|
||||||
|
|
||||||
section{* Miscellaneous ...*}
|
|
||||||
|
|
||||||
section(in order){* sdfsdf*} (* undocumented trouvaille when analysing the code *)
|
|
||||||
|
|
||||||
|
|
||||||
end
|
end
|
||||||
|
|
Binary file not shown.
|
@ -408,6 +408,7 @@ val locale =
|
||||||
Scan.option ((Parse.$$$ "(" -- improper -- Parse.$$$ "in") |--
|
Scan.option ((Parse.$$$ "(" -- improper -- Parse.$$$ "in") |--
|
||||||
Parse.!!! (improper |-- Parse.name --| (improper -- Parse.$$$ ")")));
|
Parse.!!! (improper |-- Parse.name --| (improper -- Parse.$$$ ")")));
|
||||||
|
|
||||||
|
(*
|
||||||
val reference =
|
val reference =
|
||||||
Parse.position Parse.name
|
Parse.position Parse.name
|
||||||
-- Scan.option (Parse.$$$ "::" |-- Parse.!!! (Parse.position Parse.name));
|
-- Scan.option (Parse.$$$ "::" |-- Parse.!!! (Parse.position Parse.name));
|
||||||
|
@ -423,7 +424,7 @@ val attributes =
|
||||||
--| Parse.$$$ "]"
|
--| Parse.$$$ "]"
|
||||||
|
|
||||||
fun convert_meta_args (NONE : ((((string * Position.T) * (string * Position.T) option) * ((string * Position.T) * string) list) option)) = ""
|
fun convert_meta_args (NONE : ((((string * Position.T) * (string * Position.T) option) * ((string * Position.T) * string) list) option)) = ""
|
||||||
|
*)
|
||||||
val meta_args_parser_hook = Unsynchronized.ref((fn thy => fn s => ("",s)): theory -> string parser)
|
val meta_args_parser_hook = Unsynchronized.ref((fn thy => fn s => ("",s)): theory -> string parser)
|
||||||
|
|
||||||
|
|
||||||
|
|
|
@ -0,0 +1,112 @@
|
||||||
|
theory Example
|
||||||
|
imports "../../ontologies/CENELEC_50126"
|
||||||
|
begin
|
||||||
|
|
||||||
|
section{* Some show-off's of general antiquotations. *}
|
||||||
|
|
||||||
|
|
||||||
|
(* some show-off of standard anti-quotations: *)
|
||||||
|
print_attributes
|
||||||
|
print_antiquotations
|
||||||
|
|
||||||
|
text\<open> @{thm refl} of name @{thm [source] refl}
|
||||||
|
@{thm[mode=Rule] conjI}
|
||||||
|
@{file "../../Isa_DOF.thy"}
|
||||||
|
@{value "3+4::int"}
|
||||||
|
@{const hd}
|
||||||
|
@{theory List}}
|
||||||
|
@{term "3"}
|
||||||
|
@{type bool}
|
||||||
|
@{term [show_types] "f x = a + x"} \<close>
|
||||||
|
|
||||||
|
section{* Example *}
|
||||||
|
|
||||||
|
text*[tralala] {* Brexit means Brexit *}
|
||||||
|
|
||||||
|
text*[ass1::assumption] {* Brexit means Brexit *}
|
||||||
|
|
||||||
|
text*[hyp1::hypothesis] {* P inequal NP *}
|
||||||
|
|
||||||
|
|
||||||
|
text*[ass122::srac] {* The overall sampling frequence of the odometer
|
||||||
|
subsystem is therefore 14 khz, which includes sampling, computing and
|
||||||
|
result communication times... *}
|
||||||
|
|
||||||
|
text*[t10::test_result] {* This is a meta-test. This could be an ML-command
|
||||||
|
that governs the external test-execution via, eg., a makefile or specific calls
|
||||||
|
to a test-environment or test-engine *}
|
||||||
|
|
||||||
|
text \<open> @{ec \<open>ass122\<close>}}\<close>
|
||||||
|
|
||||||
|
text \<open> As established by @{docref (unchecked) \<open>t10\<close>},
|
||||||
|
@{docref (define) \<open>t10\<close>} \<close>
|
||||||
|
text \<open> the @{docref \<open>t10\<close>}
|
||||||
|
as well as the @{docref \<open>ass122\<close>}\<close>
|
||||||
|
text \<open> represent a justification of the safety related applicability
|
||||||
|
condition @{srac \<open>ass122\<close>} aka exported constraint @{ec \<open>ass122\<close>}.
|
||||||
|
\<close>
|
||||||
|
|
||||||
|
text{* And some ontologically inconsistent reference: @{hypothesis \<open>ass1\<close>} as well as *}
|
||||||
|
-- wrong
|
||||||
|
|
||||||
|
text{* ... some more ontologically inconsistent reference: @{assumption \<open>hyp1\<close>} as well as *}
|
||||||
|
-- wrong
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
text{* And a further ontologically totally inconsistent reference:
|
||||||
|
@{test_result \<open>ass122\<close>} as well as ... *}
|
||||||
|
-- wrong
|
||||||
|
|
||||||
|
text{* the ontologically inconsistent reference: @{ec \<open>t10\<close>} *}
|
||||||
|
-- wrong
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
section{* Some Tests for Ontology Framework and its CENELEC Instance *}
|
||||||
|
|
||||||
|
declare_reference* [lalala::requirement, alpha="main", beta=42]
|
||||||
|
|
||||||
|
declare_reference* [lalala::quod] (* shouldn't work: multiple declaration *)
|
||||||
|
|
||||||
|
declare_reference* [blablabla::cid, alpha="beta sdf", beta=gamma, delta=dfg_fgh\<^sub>1]
|
||||||
|
|
||||||
|
paragraph*[sdf]{* just a paragraph *}
|
||||||
|
paragraph* [sdfk] \<open> just a paragraph - lexical variant \<close>
|
||||||
|
|
||||||
|
subsection*[sdf]{* shouldn't work, multiple ref. *}
|
||||||
|
|
||||||
|
section*[sedf::requirement, alpja= refl]{* Shouldn't work - misspelled attribute. *}
|
||||||
|
text\<open>\label{sedf}\<close> (* Hack to make the LaTeX-ing running. Should disappear. *)
|
||||||
|
|
||||||
|
section*[seedf::test_case, dfg=34,fgdfg=zf]{* and another example with attribute setting,
|
||||||
|
but wrong doc_class constraint. *}
|
||||||
|
|
||||||
|
section{* Text Antiquotation Infrastructure ... *}
|
||||||
|
|
||||||
|
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{* @{ec \<open>ass122\<close>} -- global reference to a exported constraint in another file.
|
||||||
|
Note that the link is actually a srac, which, according to
|
||||||
|
the ontology, happens to be an "ec". *}
|
||||||
|
|
||||||
|
text{* @{test_specification \<open>ass122\<close>} -- wrong: "reference ontologically inconsistent". *}
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
text{* Here is a reference to @{docref \<open>sedf\<close>} *}
|
||||||
|
(* works currently only in connection with the above label-hack.
|
||||||
|
Try to hover over the sedf - link and activate it !!! *)
|
||||||
|
|
||||||
|
|
||||||
|
section \<open>Miscellaneous\<close>
|
||||||
|
|
||||||
|
section(in order){* sdfsdf*} (* undocumented trouvaille when analysing the code *)
|
||||||
|
|
||||||
|
|
||||||
|
end
|
||||||
|
|
||||||
|
|
Reference in New Issue