src/Pure/General/comment.ML
author wenzelm
Sun Mar 10 21:12:29 2019 +0100 (3 months ago)
changeset 69891 def3ec9cdb7e
parent 67572 a93cf1d6ba87
child 69965 da5e7278286b
permissions -rw-r--r--
document markers are formal comments, and may thus occur anywhere in the command-span;
clarified Outer_Syntax.parse_span, Outer_Syntax.parse_text wrt. span structure;
tuned 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@67506
    10
  val 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@67506
    31
      markups = [Markup.language_document true]}),
wenzelm@67506
    32
   (Cancel,
wenzelm@67506
    33
     {symbol = Symbol.cancel, blanks = false,
wenzelm@67506
    34
      markups = [Markup.language_text true]}),
wenzelm@67506
    35
   (Latex,
wenzelm@67506
    36
     {symbol = Symbol.latex, blanks = false,
wenzelm@69891
    37
      markups = [Markup.language_latex true, Markup.no_words]}),
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@67506
    44
val markups = #markups o get_kind;
wenzelm@67425
    45
wenzelm@67425
    46
fun is_symbol sym = exists (fn (_, {symbol, ...}) => symbol = sym) kinds;
wenzelm@67425
    47
wenzelm@67425
    48
wenzelm@67425
    49
(* scan *)
wenzelm@67425
    50
wenzelm@67425
    51
local
wenzelm@67425
    52
wenzelm@67425
    53
open Basic_Symbol_Pos;
wenzelm@67425
    54
wenzelm@67425
    55
val err_prefix = "Error in formal comment: ";
wenzelm@67425
    56
wenzelm@67425
    57
val scan_blanks = Scan.many (Symbol.is_blank o Symbol_Pos.symbol);
wenzelm@67425
    58
wenzelm@67425
    59
fun scan_symbol kind =
wenzelm@67429
    60
  let val {blanks, symbol, ...} = get_kind kind
wenzelm@67425
    61
  in if blanks then $$$ symbol @@@ scan_blanks else $$$ symbol end;
wenzelm@67425
    62
wenzelm@67425
    63
fun scan_strict kind =
wenzelm@67425
    64
  scan_symbol kind @@@
wenzelm@67425
    65
    Symbol_Pos.!!! (fn () => err_prefix ^ "cartouche expected after " ^ print_kind kind)
wenzelm@67425
    66
      (Symbol_Pos.scan_cartouche err_prefix) >> pair kind;
wenzelm@67425
    67
wenzelm@67425
    68
fun scan_permissive kind =
wenzelm@67425
    69
  scan_symbol kind -- Scan.option (Symbol_Pos.scan_cartouche err_prefix) >>
wenzelm@67425
    70
    (fn (ss, NONE) => (NONE, ss) | (_, SOME ss) => (SOME kind, ss));
wenzelm@67425
    71
wenzelm@67425
    72
in
wenzelm@67425
    73
wenzelm@67425
    74
val scan_comment = scan_strict Comment;
wenzelm@67425
    75
val scan_cancel = scan_strict Cancel;
wenzelm@67429
    76
val scan_latex = scan_strict Latex;
wenzelm@69891
    77
val scan_marker = scan_strict Marker;
wenzelm@69891
    78
wenzelm@69891
    79
val scan_inner = scan_comment || scan_cancel || scan_latex;
wenzelm@69891
    80
val scan_outer = scan_inner || scan_marker;
wenzelm@67425
    81
wenzelm@67425
    82
val scan_body =
wenzelm@67425
    83
  Scan.many1 (fn (s, _) => not (is_symbol s) andalso Symbol.not_eof s) >> pair NONE ||
wenzelm@67429
    84
  scan_permissive Comment || scan_permissive Cancel || scan_permissive Latex;
wenzelm@67425
    85
wenzelm@67425
    86
fun read_body syms =
wenzelm@67572
    87
  (if exists (is_symbol o Symbol_Pos.symbol) syms then
wenzelm@67425
    88
    Scan.read Symbol_Pos.stopper (Scan.repeat scan_body) syms
wenzelm@67572
    89
  else NONE) |> the_default [(NONE, syms)];
wenzelm@67425
    90
wenzelm@67425
    91
end;
wenzelm@67425
    92
wenzelm@67425
    93
end;