src/Pure/General/comment.ML
changeset 69966 cba5b866c633
parent 69965 da5e7278286b
child 69968 1a400b14fd3a
     1.1 --- a/src/Pure/General/comment.ML	Sun Mar 24 17:24:24 2019 +0100
     1.2 +++ b/src/Pure/General/comment.ML	Sun Mar 24 17:33:11 2019 +0100
     1.3 @@ -7,7 +7,7 @@
     1.4  signature COMMENT =
     1.5  sig
     1.6    datatype kind = Comment | Cancel | Latex | Marker
     1.7 -  val markups: kind -> Markup.T list
     1.8 +  val kind_markups: kind -> Markup.T list
     1.9    val is_symbol: Symbol.symbol -> bool
    1.10    val scan_comment: (kind * Symbol_Pos.T list) scanner
    1.11    val scan_cancel: (kind * Symbol_Pos.T list) scanner
    1.12 @@ -41,7 +41,8 @@
    1.13  
    1.14  val get_kind = the o AList.lookup (op =) kinds;
    1.15  val print_kind = quote o #symbol o get_kind;
    1.16 -val markups = #markups o get_kind;
    1.17 +
    1.18 +fun kind_markups kind = Markup.cartouche :: #markups (get_kind kind);
    1.19  
    1.20  fun is_symbol sym = exists (fn (_, {symbol, ...}) => symbol = sym) kinds;
    1.21