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