src/Pure/General/comment.ML
changeset 67425 7d4a088dbc0e
child 67426 6311cf9dc943
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/General/comment.ML	Sun Jan 14 14:11:02 2018 +0100
     1.3 @@ -0,0 +1,73 @@
     1.4 +(*  Title:      Pure/General/comment.ML
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +Formal comments.
     1.8 +*)
     1.9 +
    1.10 +signature COMMENT =
    1.11 +sig
    1.12 +  datatype kind = Comment | Cancel
    1.13 +  val scan_comment: Symbol_Pos.T list -> (kind * Symbol_Pos.T list) * Symbol_Pos.T list
    1.14 +  val scan_cancel: Symbol_Pos.T list -> (kind * Symbol_Pos.T list) * Symbol_Pos.T list
    1.15 +  val scan: Symbol_Pos.T list -> (kind * Symbol_Pos.T list) * Symbol_Pos.T list
    1.16 +  val read_body: Symbol_Pos.T list -> (kind option * Symbol_Pos.T list) list option
    1.17 +end;
    1.18 +
    1.19 +structure Comment: COMMENT =
    1.20 +struct
    1.21 +
    1.22 +(* kinds *)
    1.23 +
    1.24 +datatype kind = Comment | Cancel;
    1.25 +
    1.26 +val kinds =
    1.27 +  [(Comment, {symbol = Symbol.comment, blanks = true}),
    1.28 +   (Cancel, {symbol = Symbol.cancel, blanks = false})];
    1.29 +
    1.30 +val get_kind = the o AList.lookup (op =) kinds;
    1.31 +val print_kind = quote o #symbol o get_kind;
    1.32 +
    1.33 +fun is_symbol sym = exists (fn (_, {symbol, ...}) => symbol = sym) kinds;
    1.34 +
    1.35 +
    1.36 +(* scan *)
    1.37 +
    1.38 +local
    1.39 +
    1.40 +open Basic_Symbol_Pos;
    1.41 +
    1.42 +val err_prefix = "Error in formal comment: ";
    1.43 +
    1.44 +val scan_blanks = Scan.many (Symbol.is_blank o Symbol_Pos.symbol);
    1.45 +
    1.46 +fun scan_symbol kind =
    1.47 +  let val {blanks, symbol} = get_kind kind
    1.48 +  in if blanks then $$$ symbol @@@ scan_blanks else $$$ symbol end;
    1.49 +
    1.50 +fun scan_strict kind =
    1.51 +  scan_symbol kind @@@
    1.52 +    Symbol_Pos.!!! (fn () => err_prefix ^ "cartouche expected after " ^ print_kind kind)
    1.53 +      (Symbol_Pos.scan_cartouche err_prefix) >> pair kind;
    1.54 +
    1.55 +fun scan_permissive kind =
    1.56 +  scan_symbol kind -- Scan.option (Symbol_Pos.scan_cartouche err_prefix) >>
    1.57 +    (fn (ss, NONE) => (NONE, ss) | (_, SOME ss) => (SOME kind, ss));
    1.58 +
    1.59 +in
    1.60 +
    1.61 +val scan_comment = scan_strict Comment;
    1.62 +val scan_cancel = scan_strict Cancel;
    1.63 +val scan = scan_comment || scan_cancel;
    1.64 +
    1.65 +val scan_body =
    1.66 +  Scan.many1 (fn (s, _) => not (is_symbol s) andalso Symbol.not_eof s) >> pair NONE ||
    1.67 +  scan_permissive Comment || scan_permissive Cancel;
    1.68 +
    1.69 +fun read_body syms =
    1.70 +  if exists (is_symbol o Symbol_Pos.symbol) syms then
    1.71 +    Scan.read Symbol_Pos.stopper (Scan.repeat scan_body) syms
    1.72 +  else NONE;
    1.73 +
    1.74 +end;
    1.75 +
    1.76 +end;