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