diff --git a/src/tests/OutOfOrderPresntn.thy b/src/tests/OutOfOrderPresntn.thy new file mode 100644 index 00000000..01458687 --- /dev/null +++ b/src/tests/OutOfOrderPresntn.thy @@ -0,0 +1,94 @@ +(************************************************************************* + * Copyright (C) + * 2019 The University of Exeter + * 2018-2019 The University of Paris-Saclay + * 2018 The University of Sheffield + * + * License: + * This program can be redistributed and/or modified under the terms + * of the 2-clause BSD-style license. + * + * SPDX-License-Identifier: BSD-2-Clause + *************************************************************************) + +theory + OutOfOrderPresntn +imports + "Isabelle_DOF.Conceptual" +keywords "text-" :: document_body +begin + +section\Elementary Creation of Doc-items and Access of their Attibutes\ + + +text\Current status:\ +print_doc_classes +print_doc_items + +(* this corresponds to low-level accesses : *) +ML\ +val {docobj_tab={tab = docitem_tab, ...},docclass_tab, ISA_transformer_tab, monitor_tab,...} + = DOF_core.get_data @{context}; +Symtab.dest docitem_tab; +Symtab.dest docclass_tab; +\ + + + +ML\ +Pure_Syn.document_command; + +fun output_document state markdown src = + let + val ctxt = Toplevel.presentation_context state; + val _ = Context_Position.report ctxt + (Input.pos_of src) + (Markup.language_document (Input.is_delimited src)); + in Thy_Output.output_document ctxt markdown src end; + (* this thing converts also source to (latex) text ... *) + +output_document : Toplevel.state -> {markdown: bool} -> Input.source -> Latex.text list; + + +fun gen_enriched_document_command2 cid_transform attr_transform + markdown + (((((oid,pos),cid_pos), doc_attrs) : ODL_Command_Parser.meta_args_t, + xstring_opt:(xstring * Position.T) option), + toks:Input.source) + : theory -> theory = + let val toplvl = Toplevel.theory_toplevel + + (* as side-effect, generates markup *) + fun check_n_tex_text thy = let val text = output_document (toplvl thy) markdown toks + val file = {path = Path.make [oid ^ "_snippet.tex"], + pos = @{here}, + content = Latex.output_text text} + val _ = Generated_Files.write_file (Path.make ["latex_test"]) file + val _ = writeln (Latex.output_text text) + in thy end + + (* ... generating the level-attribute syntax *) + in + ( ODL_Command_Parser.create_and_check_docitem false oid pos (cid_transform cid_pos) (attr_transform doc_attrs) + #> check_n_tex_text ) + end; + +val _ = + Outer_Syntax.command ("text-", @{here}) "formal comment macro" + (ODL_Command_Parser.attributes -- Parse.opt_target -- Parse.document_source + >> (Toplevel.theory o (gen_enriched_document_command2 I I {markdown = true} ))); + +\ + + +text\And here a tex - text macro.\ + +text-[dfgdfg::B]\ Lorem ipsum ... @{thm refl} \ + +(*<*) +text\Final Status:\ +print_doc_items +print_doc_classes + +end +(*>*)