more formal inlining of system information;
authorwenzelm
Fri, 04 Jan 2013 11:21:31 +0100
changeset 50714 2af9e4614ba4
parent 50713 dae523e6198b
child 50715 8cfd585b9162
more formal inlining of system information;
lib/scripts/keywords
src/Pure/Isar/keyword.ML
--- 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;