src/Doc/Isar_Ref/document/showsymbols
changeset 67146 909dcdec2122
parent 63676 88727334666e
     1.1 --- a/src/Doc/Isar_Ref/document/showsymbols	Wed Dec 06 14:19:36 2017 +0100
     1.2 +++ b/src/Doc/Isar_Ref/document/showsymbols	Wed Dec 06 15:46:35 2017 +0100
     1.3 @@ -5,13 +5,8 @@
     1.4  $eol = "&";
     1.5  
     1.6  while (<ARGV>) {
     1.7 -    if (m/^\\newcommand\{\\(isasym|isactrl)([A-Za-z]+)\}/) {
     1.8 -        if ($1 eq "isasym") {
     1.9 -            print "\\verb,\\<$2>, & {\\isasym$2} $eol\n";
    1.10 -        }
    1.11 -        else {
    1.12 -            print "\\verb,\\<^$2>, & {\\isactrl$2} $eol\n";
    1.13 -        }
    1.14 +    if (m/^\\newcommand\{\\isasym([A-Za-z]+)\}/) {
    1.15 +        print "\\verb,\\<$1>, & {\\isasym$1} $eol\n";
    1.16          if ("$eol" eq "&") {
    1.17              $eol = "\\\\";
    1.18          } else {