diff -r ea7c2ee8a47a -r 3390bb8cf681 src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Wed Jul 11 17:47:47 2007 +0200
+++ b/src/Pure/General/markup.ML	Wed Jul 11 17:47:48 2007 +0200
@@ -39,14 +39,13 @@
   val termN: string val term: T
   val keywordN: string val keyword: string -> T
   val commandN: string val command: string -> T
-  val identN: string val ident: T
   val stringN: string val string: T
   val altstringN: string val altstring: T
   val verbatimN: string val verbatim: T
-  val spaceN: string val space: T
   val commentN: string val comment: T
   val controlN: string val control: T
   val malformedN: string val malformed: T
+  val antiqN: string val antiq: T
   val whitespaceN: string val whitespace: T
   val junkN: string val junk: T
   val commandspanN: string val commandspan: string -> T
@@ -54,9 +53,9 @@
   val stateN: string val state: T
   val subgoalN: string val subgoal: T
   val default_output: T -> output * output
+  val add_mode: string -> (T -> output * output) -> unit
   val output: T -> output * output
   val enclose: T -> output -> output
-  val add_mode: string -> (T -> output * output) -> unit
 end;
 
 structure Markup: MARKUP =
@@ -129,15 +128,15 @@
 val (keywordN, keyword) = markup_string "keyword" nameN;
 val (commandN, command) = markup_string "command" nameN;
 
-val (identN, ident) = markup "ident";
 val (stringN, string) = markup "string";
 val (altstringN, altstring) = markup "altstring";
 val (verbatimN, verbatim) = markup "verbatim";
-val (spaceN, space) = markup "space";
 val (commentN, comment) = markup "comment";
 val (controlN, control) = markup "control";
 val (malformedN, malformed) = markup "malformed";
 
+val (antiqN, antiq) = markup "antiq";
+
 val (whitespaceN, whitespace) = markup "whitespace";
 val (junkN, junk) = markup "junk";
 val (commandspanN, commandspan) = markup_string "commandspan" nameN;
@@ -164,9 +163,8 @@
     the_default default (Library.get_first (Symtab.lookup (! modes)) (! print_mode));
 end;
 
-fun output m =
-  if m = none then ("", "")
-  else #output (get_mode ()) m;
+fun output ("", _) = ("", "")
+  | output m = #output (get_mode ()) m;
 
 val enclose = output #-> Library.enclose;