diff --git a/examples/technical_report/Isabelle_DOF-Manual/Isabelle_DOF-Manual.thy b/examples/technical_report/Isabelle_DOF-Manual/Isabelle_DOF-Manual.thy index d8c0fed..a19ad05 100755 --- a/examples/technical_report/Isabelle_DOF-Manual/Isabelle_DOF-Manual.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/Isabelle_DOF-Manual.thy @@ -19,6 +19,8 @@ close_monitor*[this] check_doc_global text\Resulting trace in \<^verbatim>\doc_item\ ''this'': \ ML\@{trace_attribute this}\ + + end (*>*) diff --git a/src/DOF/Isa_COL.thy b/src/DOF/Isa_COL.thy index e13af5c..f6273f3 100755 --- a/src/DOF/Isa_COL.thy +++ b/src/DOF/Isa_COL.thy @@ -241,10 +241,47 @@ setup\\ section\Tables\ (* TODO ! ! ! *) (* dito the future monitor: table - block *) +(* some studies *) +ML\ +local + +fun mk_line st1 st2 [a] = [a @ [Latex.string st2]] + |mk_line st1 st2 (a::S) = [a @ [Latex.string st1]] @ mk_line st1 st2 S; + +fun table_antiquotation name = + Thy_Output.antiquotation_raw_embedded name + (Scan.repeat1(Scan.repeat1(Scan.lift Args.cartouche_input))) + (fn ctxt => + (fn content:Input.source list list => + let fun check _ = () (* ToDo *) + val _ = check content + in content + |> (map(map (Thy_Output.output_document ctxt {markdown = false}) + #> mk_line "&" "\\\\" + #> List.concat ) + #> List.concat) + |> Latex.enclose_block "\\table[allerhandquatsch]{" "}" + end + ) + ); + +in + +val _ = + Theory.setup (table_antiquotation \<^binding>\table_inline\ ); + +end +\ + section\Tests\ - +(*<*) +text\ @{table_inline [display] + \\\dfg\\dfg\\dfg\\ + \\1\ \2\ \3\\ + \}\ +(*>*) ML\@{term "side_by_side_figure"}; @{typ "doc_class rexp"}; DOF_core.SPY;\ diff --git a/src/ontologies/CENELEC_50128/CENELEC_50128.thy b/src/ontologies/CENELEC_50128/CENELEC_50128.thy index f4496ba..02fe9fd 100755 --- a/src/ontologies/CENELEC_50128/CENELEC_50128.thy +++ b/src/ontologies/CENELEC_50128/CENELEC_50128.thy @@ -319,7 +319,7 @@ section\Objectives, Conformance and Software Integrity Levels\ datatype sil = SIL0 | SIL1 | SIL2 | SIL3 | SIL4 -type_synonym saftety_integraytion_level = sil +type_synonym safety_integration_level = sil doc_class objectives =