equal
deleted
inserted
replaced
68 |
68 |
69 val subscript = implode o map (prefix "\<^isub>") o explode |
69 val subscript = implode o map (prefix "\<^isub>") o explode |
70 fun nat_subscript n = |
70 fun nat_subscript n = |
71 n |> string_of_int |> print_mode_active Symbol.xsymbolsN ? subscript |
71 n |> string_of_int |> print_mode_active Symbol.xsymbolsN ? subscript |
72 |
72 |
73 fun plain_string_from_xml_tree t = |
73 val unyxml = XML.content_of o YXML.parse_body |
74 Buffer.empty |> XML.add_content t |> Buffer.content |
|
75 val unyxml = plain_string_from_xml_tree o YXML.parse |
|
76 |
74 |
77 val is_long_identifier = forall Syntax.is_identifier o space_explode "." |
75 val is_long_identifier = forall Syntax.is_identifier o space_explode "." |
78 fun maybe_quote y = |
76 fun maybe_quote y = |
79 let val s = unyxml y in |
77 let val s = unyxml y in |
80 y |> ((not (is_long_identifier (perhaps (try (unprefix "'")) s)) andalso |
78 y |> ((not (is_long_identifier (perhaps (try (unprefix "'")) s)) andalso |