# HG changeset patch
# User wenzelm
# Date 1516053781 -3600
# Node ID e5ba0ca1e465e9563f0b95eacabc0279658cc4ae
# Parent  78759a7bd874c9c761d65f9320e6611ef951fc38
clarified markup;

diff -r 78759a7bd874 -r e5ba0ca1e465 src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Mon Jan 15 22:46:04 2018 +0100
+++ b/src/Pure/Isar/token.ML	Mon Jan 15 23:03:01 2018 +0100
@@ -289,7 +289,7 @@
   | Alt_String => (Markup.alt_string, "")
   | Verbatim => (Markup.verbatim, "")
   | Cartouche => (Markup.cartouche, "")
-  | Comment NONE => (Markup.comment, "")
+  | Comment _ => (Markup.comment, "")
   | Error msg => (Markup.bad (), msg)
   | _ => (Markup.empty, "");
 
diff -r 78759a7bd874 -r e5ba0ca1e465 src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Mon Jan 15 22:46:04 2018 +0100
+++ b/src/Pure/Syntax/lexicon.ML	Mon Jan 15 23:03:01 2018 +0100
@@ -167,7 +167,7 @@
   | StrSy => Markup.inner_string
   | StringSy => Markup.inner_string
   | Cartouche => Markup.inner_cartouche
-  | Comment NONE => Markup.inner_comment
+  | Comment _ => Markup.inner_comment
   | _ => Markup.empty;
 
 fun report_of_token (Token (kind, s, (pos, _))) =