# HG changeset patch
# User wenzelm
# Date 1184078704 -7200
# Node ID 1716f19e7d25d53968446c5b13d70cb119311edc
# Parent  fb1102e98cd40bf6788f2bf62e83c31f74f570de
Markup.output;
removed no_state markup -- produce empty state;

diff -r fb1102e98cd4 -r 1716f19e7d25 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Tue Jul 10 16:45:03 2007 +0200
+++ b/src/Pure/Isar/toplevel.ML	Tue Jul 10 16:45:04 2007 +0200
@@ -213,16 +213,14 @@
   |> Pretty.chunks |> Pretty.writeln;
 
 fun print_state prf_only state =
-  let val prts =
-    (case try node_of state of
-      NONE => []
-    | SOME (Theory (gthy, _)) => if prf_only then [] else pretty_context gthy
-    | SOME (Proof (prf, _)) =>
-        Proof.pretty_state (ProofHistory.position prf) (ProofHistory.current prf)
-    | SOME (SkipProof (h, _)) =>
-        [Pretty.str ("skipped proof: depth " ^ string_of_int (History.current h))])
-  in Pretty.markup_chunks (if null prts then Markup.no_state else Markup.state) prts end
-  |> Pretty.writeln;
+  (case try node_of state of
+    NONE => []
+  | SOME (Theory (gthy, _)) => if prf_only then [] else pretty_context gthy
+  | SOME (Proof (prf, _)) =>
+      Proof.pretty_state (ProofHistory.position prf) (ProofHistory.current prf)
+  | SOME (SkipProof (h, _)) =>
+      [Pretty.str ("skipped proof: depth " ^ string_of_int (History.current h))])
+  |> Pretty.markup_chunks Markup.state |> Pretty.writeln;
 
 
 
@@ -754,7 +752,7 @@
 
 fun raw_loop src =
   let val prompt =
-    Output.escape (Source.default_prompt |> (Pretty.mode_markup Markup.prompt |-> enclose))
+    Output.escape ((Markup.output Markup.prompt |-> enclose) Source.default_prompt)
   in
     (case get_interrupt (Source.set_prompt prompt src) of
       NONE => (writeln "\nInterrupt."; raw_loop src)