# HG changeset patch # User wenzelm # Date 1517687188 -3600 # Node ID a93cf1d6ba87e1a227aa80bdacf4443bf795efc0 # Parent f858fe5531ac2086df270b3db295d31e769538cb clarified signature; diff -r f858fe5531ac -r a93cf1d6ba87 src/Pure/General/comment.ML --- a/src/Pure/General/comment.ML Sat Feb 03 20:34:26 2018 +0100 +++ b/src/Pure/General/comment.ML Sat Feb 03 20:46:28 2018 +0100 @@ -13,7 +13,7 @@ val scan_cancel: (kind * Symbol_Pos.T list) scanner val scan_latex: (kind * Symbol_Pos.T list) scanner val scan: (kind * Symbol_Pos.T list) scanner - val read_body: Symbol_Pos.T list -> (kind option * Symbol_Pos.T list) list option + val read_body: Symbol_Pos.T list -> (kind option * Symbol_Pos.T list) list end; structure Comment: COMMENT = @@ -76,9 +76,9 @@ scan_permissive Comment || scan_permissive Cancel || scan_permissive Latex; fun read_body syms = - if exists (is_symbol o Symbol_Pos.symbol) syms then + (if exists (is_symbol o Symbol_Pos.symbol) syms then Scan.read Symbol_Pos.stopper (Scan.repeat scan_body) syms - else NONE; + else NONE) |> the_default [(NONE, syms)]; end; diff -r f858fe5531ac -r a93cf1d6ba87 src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Sat Feb 03 20:34:26 2018 +0100 +++ b/src/Pure/Thy/thy_output.ML Sat Feb 03 20:46:28 2018 +0100 @@ -60,9 +60,7 @@ SOME kind => output_comment ctxt (kind, syms) | NONE => [Latex.symbols syms]) and output_document_text ctxt syms = - (case Comment.read_body syms of - SOME res => maps (output_comment_document ctxt) res - | NONE => [Latex.symbols syms]) + Comment.read_body syms |> maps (output_comment_document ctxt) and output_document ctxt {markdown} source = let val pos = Input.pos_of source; @@ -122,9 +120,9 @@ in fun output_body ctxt antiq bg en syms = - (case Comment.read_body syms of - SOME res => maps (output_comment_symbols ctxt {antiq = antiq}) res - | NONE => output_symbols syms) |> Latex.enclose_body bg en + Comment.read_body syms + |> maps (output_comment_symbols ctxt {antiq = antiq}) + |> Latex.enclose_body bg en and output_token ctxt tok = let fun output antiq bg en = @@ -148,7 +146,7 @@ output_body ctxt false "" "" (Symbol_Pos.explode (s, Position.none)); fun check_comments ctxt = - Comment.read_body #> (Option.app o List.app) (fn (comment, syms) => + Comment.read_body #> List.app (fn (comment, syms) => let val pos = #1 (Symbol_Pos.range syms); val _ =