# HG changeset patch # User wenzelm # Date 1112858808 -7200 # Node ID 5c5925dc4921884334e532a038426f84a808cbbd # Parent 7e7412fffc0c524e16ec0ea845e85be4785405f7 Scan.peek; diff -r 7e7412fffc0c -r 5c5925dc4921 src/Pure/Isar/isar_output.ML --- a/src/Pure/Isar/isar_output.ML Thu Apr 07 09:26:40 2005 +0200 +++ b/src/Pure/Isar/isar_output.ML Thu Apr 07 09:26:48 2005 +0200 @@ -257,7 +257,7 @@ fun parse_thy markup lex trs src = let val text = P.position P.text; - val token = Scan.depend (fn i => + val token = Scan.peek (fn i => (improper |-- markup Markup -- P.!!!! (improper |-- text --| improper_end) >> (fn (x, y) => (true, (SOME true, ((Latex.Markup (T.val_of x), y), i)))) || improper |-- markup MarkupEnv -- P.!!!! (improper |-- text --| improper_end) @@ -267,8 +267,7 @@ (improper -- markup Verbatim) |-- P.!!!! (improper |-- text --| improper_end) >> (fn y => (true, (NONE, ((Latex.Verbatim, y), i)))) || P.position (Scan.one T.not_eof) - >> (fn (x, pos) => (T.is_kind T.Command x, (SOME false, ((Latex.Basic x, ("", pos)), i))))) - >> pair i); + >> (fn (x, pos) => (T.is_kind T.Command x, (SOME false, ((Latex.Basic x, ("", pos)), i)))))); val body = Scan.any (not o fst andf not o #2 stopper); val section = body -- Scan.one fst -- body