fixed command prompt (was broken due to P.tags);
authorwenzelm
Thu, 18 Aug 2005 12:07:33 +0200
changeset 17118 1ff59b7b35b7
parent 17117 e2bed9e82454
child 17119 b241ba3eb4db
fixed command prompt (was broken due to P.tags);
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));