src/Pure/General/comment.ML
changeset 67429 95877cc6630e
parent 67426 6311cf9dc943
child 67506 30233285270a
     1.1 --- a/src/Pure/General/comment.ML	Sun Jan 14 15:31:02 2018 +0100
     1.2 +++ b/src/Pure/General/comment.ML	Sun Jan 14 16:21:29 2018 +0100
     1.3 @@ -6,9 +6,11 @@
     1.4  
     1.5  signature COMMENT =
     1.6  sig
     1.7 -  datatype kind = Comment | Cancel
     1.8 +  datatype kind = Comment | Cancel | Latex
     1.9 +  val markup: kind -> Markup.T
    1.10    val scan_comment: (kind * Symbol_Pos.T list) scanner
    1.11    val scan_cancel: (kind * Symbol_Pos.T list) scanner
    1.12 +  val scan_latex: (kind * Symbol_Pos.T list) scanner
    1.13    val scan: (kind * Symbol_Pos.T list) scanner
    1.14    val read_body: Symbol_Pos.T list -> (kind option * Symbol_Pos.T list) list option
    1.15  end;
    1.16 @@ -18,14 +20,16 @@
    1.17  
    1.18  (* kinds *)
    1.19  
    1.20 -datatype kind = Comment | Cancel;
    1.21 +datatype kind = Comment | Cancel | Latex;
    1.22  
    1.23  val kinds =
    1.24 -  [(Comment, {symbol = Symbol.comment, blanks = true}),
    1.25 -   (Cancel, {symbol = Symbol.cancel, blanks = false})];
    1.26 +  [(Comment, {symbol = Symbol.comment, blanks = true, markup = Markup.language_document true}),
    1.27 +   (Cancel, {symbol = Symbol.cancel, blanks = false, markup = Markup.language_text true}),
    1.28 +   (Latex, {symbol = Symbol.latex, blanks = false, markup = Markup.language_latex true})];
    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 +val markup = #markup o get_kind;
    1.33  
    1.34  fun is_symbol sym = exists (fn (_, {symbol, ...}) => symbol = sym) kinds;
    1.35  
    1.36 @@ -41,7 +45,7 @@
    1.37  val scan_blanks = Scan.many (Symbol.is_blank o Symbol_Pos.symbol);
    1.38  
    1.39  fun scan_symbol kind =
    1.40 -  let val {blanks, symbol} = get_kind kind
    1.41 +  let val {blanks, symbol, ...} = get_kind kind
    1.42    in if blanks then $$$ symbol @@@ scan_blanks else $$$ symbol end;
    1.43  
    1.44  fun scan_strict kind =
    1.45 @@ -57,11 +61,12 @@
    1.46  
    1.47  val scan_comment = scan_strict Comment;
    1.48  val scan_cancel = scan_strict Cancel;
    1.49 -val scan = scan_comment || scan_cancel;
    1.50 +val scan_latex = scan_strict Latex;
    1.51 +val scan = scan_comment || scan_cancel || scan_latex;
    1.52  
    1.53  val scan_body =
    1.54    Scan.many1 (fn (s, _) => not (is_symbol s) andalso Symbol.not_eof s) >> pair NONE ||
    1.55 -  scan_permissive Comment || scan_permissive Cancel;
    1.56 +  scan_permissive Comment || scan_permissive Cancel || scan_permissive Latex;
    1.57  
    1.58  fun read_body syms =
    1.59    if exists (is_symbol o Symbol_Pos.symbol) syms then