equal
deleted
inserted
replaced
138 val is_long_identifier = forall Symbol_Pos.is_identifier o Long_Name.explode |
138 val is_long_identifier = forall Symbol_Pos.is_identifier o Long_Name.explode |
139 fun maybe_quote y = |
139 fun maybe_quote y = |
140 let val s = unyxml y in |
140 let val s = unyxml y in |
141 y |> ((not (is_long_identifier (unquote_tvar s)) andalso |
141 y |> ((not (is_long_identifier (unquote_tvar s)) andalso |
142 not (is_long_identifier (unquery_var s))) orelse |
142 not (is_long_identifier (unquery_var s))) orelse |
143 Keyword.is_keyword s) ? quote |
143 Keyword.is_keyword (Keyword.get_keywords ()) s) ? quote |
144 end |
144 end |
145 |
145 |
146 fun string_of_ext_time (plus, time) = |
146 fun string_of_ext_time (plus, time) = |
147 let val us = Time.toMicroseconds time in |
147 let val us = Time.toMicroseconds time in |
148 (if plus then "> " else "") ^ |
148 (if plus then "> " else "") ^ |