src/Doc/Isar_Ref/document/showsymbols
changeset 63676 88727334666e
parent 56451 856492b0f755
child 67146 909dcdec2122
--- a/src/Doc/Isar_Ref/document/showsymbols	Fri Aug 12 14:19:27 2016 +0200
+++ b/src/Doc/Isar_Ref/document/showsymbols	Fri Aug 12 15:25:25 2016 +0200
@@ -5,11 +5,13 @@
 $eol = "&";
 
 while (<ARGV>) {
-    if (m/^\\newcommand\{\\isasym([A-Za-z]+)\}/) {
-       print "\\verb,\\<$1>, & {\\isasym$1} $eol\n";
-#       print "\\verb,\\<$1>, & \\isactrlbold{\\isasym$1}~{\\isasym$1} $eol\n";
-#       print "\\verb,\\<$1>, & B\\isactrlsup{\\isasym$1} $eol\n";
-#       print "\\verb,\\<$1>, & B\\isactrlsub{\\isasym$1} $eol\n";
+    if (m/^\\newcommand\{\\(isasym|isactrl)([A-Za-z]+)\}/) {
+        if ($1 eq "isasym") {
+            print "\\verb,\\<$2>, & {\\isasym$2} $eol\n";
+        }
+        else {
+            print "\\verb,\\<^$2>, & {\\isactrl$2} $eol\n";
+        }
         if ("$eol" eq "&") {
             $eol = "\\\\";
         } else {