# HG changeset patch
# User wenzelm
# Date 1189196025 -7200
# Node ID ea220faa69e77f871e168b8c0caee85d9af244ae
# Parent  e9edafca311c94888578ec7a75ebdc1fab99bc8b
added hilite markup;

diff -r e9edafca311c -r ea220faa69e7 src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Fri Sep 07 20:40:08 2007 +0200
+++ b/src/Pure/General/markup.ML	Fri Sep 07 22:13:45 2007 +0200
@@ -55,6 +55,7 @@
   val stateN: string val state: T
   val subgoalN: string val subgoal: T
   val sendbackN: string val sendback: T
+  val hiliteN: string val hilite: T
   val default_output: T -> output * output
   val add_mode: string -> (T -> output * output) -> unit
   val output: T -> output * output
@@ -155,6 +156,7 @@
 val (stateN, state) = markup "state";
 val (subgoalN, subgoal) = markup "subgoal";
 val (sendbackN, sendback) = markup "sendback";
+val (hiliteN, hilite) = markup "hilite";
 
 
 (* print mode operations *)
diff -r e9edafca311c -r ea220faa69e7 src/Pure/ProofGeneral/proof_general_emacs.ML
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Fri Sep 07 20:40:08 2007 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Fri Sep 07 22:13:45 2007 +0200
@@ -103,6 +103,7 @@
   (if name = Markup.promptN then ("", special "372")
     else if name = Markup.stateN then (special "366" ^ "\n", "\n" ^ special "367")
     else if name = Markup.sendbackN then (special "376", special "377")
+    else if name = Markup.hiliteN then (special "327", special "330")
     else ("", ""))
   |> (name <> Markup.promptN andalso print_mode_active "test_markup") ?
     (fn (bg, en) =>