--- 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;
--- 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);