diff options
| -rw-r--r-- | Latex.thy | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -44,7 +44,7 @@ fun export_snippet searchterm lthy = Thy_Info.add_presentation (fn {options, seg |> map (fn sym => if Symbol.is_ascii_letter sym orelse Symbol.is_ascii_digit sym then sym else if Symbol.is_printable sym then "-" else "") - val looks_like_name = not (exists (Symbol.is_blank) symbols) andalso length symbols <> 0; + val looks_like_name = not (exists (Symbol.is_blank) (Symbol.explode name)) andalso length symbols <> 0; val command_name = Toplevel.name_of command in (not looks_like_name, command_name ^ ":" ^ (if looks_like_name then String.concat symbols else "")) end); |