equal
deleted
inserted
replaced
102 if invisible_token tok then "" |
102 if invisible_token tok then "" |
103 else if T.is_kind T.Command tok then |
103 else if T.is_kind T.Command tok then |
104 "\\isacommand{" ^ output_syms s ^ "}" |
104 "\\isacommand{" ^ output_syms s ^ "}" |
105 else if T.is_kind T.Keyword tok andalso Syntax.is_ascii_identifier s then |
105 else if T.is_kind T.Keyword tok andalso Syntax.is_ascii_identifier s then |
106 "\\isakeyword{" ^ output_syms s ^ "}" |
106 "\\isakeyword{" ^ output_syms s ^ "}" |
107 else if T.is_kind T.String tok then output_syms (Library.quote s) |
107 else if T.is_kind T.String tok then |
|
108 enclose "{\\isachardoublequoteopen}" "{\\isachardoublequoteclose}" (output_syms s) |
|
109 else if T.is_kind T.AltString tok then |
|
110 enclose "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}" (output_syms s) |
108 else if T.is_kind T.Verbatim tok then output_syms (enclose "{*" "*}" s) |
111 else if T.is_kind T.Verbatim tok then output_syms (enclose "{*" "*}" s) |
109 else output_syms s |
112 else output_syms s |
110 end; |
113 end; |
111 |
114 |
112 fun output_markup cmd txt = "%\n\\isamarkup" ^ cmd ^ "{" ^ Symbol.strip_blanks txt ^ "%\n}\n"; |
115 fun output_markup cmd txt = "%\n\\isamarkup" ^ cmd ^ "{" ^ Symbol.strip_blanks txt ^ "%\n}\n"; |