# HG changeset patch
# User wenzelm
# Date 1124359653 -7200
# Node ID 1ff59b7b35b7f69733db5ca62dad3078da897d92
# Parent  e2bed9e8245493853c8e5db8a8007f825006f404
fixed command prompt (was broken due to P.tags);

diff -r e2bed9e82454 -r 1ff59b7b35b7 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Thu Aug 18 11:59:17 2005 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Thu Aug 18 12:07:33 2005 +0200
@@ -76,7 +76,7 @@
 fun body cmd do_trace (name, _) =
   (case cmd name of
     SOME (int_only, parse) =>
-      P.!!! (Scan.prompt (name ^ "# ") (trace do_trace parse >> pair int_only))
+      P.!!! (Scan.prompt (name ^ "# ") (trace do_trace (P.tags |-- parse) >> pair int_only))
   | NONE => sys_error ("no parser for outer syntax command " ^ quote name));
 
 in
@@ -84,7 +84,7 @@
 fun command do_terminate do_trace cmd =
   P.semicolon >> K NONE ||
   P.sync >> K NONE ||
-  ((P.position P.command --| P.tags) :-- body cmd do_trace) --| terminate do_terminate
+  (P.position P.command :-- body cmd do_trace) --| terminate do_terminate
     >> (fn ((name, pos), (int_only, f)) =>
       SOME (Toplevel.empty |> Toplevel.name name |> Toplevel.position pos |>
         Toplevel.interactive int_only |> f));