src/Pure/PIDE/markup.ML
changeset 50715 8cfd585b9162
parent 50683 34b109c5324c
child 50781 a0f22c2d60cc
--- a/src/Pure/PIDE/markup.ML	Fri Jan 04 11:21:31 2013 +0100
+++ b/src/Pure/PIDE/markup.ML	Fri Jan 04 12:33:25 2013 +0100
@@ -120,6 +120,7 @@
   val no_reportN: string val no_report: T
   val badN: string val bad: T
   val intensifyN: string val intensify: T
+  val browserN: string
   val graphviewN: string
   val sendbackN: string
   val paddingN: string
@@ -382,6 +383,7 @@
 
 (* active areas *)
 
+val browserN = "browser"
 val graphviewN = "graphview";
 
 val sendbackN = "sendback";