lib/scripts/keywords
changeset 36316 f9b45eac4c60
parent 35022 c844b93dd147
child 46967 499d9bbd8de9
equal deleted inserted replaced
36315:e859879079c8 36316:f9b45eac4c60
    37       &set_keyword($name, "minor");
    37       &set_keyword($name, "minor");
    38     }
    38     }
    39     elsif (m/^Outer syntax command:\s*"(.*)"\s*\((.*)\)/) {
    39     elsif (m/^Outer syntax command:\s*"(.*)"\s*\((.*)\)/) {
    40       my $name = $1;
    40       my $name = $1;
    41       my $kind = $2;
    41       my $kind = $2;
       
    42       if ($kind eq "theory-schematic-goal") { $kind = "theory-goal"; }
    42       &set_keyword($name, $kind);
    43       &set_keyword($name, $kind);
    43     }
    44     }
    44   }
    45   }
    45 }
    46 }
    46 
    47