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