Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
clarified markup;
authorwenzelm
Mon, 15 Jan 2018 23:03:01 +0100
changeset 67440 e5ba0ca1e465
parent 67439 78759a7bd874
child 67441 cafbb63f10e5
clarified markup;
src/Pure/Isar/token.ML file | annotate | diff | comparison | revisions
src/Pure/Syntax/lexicon.ML file | annotate | diff | comparison | revisions 
--- 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, "");
 
--- 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, _))) =
isabelle