# HG changeset patch
# User wenzelm
# Date 1184168872 -7200
# Node ID 97e41d1683115ad0a50644e19b89eff38977b7b4
# Parent  1993b865c5ac5cc6b061a231e18670bccc3942e5
tuned markup;

diff -r 1993b865c5ac -r 97e41d168311 src/Pure/Thy/thy_edit.ML
--- a/src/Pure/Thy/thy_edit.ML	Wed Jul 11 17:47:51 2007 +0200
+++ b/src/Pure/Thy/thy_edit.ML	Wed Jul 11 17:47:52 2007 +0200
@@ -69,22 +69,15 @@
 val token_kind_markup =
  fn T.Command   => (Markup.commandN, [])
   | T.Keyword   => (Markup.keywordN, [])
-  | T.Ident     => Markup.ident
-  | T.LongIdent => Markup.ident
-  | T.SymIdent  => Markup.ident
-  | T.Var       => Markup.ident
-  | T.TypeIdent => Markup.ident
-  | T.TypeVar   => Markup.ident
-  | T.Nat       => Markup.ident
   | T.String    => Markup.string
   | T.AltString => Markup.altstring
   | T.Verbatim  => Markup.verbatim
-  | T.Space     => Markup.space
   | T.Comment   => Markup.comment
   | T.Sync      => Markup.control
   | T.Malformed => Markup.malformed
   | T.Error _   => Markup.malformed
-  | T.EOF       => Markup.control;
+  | T.EOF       => Markup.control
+  | _           => Markup.none;
 
 fun present_token tok =
   Markup.enclose (token_kind_markup (T.kind_of tok)) (Output.output (T.unparse tok));