src/Pure/General/markup.ML
changeset 24555 ea220faa69e7
parent 24289 bfd59eb6e24e
child 24612 d1b315bdb8d7
--- 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 *)