clarified signature;
authorwenzelm
Sun Mar 24 17:33:11 2019 +0100 (4 weeks ago)
changeset 69966cba5b866c633
parent 69965 da5e7278286b
child 69967 8a9d0d894ec0
clarified signature;
src/Pure/General/comment.ML
src/Pure/Thy/thy_output.ML
     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  
     2.1 --- a/src/Pure/Thy/thy_output.ML	Sun Mar 24 17:24:24 2019 +0100
     2.2 +++ b/src/Pure/Thy/thy_output.ML	Sun Mar 24 17:33:11 2019 +0100
     2.3 @@ -161,7 +161,7 @@
     2.4        val pos = #1 (Symbol_Pos.range syms);
     2.5        val _ =
     2.6          comment |> Option.app (fn kind =>
     2.7 -          Context_Position.reports ctxt (map (pair pos) (Markup.cartouche :: Comment.markups kind)));
     2.8 +          Context_Position.reports ctxt (map (pair pos) (Comment.kind_markups kind)));
     2.9        val _ = output_comment_symbols ctxt {antiq = false} (comment, syms);
    2.10      in if comment = SOME Comment.Comment then check_comments ctxt syms else () end);
    2.11