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;
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@67429
    10
  val markup: kind -> Markup.T
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@67429
    26
  [(Comment, {symbol = Symbol.comment, blanks = true, markup = Markup.language_document true}),
wenzelm@67429
    27
   (Cancel, {symbol = Symbol.cancel, blanks = false, markup = Markup.language_text true}),
wenzelm@67429
    28
   (Latex, {symbol = Symbol.latex, blanks = false, markup = Markup.language_latex true})];
wenzelm@67425
    29
wenzelm@67425
    30
val get_kind = the o AList.lookup (op =) kinds;
wenzelm@67425
    31
val print_kind = quote o #symbol o get_kind;
wenzelm@67429
    32
val markup = #markup o get_kind;
wenzelm@67425
    33
wenzelm@67425
    34
fun is_symbol sym = exists (fn (_, {symbol, ...}) => symbol = sym) kinds;
wenzelm@67425
    35
wenzelm@67425
    36
wenzelm@67425
    37
(* scan *)
wenzelm@67425
    38
wenzelm@67425
    39
local
wenzelm@67425
    40
wenzelm@67425
    41
open Basic_Symbol_Pos;
wenzelm@67425
    42
wenzelm@67425
    43
val err_prefix = "Error in formal comment: ";
wenzelm@67425
    44
wenzelm@67425
    45
val scan_blanks = Scan.many (Symbol.is_blank o Symbol_Pos.symbol);
wenzelm@67425
    46
wenzelm@67425
    47
fun scan_symbol kind =
wenzelm@67429
    48
  let val {blanks, symbol, ...} = get_kind kind
wenzelm@67425
    49
  in if blanks then $$$ symbol @@@ scan_blanks else $$$ symbol end;
wenzelm@67425
    50
wenzelm@67425
    51
fun scan_strict kind =
wenzelm@67425
    52
  scan_symbol kind @@@
wenzelm@67425
    53
    Symbol_Pos.!!! (fn () => err_prefix ^ "cartouche expected after " ^ print_kind kind)
wenzelm@67425
    54
      (Symbol_Pos.scan_cartouche err_prefix) >> pair kind;
wenzelm@67425
    55
wenzelm@67425
    56
fun scan_permissive kind =
wenzelm@67425
    57
  scan_symbol kind -- Scan.option (Symbol_Pos.scan_cartouche err_prefix) >>
wenzelm@67425
    58
    (fn (ss, NONE) => (NONE, ss) | (_, SOME ss) => (SOME kind, ss));
wenzelm@67425
    59
wenzelm@67425
    60
in
wenzelm@67425
    61
wenzelm@67425
    62
val scan_comment = scan_strict Comment;
wenzelm@67425
    63
val scan_cancel = scan_strict Cancel;
wenzelm@67429
    64
val scan_latex = scan_strict Latex;
wenzelm@67429
    65
val scan = scan_comment || scan_cancel || scan_latex;
wenzelm@67425
    66
wenzelm@67425
    67
val scan_body =
wenzelm@67425
    68
  Scan.many1 (fn (s, _) => not (is_symbol s) andalso Symbol.not_eof s) >> pair NONE ||
wenzelm@67429
    69
  scan_permissive Comment || scan_permissive Cancel || scan_permissive Latex;
wenzelm@67425
    70
wenzelm@67425
    71
fun read_body syms =
wenzelm@67425
    72
  if exists (is_symbol o Symbol_Pos.symbol) syms then
wenzelm@67425
    73
    Scan.read Symbol_Pos.stopper (Scan.repeat scan_body) syms
wenzelm@67425
    74
  else NONE;
wenzelm@67425
    75
wenzelm@67425
    76
end;
wenzelm@67425
    77
wenzelm@67425
    78
end;