src/Pure/General/comment.ML
changeset 67572 a93cf1d6ba87
parent 67571 f858fe5531ac
child 69891 def3ec9cdb7e
     1.1 --- a/src/Pure/General/comment.ML	Sat Feb 03 20:34:26 2018 +0100
     1.2 +++ b/src/Pure/General/comment.ML	Sat Feb 03 20:46:28 2018 +0100
     1.3 @@ -13,7 +13,7 @@
     1.4    val scan_cancel: (kind * Symbol_Pos.T list) scanner
     1.5    val scan_latex: (kind * Symbol_Pos.T list) scanner
     1.6    val scan: (kind * Symbol_Pos.T list) scanner
     1.7 -  val read_body: Symbol_Pos.T list -> (kind option * Symbol_Pos.T list) list option
     1.8 +  val read_body: Symbol_Pos.T list -> (kind option * Symbol_Pos.T list) list
     1.9  end;
    1.10  
    1.11  structure Comment: COMMENT =
    1.12 @@ -76,9 +76,9 @@
    1.13    scan_permissive Comment || scan_permissive Cancel || scan_permissive Latex;
    1.14  
    1.15  fun read_body syms =
    1.16 -  if exists (is_symbol o Symbol_Pos.symbol) syms then
    1.17 +  (if exists (is_symbol o Symbol_Pos.symbol) syms then
    1.18      Scan.read Symbol_Pos.stopper (Scan.repeat scan_body) syms
    1.19 -  else NONE;
    1.20 +  else NONE) |> the_default [(NONE, syms)];
    1.21  
    1.22  end;
    1.23