# HG changeset patch
# User wenzelm
# Date 1553445191 -3600
# Node ID cba5b866c633f76f9c3eaa30aa87d9f2a30c6cb4
# Parent  da5e7278286b0616f4679e7ebdedc00b96b2c1fc
clarified signature;

diff -r da5e7278286b -r cba5b866c633 src/Pure/General/comment.ML
--- a/src/Pure/General/comment.ML	Sun Mar 24 17:24:24 2019 +0100
+++ b/src/Pure/General/comment.ML	Sun Mar 24 17:33:11 2019 +0100
@@ -7,7 +7,7 @@
 signature COMMENT =
 sig
   datatype kind = Comment | Cancel | Latex | Marker
-  val markups: kind -> Markup.T list
+  val kind_markups: kind -> Markup.T list
   val is_symbol: Symbol.symbol -> bool
   val scan_comment: (kind * Symbol_Pos.T list) scanner
   val scan_cancel: (kind * Symbol_Pos.T list) scanner
@@ -41,7 +41,8 @@
 
 val get_kind = the o AList.lookup (op =) kinds;
 val print_kind = quote o #symbol o get_kind;
-val markups = #markups o get_kind;
+
+fun kind_markups kind = Markup.cartouche :: #markups (get_kind kind);
 
 fun is_symbol sym = exists (fn (_, {symbol, ...}) => symbol = sym) kinds;
 
diff -r da5e7278286b -r cba5b866c633 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Sun Mar 24 17:24:24 2019 +0100
+++ b/src/Pure/Thy/thy_output.ML	Sun Mar 24 17:33:11 2019 +0100
@@ -161,7 +161,7 @@
       val pos = #1 (Symbol_Pos.range syms);
       val _ =
         comment |> Option.app (fn kind =>
-          Context_Position.reports ctxt (map (pair pos) (Markup.cartouche :: Comment.markups kind)));
+          Context_Position.reports ctxt (map (pair pos) (Comment.kind_markups kind)));
       val _ = output_comment_symbols ctxt {antiq = false} (comment, syms);
     in if comment = SOME Comment.Comment then check_comments ctxt syms else () end);