src/Pure/Isar/outer_lex.ML
changeset 24022 ab76c73b3b58
parent 23788 54ce229dc858
child 24577 c6acb6d79757
     1.1 --- a/src/Pure/Isar/outer_lex.ML	Sat Jul 28 20:40:26 2007 +0200
     1.2 +++ b/src/Pure/Isar/outer_lex.ML	Sat Jul 28 20:40:27 2007 +0200
     1.3 @@ -300,7 +300,7 @@
     1.4  
     1.5  fun scan (lex1, lex2) =
     1.6    let
     1.7 -    val scanner = Scan.state :-- (fn pos =>
     1.8 +    val scanner = Scan.state :|-- (fn pos =>
     1.9        let
    1.10          fun token k x = Token (pos, (k, x));
    1.11          fun sync _ = token Sync Symbol.sync;
    1.12 @@ -323,7 +323,7 @@
    1.13              Syntax.scan_tvar >> token TypeVar ||
    1.14              Syntax.scan_nat >> token Nat ||
    1.15              scan_symid >> token SymIdent))
    1.16 -      end) >> #2;
    1.17 +      end);
    1.18    in !! (lex_err (fn cs => "bad input " ^ quote (Symbol.beginning 10 cs))) scanner end;
    1.19  
    1.20  
    1.21 @@ -333,8 +333,8 @@
    1.22  
    1.23  val is_junk = (not o Symbol.is_blank) andf Symbol.is_regular;
    1.24  
    1.25 -fun recover msg = Scan.state :-- (fn pos =>
    1.26 -  keep_line (Scan.many is_junk) >> (fn xs => [Token (pos, (Error msg, implode xs))])) >> #2;
    1.27 +fun recover msg = Scan.state :|-- (fn pos =>
    1.28 +  keep_line (Scan.many is_junk) >> (fn xs => [Token (pos, (Error msg, implode xs))]));
    1.29  
    1.30  in
    1.31