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";