src/Pure/General/comment.ML
author wenzelm
Sun Mar 24 17:53:46 2019 +0100 (2 months ago)
changeset 69968 1a400b14fd3a
parent 69966 cba5b866c633
child 70229 c03f381fd373
permissions -rw-r--r--
clarified spell-checking (see also 30233285270a);
     1 (*  Title:      Pure/General/comment.ML
     2     Author:     Makarius
     3 
     4 Formal comments.
     5 *)
     6 
     7 signature COMMENT =
     8 sig
     9   datatype kind = Comment | Cancel | Latex | Marker
    10   val kind_markups: kind -> Markup.T list
    11   val is_symbol: Symbol.symbol -> bool
    12   val scan_comment: (kind * Symbol_Pos.T list) scanner
    13   val scan_cancel: (kind * Symbol_Pos.T list) scanner
    14   val scan_latex: (kind * Symbol_Pos.T list) scanner
    15   val scan_marker: (kind * Symbol_Pos.T list) scanner
    16   val scan_inner: (kind * Symbol_Pos.T list) scanner
    17   val scan_outer: (kind * Symbol_Pos.T list) scanner
    18   val read_body: Symbol_Pos.T list -> (kind option * Symbol_Pos.T list) list
    19 end;
    20 
    21 structure Comment: COMMENT =
    22 struct
    23 
    24 (* kinds *)
    25 
    26 datatype kind = Comment | Cancel | Latex | Marker;
    27 
    28 val kinds =
    29   [(Comment,
    30      {symbol = Symbol.comment, blanks = true,
    31       markups = [Markup.language_document true, Markup.plain_text]}),
    32    (Cancel,
    33      {symbol = Symbol.cancel, blanks = false,
    34       markups = [Markup.language_text true, Markup.raw_text]}),
    35    (Latex,
    36      {symbol = Symbol.latex, blanks = false,
    37       markups = [Markup.language_latex true, Markup.raw_text]}),
    38    (Marker,
    39      {symbol = Symbol.marker, blanks = false,
    40       markups = [Markup.language_document_marker]})];
    41 
    42 val get_kind = the o AList.lookup (op =) kinds;
    43 val print_kind = quote o #symbol o get_kind;
    44 
    45 fun kind_markups kind = Markup.cartouche :: #markups (get_kind kind);
    46 
    47 fun is_symbol sym = exists (fn (_, {symbol, ...}) => symbol = sym) kinds;
    48 
    49 
    50 (* scan *)
    51 
    52 local
    53 
    54 open Basic_Symbol_Pos;
    55 
    56 val err_prefix = "Error in formal comment: ";
    57 
    58 val scan_blanks = Scan.many (Symbol.is_blank o Symbol_Pos.symbol);
    59 
    60 fun scan_symbol kind =
    61   let val {blanks, symbol, ...} = get_kind kind
    62   in if blanks then $$$ symbol @@@ scan_blanks else $$$ symbol end;
    63 
    64 fun scan_strict kind =
    65   scan_symbol kind @@@
    66     Symbol_Pos.!!! (fn () => err_prefix ^ "cartouche expected after " ^ print_kind kind)
    67       (Symbol_Pos.scan_cartouche err_prefix) >> pair kind;
    68 
    69 fun scan_permissive kind =
    70   scan_symbol kind -- Scan.option (Symbol_Pos.scan_cartouche err_prefix) >>
    71     (fn (ss, NONE) => (NONE, ss) | (_, SOME ss) => (SOME kind, ss));
    72 
    73 in
    74 
    75 val scan_comment = scan_strict Comment;
    76 val scan_cancel = scan_strict Cancel;
    77 val scan_latex = scan_strict Latex;
    78 val scan_marker = scan_strict Marker;
    79 
    80 val scan_inner = scan_comment || scan_cancel || scan_latex;
    81 val scan_outer = scan_inner || scan_marker;
    82 
    83 val scan_body =
    84   Scan.many1 (fn (s, _) => not (is_symbol s) andalso Symbol.not_eof s) >> pair NONE ||
    85   scan_permissive Comment || scan_permissive Cancel || scan_permissive Latex;
    86 
    87 fun read_body syms =
    88   (if exists (is_symbol o Symbol_Pos.symbol) syms then
    89     Scan.read Symbol_Pos.stopper (Scan.repeat scan_body) syms
    90   else NONE) |> the_default [(NONE, syms)];
    91 
    92 end;
    93 
    94 end;