src/Pure/General/comment.ML
author wenzelm
Sun Jan 14 14:11:02 2018 +0100 (17 months ago)
changeset 67425 7d4a088dbc0e
child 67426 6311cf9dc943
permissions -rw-r--r--
clarified modules: uniform notion of formal comments;
     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
    10   val scan_comment: Symbol_Pos.T list -> (kind * Symbol_Pos.T list) * Symbol_Pos.T list
    11   val scan_cancel: Symbol_Pos.T list -> (kind * Symbol_Pos.T list) * Symbol_Pos.T list
    12   val scan: Symbol_Pos.T list -> (kind * Symbol_Pos.T list) * Symbol_Pos.T list
    13   val read_body: Symbol_Pos.T list -> (kind option * Symbol_Pos.T list) list option
    14 end;
    15 
    16 structure Comment: COMMENT =
    17 struct
    18 
    19 (* kinds *)
    20 
    21 datatype kind = Comment | Cancel;
    22 
    23 val kinds =
    24   [(Comment, {symbol = Symbol.comment, blanks = true}),
    25    (Cancel, {symbol = Symbol.cancel, blanks = false})];
    26 
    27 val get_kind = the o AList.lookup (op =) kinds;
    28 val print_kind = quote o #symbol o get_kind;
    29 
    30 fun is_symbol sym = exists (fn (_, {symbol, ...}) => symbol = sym) kinds;
    31 
    32 
    33 (* scan *)
    34 
    35 local
    36 
    37 open Basic_Symbol_Pos;
    38 
    39 val err_prefix = "Error in formal comment: ";
    40 
    41 val scan_blanks = Scan.many (Symbol.is_blank o Symbol_Pos.symbol);
    42 
    43 fun scan_symbol kind =
    44   let val {blanks, symbol} = get_kind kind
    45   in if blanks then $$$ symbol @@@ scan_blanks else $$$ symbol end;
    46 
    47 fun scan_strict kind =
    48   scan_symbol kind @@@
    49     Symbol_Pos.!!! (fn () => err_prefix ^ "cartouche expected after " ^ print_kind kind)
    50       (Symbol_Pos.scan_cartouche err_prefix) >> pair kind;
    51 
    52 fun scan_permissive kind =
    53   scan_symbol kind -- Scan.option (Symbol_Pos.scan_cartouche err_prefix) >>
    54     (fn (ss, NONE) => (NONE, ss) | (_, SOME ss) => (SOME kind, ss));
    55 
    56 in
    57 
    58 val scan_comment = scan_strict Comment;
    59 val scan_cancel = scan_strict Cancel;
    60 val scan = scan_comment || scan_cancel;
    61 
    62 val scan_body =
    63   Scan.many1 (fn (s, _) => not (is_symbol s) andalso Symbol.not_eof s) >> pair NONE ||
    64   scan_permissive Comment || scan_permissive Cancel;
    65 
    66 fun read_body syms =
    67   if exists (is_symbol o Symbol_Pos.symbol) syms then
    68     Scan.read Symbol_Pos.stopper (Scan.repeat scan_body) syms
    69   else NONE;
    70 
    71 end;
    72 
    73 end;