Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

Restructured arguments for LaTeX invironments.

This commit is contained in:
Achim D. Brucker 2018-09-18 14:26:19 +01:00
parent da7f286dd5
commit 1382d7c600
1 changed files with 4 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
Isa_DOF.thy
View File

@ -610,13 +610,15 @@ fun meta_args_2_string thy ((((lab, _), cid_opt), attr_list) : meta_args_t) =
NONE => DOF_core.default_cid
| SOME(cid,_) => DOF_core.name2doc_class_name thy cid
val cid_txt = "type = " ^ (enclose "{" "}" cid_long);
fun markup2string x = XML.content_of (YXML.parse_body x)
fun markup2string x = YXML.content_of x
fun toLong n = #long_name(the(DOF_core.get_attribute_info cid_long (markup2string n) thy))
fun str ((lhs,_),rhs) = (toLong lhs)^" = "^(enclose "{" "}" (markup2string rhs))
(* no normalization on lhs (could be long-name)
no paraphrasing on rhs (could be fully paranthesized
pretty-printed formula in LaTeX notation ... *)
in enclose "[" "]" (commas ([l,cid_txt] @ (map str attr_list ))) end
in
enclose "[" "]" (String.concat [ cid_txt, ", args={", (commas ([cid_txt,l] @ (map str attr_list ))), "}"])
end
val semi = Scan.option (Parse.$$$ ";");