fixed command prompt (was broken due to P.tags);
authorwenzelm
Thu Aug 18 12:07:33 2005 +0200 (2005-08-18)
changeset 171181ff59b7b35b7
parent 17117 e2bed9e82454
child 17119 b241ba3eb4db
fixed command prompt (was broken due to P.tags);
src/Pure/Isar/outer_syntax.ML
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Thu Aug 18 11:59:17 2005 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Thu Aug 18 12:07:33 2005 +0200
     1.3 @@ -76,7 +76,7 @@
     1.4  fun body cmd do_trace (name, _) =
     1.5    (case cmd name of
     1.6      SOME (int_only, parse) =>
     1.7 -      P.!!! (Scan.prompt (name ^ "# ") (trace do_trace parse >> pair int_only))
     1.8 +      P.!!! (Scan.prompt (name ^ "# ") (trace do_trace (P.tags |-- parse) >> pair int_only))
     1.9    | NONE => sys_error ("no parser for outer syntax command " ^ quote name));
    1.10  
    1.11  in
    1.12 @@ -84,7 +84,7 @@
    1.13  fun command do_terminate do_trace cmd =
    1.14    P.semicolon >> K NONE ||
    1.15    P.sync >> K NONE ||
    1.16 -  ((P.position P.command --| P.tags) :-- body cmd do_trace) --| terminate do_terminate
    1.17 +  (P.position P.command :-- body cmd do_trace) --| terminate do_terminate
    1.18      >> (fn ((name, pos), (int_only, f)) =>
    1.19        SOME (Toplevel.empty |> Toplevel.name name |> Toplevel.position pos |>
    1.20          Toplevel.interactive int_only |> f));