added meta_args transmission
HOL-OCL/Isabelle_DOF/Isabelle2018 There was a failure building this commit
Details
HOL-OCL/Isabelle_DOF/Isabelle2018 There was a failure building this commit
Details
This commit is contained in:
parent
4e4d1a1aad
commit
d4bb579e09
|
@ -198,7 +198,7 @@ fun present_token ctxt tok =
|
|||
(output_document ctxt {markdown = false} source)
|
||||
| Markup_Env_Token (cmd, meta_args, source) =>
|
||||
[Latex.environment_block
|
||||
("isamarkup" ^ cmd)
|
||||
("isamarkup" ^ cmd ^ meta_args)
|
||||
(Latex.string meta_args :: output_document ctxt {markdown = true} source)]
|
||||
| Raw_Token source =>
|
||||
Latex.string "%\n" :: output_document ctxt {markdown = true} source @ [Latex.string "\n"]);
|
||||
|
|
Loading…
Reference in New Issue