--- 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 *)
--- 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;