Scan.peek;
authorwenzelm
Thu Apr 07 09:26:48 2005 +0200 (2005-04-07 ago)
changeset 156665c5925dc4921
parent 15665 7e7412fffc0c
child 15667 b7bdc1651198
Scan.peek;
src/Pure/Isar/isar_output.ML
     1.1 --- a/src/Pure/Isar/isar_output.ML	Thu Apr 07 09:26:40 2005 +0200
     1.2 +++ b/src/Pure/Isar/isar_output.ML	Thu Apr 07 09:26:48 2005 +0200
     1.3 @@ -257,7 +257,7 @@
     1.4  fun parse_thy markup lex trs src =
     1.5    let
     1.6      val text = P.position P.text;
     1.7 -    val token = Scan.depend (fn i =>
     1.8 +    val token = Scan.peek (fn i =>
     1.9       (improper |-- markup Markup -- P.!!!! (improper |-- text --| improper_end)
    1.10          >> (fn (x, y) => (true, (SOME true, ((Latex.Markup (T.val_of x), y), i)))) ||
    1.11        improper |-- markup MarkupEnv -- P.!!!! (improper |-- text --| improper_end)
    1.12 @@ -267,8 +267,7 @@
    1.13        (improper -- markup Verbatim) |-- P.!!!! (improper |-- text --| improper_end)
    1.14          >> (fn y => (true, (NONE, ((Latex.Verbatim, y), i)))) ||
    1.15        P.position (Scan.one T.not_eof)
    1.16 -        >> (fn (x, pos) => (T.is_kind T.Command x, (SOME false, ((Latex.Basic x, ("", pos)), i)))))
    1.17 -      >> pair i);
    1.18 +        >> (fn (x, pos) => (T.is_kind T.Command x, (SOME false, ((Latex.Basic x, ("", pos)), i))))));
    1.19  
    1.20      val body = Scan.any (not o fst andf not o #2 stopper);
    1.21      val section = body -- Scan.one fst -- body