# 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