From 43c857af2c2c93ae230fccfba345dfe9eb0dd5c6 Mon Sep 17 00:00:00 2001 From: Burkhart Wolff Date: Fri, 17 Jun 2022 20:35:32 +0200 Subject: [PATCH] roughly ported Latex testbench to 21-1 --- src/tests/OutOfOrderPresntn.thy | 59 ++++++++++++++++++--------------- 1 file changed, 33 insertions(+), 26 deletions(-) diff --git a/src/tests/OutOfOrderPresntn.thy b/src/tests/OutOfOrderPresntn.thy index 4caf8b8..97a1de8 100644 --- a/src/tests/OutOfOrderPresntn.thy +++ b/src/tests/OutOfOrderPresntn.thy @@ -33,16 +33,15 @@ Symtab.dest docitem_tab; Symtab.dest docclass_tab; \ - +ML\open Document_Output;\ +ML\open XML; XML.string_of\ ML\ -Pure_Syn.document_command; -val _ = Thy_Output.output_document +val _ = Document_Output.document_output -fun gen_enriched_document_command2 cid_transform attr_transform - markdown - (((((oid,pos),cid_pos), doc_attrs) : ODL_Command_Parser.meta_args_t, +fun gen_enriched_document_command2 name {body} cid_transform attr_transform markdown + (((((oid,pos),cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t, xstring_opt:(xstring * Position.T) option), toks:Input.source) : theory -> theory = @@ -54,23 +53,29 @@ fun gen_enriched_document_command2 cid_transform attr_transform val _ = Context_Position.reports ctxt [(pos, Markup.language_document (Input.is_delimited toks)), (pos, Markup.plain_text)]; + fun markup xml = let val m = if body then Markup.latex_body + else Markup.latex_heading + in [XML.Elem (m (Latex.output_name name), + xml)] end; - val text = Thy_Output.output_document + val text = Document_Output.output_document (Proof_Context.init_global thy) markdown toks +(* type file = {path: Path.T, pos: Position.T, content: string} *) + val strg = XML.string_of (hd (Latex.output text)) val file = {path = Path.make [oid ^ "_snippet.tex"], pos = @{here}, - content = Latex.output_text text} - + content = strg} + val _ = Generated_Files.write_file (Path.make ["latex_test"]) file - val _ = writeln (Latex.output_text text) + val _ = writeln (strg) in thy end (* ... generating the level-attribute syntax *) in - ( ODL_Command_Parser.create_and_check_docitem + ( Value_Command.Docitem_Parser.create_and_check_docitem {is_monitor = false} {is_inline = false} oid pos (cid_transform cid_pos) (attr_transform doc_attrs) #> check_n_tex_text ) @@ -78,8 +83,8 @@ fun gen_enriched_document_command2 cid_transform attr_transform 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} ))); + (ODL_Meta_Args_Parser.attributes -- Parse.opt_target -- Parse.document_source + >> (Toplevel.theory o (gen_enriched_document_command2 "TTT" {body=true} I I {markdown = true} ))); (* copied from Pure_syn for experiments *) @@ -91,9 +96,11 @@ fun output_document2 state markdown txt = Context_Position.reports ctxt [(pos, Markup.language_document (Input.is_delimited txt)), (pos, Markup.plain_text)]; - val txt' = Thy_Output.output_document ctxt markdown txt - val _ = writeln (Latex.output_text txt') - in Thy_Output.output_document ctxt markdown txt end; + val txt' = Document_Output.output_document ctxt markdown txt + val strg = XML.string_of (hd (Latex.output txt')) + + val _ = writeln (strg) + in Document_Output.output_document ctxt markdown txt end; fun document_command2 markdown (loc, txt) = Toplevel.keep (fn state => @@ -104,7 +111,7 @@ fun document_command2 markdown (loc, txt) = ^ Position.here pos))) o Toplevel.present_local_theory loc - (fn state => ignore (output_document2 state markdown txt)); + (fn state => (output_document2 state markdown txt)); val _ = @@ -121,7 +128,7 @@ Tool: Sphinx. \ -text*[aaa::B]\dfg @{thm [display] refl}\ +text*[aaaa::B]\dfg @{thm [display] refl}\ text-[dfgdfg::B] \ Lorem ipsum ... @{thm [display] refl} _ Frédéric \textbf{TEST} \verb+sdf+ \dfgdfg\ \ @@ -174,9 +181,9 @@ text\Std Abbreviations. Inspired by the block *\control spacing\ val _ = Theory.setup - ( Thy_Output.antiquotation_raw \<^binding>\doof\ (Scan.succeed ()) + ( Document_Output.antiquotation_raw \<^binding>\doof\ (Scan.succeed ()) (fn _ => fn () => Latex.string "\\emph{doof}") - #> Thy_Output.antiquotation_raw \<^binding>\LATEX\ (Scan.succeed ()) + #> Document_Output.antiquotation_raw \<^binding>\LATEX\ (Scan.succeed ()) (fn _ => fn () => Latex.string "\\textbf{LaTeX}") ) \ @@ -220,8 +227,8 @@ fun prepare_text ctxt = fun string_2_text_antiquotation ctxt text = prepare_text ctxt text - |> Thy_Output.output_source ctxt - |> Thy_Output.isabelle ctxt + |> Document_Output.output_source ctxt + |> Document_Output.isabelle ctxt fun string_2_theory_text_antiquotation ctxt text = let @@ -229,12 +236,12 @@ fun string_2_theory_text_antiquotation ctxt text = in prepare_text ctxt text |> Token.explode0 keywords - |> maps (Thy_Output.output_token ctxt) - |> Thy_Output.isabelle ctxt + |> maps (Document_Output.output_token ctxt) + |> Document_Output.isabelle ctxt end fun gen_text_antiquotation name reportNcheck compile = - Thy_Output.antiquotation_raw_embedded name (Scan.lift Args.text_input) + Document_Output.antiquotation_raw_embedded name (Scan.lift Args.text_input) (fn ctxt => fn text:Input.source => let val _ = reportNcheck ctxt text; @@ -287,7 +294,7 @@ fun theory_text_antiquotation name = fun enclose_env ctxt block_env body = if Config.get ctxt Document_Antiquotation.thy_output_display - then Latex.environment_block block_env [body] + then Latex.environment block_env body else body;