added hilite markup;

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

--- 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) =>