# HG changeset patch
# User wenzelm
# Date 1184078705 -7200
# Node ID 58ca991e0702742c5d152251702b1eeb80eecf73
# Parent  1716f19e7d25d53968446c5b13d70cb119311edc
removed no_state markup -- produce empty state;
Markup.add_mode;

diff -r 1716f19e7d25 -r 58ca991e0702 src/Pure/ProofGeneral/proof_general_emacs.ML
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Tue Jul 10 16:45:04 2007 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Tue Jul 10 16:45:05 2007 +0200
@@ -100,15 +100,14 @@
 
 fun proof_general_markup (name, props) =
   (if name = Markup.promptN then ("", special "372")
-    else if name = Markup.no_stateN orelse name = Markup.stateN
-    then (special "366" ^ "\n", "\n" ^ special "367")
+    else if name = Markup.stateN then (special "366" ^ "\n", "\n" ^ special "367")
     else ("", ""))
   |> (name <> Markup.promptN andalso print_mode_active "test_markup") ?
     (fn (bg, en) =>
       (bg ^ enclose "<" ">" (space_implode " " (name :: map XML.attribute props)),
         enclose "</" ">" name ^ en));
 
-val _ = Pretty.add_mode proof_generalN Pretty.default_indent proof_general_markup;
+val _ = Markup.add_mode proof_generalN proof_general_markup;
 
 
 (* messages and notification *)
diff -r 1716f19e7d25 -r 58ca991e0702 src/Pure/ProofGeneral/proof_general_pgip.ML
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue Jul 10 16:45:04 2007 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue Jul 10 16:45:05 2007 +0200
@@ -270,13 +270,12 @@
   in split_markup (output_pgips [Proofstate {pgml=pgml}]) end;
 
 fun proof_general_markup (name, props) =
-  (if name = Markup.no_stateN then (output_pgips [Cleardisplay {area=Display}], "")
-    else if name = Markup.stateN then statedisplay_markup ()
+  (if name = Markup.stateN then statedisplay_markup ()
     else ("", ""));
 
 in
 
-val _ = Pretty.add_mode proof_generalN Pretty.default_indent proof_general_markup;
+val _ = Markup.add_mode proof_generalN proof_general_markup;
 
 end;