# HG changeset patch
# User wenzelm
# Date 1218570539 -7200
# Node ID 2828a276dc9330ea96495a35c8cc668904dcca79
# Parent  141772c866c9ad99f0aad9967b619943092d3531
token_kind_markup: complete coverage;

diff -r 141772c866c9 -r 2828a276dc93 src/Pure/Thy/thy_edit.ML
--- a/src/Pure/Thy/thy_edit.ML	Tue Aug 12 21:28:09 2008 +0200
+++ b/src/Pure/Thy/thy_edit.ML	Tue Aug 12 21:48:59 2008 +0200
@@ -52,24 +52,25 @@
 local
 
 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.Comment   => Markup.comment
-  | T.Sync      => Markup.control
-  | T.Malformed => Markup.malformed
-  | T.Error _   => Markup.malformed
-  | T.EOF       => Markup.control
-  | _           => Markup.none;
+ 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.none
+  | T.Comment       => Markup.comment
+  | T.InternalValue => Markup.none
+  | T.Malformed     => Markup.malformed
+  | T.Error _       => Markup.malformed
+  | T.Sync          => Markup.control
+  | T.EOF           => Markup.control;
 
 in