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