--- a/lib/scripts/keywords Fri Jan 04 11:07:39 2013 +0100
+++ b/lib/scripts/keywords Fri Jan 04 11:21:31 2013 +0100
@@ -87,13 +87,13 @@
sub collect_keywords {
while(<STDIN>) {
- if (m/^Outer syntax keyword "([^"]*)" :: (\S*)/) {
+ if (m/^\fOuter syntax keyword "([^"]*)" :: (\S*)/) {
my $name = $1;
my $kind = $2;
if (defined $convert_kinds{$kind}) { $kind = $convert_kinds{$kind} }
&set_keyword($name, $kind);
}
- elsif (m/^Outer syntax keyword "([^"]*)"/) {
+ elsif (m/^\fOuter syntax keyword "([^"]*)"/) {
my $name = $1;
&set_keyword($name, "minor");
}
--- a/src/Pure/Isar/keyword.ML Fri Jan 04 11:07:39 2013 +0100
+++ b/src/Pure/Isar/keyword.ML Fri Jan 04 11:21:31 2013 +0100
@@ -207,9 +207,9 @@
let
val Keywords {lexicons = (minor, _), commands} = get_keywords ();
val _ = sort_strings (Scan.dest_lexicon minor) |> List.app (fn name =>
- writeln ("Outer syntax keyword " ^ quote name));
+ writeln ("\fOuter syntax keyword " ^ quote name));
val _ = sort_wrt #1 (Symtab.dest commands) |> List.app (fn (name, kind) =>
- writeln ("Outer syntax keyword " ^ quote name ^ " :: " ^ kind_of kind));
+ writeln ("\fOuter syntax keyword " ^ quote name ^ " :: " ^ kind_of kind));
in () end;