src/Pure/General/markup.ML

   val commandspanN: string val commandspan: string -> T
   val promptN: string val prompt: T
   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
   val enclose: T -> output -> output
 end;

 
 val (promptN, prompt) = markup "prompt";
 val (stateN, state) = markup "state";
 val (subgoalN, subgoal) = markup "subgoal";
 val (sendbackN, sendback) = markup "sendback";
+val (hiliteN, hilite) = markup "hilite";
 
 
 (* print mode operations *)
 
 fun default_output (_: T) = ("", "");