src/Pure/General/symbol_pos.ML
changeset 55106 080c0006e917
parent 55105 75815b3b38a1
child 55107 1a29ea173bf9
     1.1 --- a/src/Pure/General/symbol_pos.ML	Mon Jan 20 20:04:52 2014 +0100
     1.2 +++ b/src/Pure/General/symbol_pos.ML	Mon Jan 20 20:24:44 2014 +0100
     1.3 @@ -204,12 +204,14 @@
     1.4  in
     1.5  
     1.6  fun scan_comment err_prefix =
     1.7 -  $$$ "(" @@@ $$$ "*" @@@
     1.8 -    !!! (fn () => err_prefix ^ "missing end of comment") (scan_body @@@ $$$ "*" @@@ $$$ ")");
     1.9 +  Scan.ahead ($$ "(" -- $$ "*") |--
    1.10 +    !!! (fn () => err_prefix ^ "unclosed comment")
    1.11 +      ($$$ "(" @@@ $$$ "*" @@@ scan_body @@@ $$$ "*" @@@ $$$ ")");
    1.12  
    1.13  fun scan_comment_body err_prefix =
    1.14 -  $$$ "(" |-- $$$ "*" |--
    1.15 -    !!! (fn () => err_prefix ^ "missing end of comment") (scan_body --| $$$ "*" --| $$$ ")");
    1.16 +  Scan.ahead ($$ "(" -- $$ "*") |--
    1.17 +    !!! (fn () => err_prefix ^ "unclosed comment")
    1.18 +      ($$ "(" |-- $$ "*" |-- scan_body --| $$ "*" --| $$ ")");
    1.19  
    1.20  val recover_comment =
    1.21    $$$ "(" @@@ $$$ "*" @@@ scan_cmts;