# 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(<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");
     }
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;