# HG changeset patch # User wenzelm # Date 1357294891 -3600 # Node ID 2af9e4614ba4eb3b840d508414910b723b1b0441 # Parent dae523e6198bc91b1940bcaef0f5d60e1e27fe5c more formal inlining of system information; diff -r dae523e6198b -r 2af9e4614ba4 lib/scripts/keywords --- 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() { - 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"); } diff -r dae523e6198b -r 2af9e4614ba4 src/Pure/Isar/keyword.ML --- 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;