# HG changeset patch
# User wenzelm
# Date 1184106592 -7200
# Node ID 8866c87d1a163a2af26db346cb43555b670eafd2
# Parent  d1ba656978c5ba822c6a2bb85388981915534855
treat OuterLex.Error;

diff -r d1ba656978c5 -r 8866c87d1a16 src/Pure/Thy/thy_edit.ML
--- a/src/Pure/Thy/thy_edit.ML	Wed Jul 11 00:29:51 2007 +0200
+++ b/src/Pure/Thy/thy_edit.ML	Wed Jul 11 00:29:52 2007 +0200
@@ -67,23 +67,24 @@
 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.Space       => Markup.space
-  | T.Comment     => Markup.comment
-  | T.Sync        => Markup.control
-  | T.Malformed _ => Markup.malformed
-  | T.EOF         => Markup.control;
+ 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;
 
 fun present_token tok =
   Markup.enclose (token_kind_markup (T.kind_of tok)) (Output.output (T.unparse tok));