aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorterru2025-09-24 16:56:22 +0200
committerterru2025-09-24 16:56:53 +0200
commitcf2bc14614eb94575d5949d8a693d9057dcfe34f (patch)
tree7a2448bafb0b333f93945483f29534e6c2ba343b
parent2f031e360bc8bd0621e6e79d3a5f732548d920c7 (diff)
fix: hash names in case of spaces in first command argHEADmain
-rw-r--r--Latex.thy2
1 files changed, 1 insertions, 1 deletions
diff --git a/Latex.thy b/Latex.thy
index 81f582d..d28fc82 100644
--- a/Latex.thy
+++ b/Latex.thy
@@ -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);