First version with inner-syntax checking infrastructure with just

one inner syntax antiquotation: file. Works on some examples.
2018-09-06 12:07:37 +02:00 · 2018-09-06 12:07:37 +02:00 · bb9c5a4f24
parent 718b6ae1f0
commit bb9c5a4f24
1 changed files with 15 additions and 0 deletions
--- a/examples/conceptual/InnerSyntaxAntiquotations.thy
+++ b/examples/conceptual/InnerSyntaxAntiquotations.thy
@ -0,0 +1,15 @@
+theory InnerSyntaxAntiquotations
+  imports "../../ontologies/Conceptual"
+begin
+
+ML\<open>
+val ({tab = x, ...},y,z)= DOF_core.get_data @{context};
+
+Symtab.dest z;
+
+\<close>
+
+text*[xcv::F, u="@{file ''./examples/conceptual/Attributes.thy''}"]\<open>Lorem ipsum ...\<close>
+
+
+end