markup for prose words within formal comments;

--- a/src/Pure/PIDE/markup.ML	Fri Apr 11 23:26:31 2014 +0200
+++ b/src/Pure/PIDE/markup.ML	Sat Apr 12 17:46:54 2014 +0200
@@ -62,6 +62,7 @@
   val breakN: string val break: int -> T
   val fbreakN: string val fbreak: T
   val itemN: string val item: T
+  val wordsN: string val words: T
   val hiddenN: string val hidden: T
   val system_optionN: string
   val theoryN: string
@@ -354,7 +355,9 @@
 val (itemN, item) = markup_elem "item";
 
 
-(* hidden text *)
+(* text properties *)
+
+val (wordsN, words) = markup_elem "words";
 
 val (hiddenN, hidden) = markup_elem "hidden";
 

--- a/src/Pure/PIDE/markup.scala	Fri Apr 11 23:26:31 2014 +0200
+++ b/src/Pure/PIDE/markup.scala	Sat Apr 12 17:46:54 2014 +0200
@@ -137,7 +137,9 @@
   val SEPARATOR = "separator"
 
 
-  /* hidden text */
+  /* text properties */
+
+  val WORDS = "words"
 
   val HIDDEN = "hidden"
 

--- a/src/Pure/Thy/thy_output.ML	Fri Apr 11 23:26:31 2014 +0200
+++ b/src/Pure/Thy/thy_output.ML	Sat Apr 12 17:46:54 2014 +0200
@@ -24,7 +24,6 @@
   val integer: string -> int
   datatype markup = Markup | MarkupEnv | Verbatim
   val eval_antiq: Scan.lexicon -> Toplevel.state -> Antiquote.antiq -> string
-  val eval_antiquote: Scan.lexicon -> Toplevel.state -> Symbol_Pos.text * Position.T -> string
   val check_text: Symbol_Pos.source -> Toplevel.state -> unit
   val present_thy: Scan.lexicon -> (string -> string list) -> (markup -> string -> bool) ->
     (Toplevel.transition * Toplevel.state) list -> Token.T list -> Buffer.T
@@ -157,7 +156,7 @@
 end;
 
 
-(* eval_antiquote *)
+(* eval_antiq *)
 
 fun eval_antiq lex state ((ss, {range = (pos, _), ...}): Antiquote.antiq) =
   let
@@ -169,18 +168,25 @@
     val print_modes = space_explode "," (Config.get print_ctxt modes) @ Latex.modes;
   in Print_Mode.with_modes print_modes (fn () => cmd print_ctxt) () end;
 
+
+(* check_text *)
+
 fun eval_antiquote lex state (txt, pos) =
   let
+    fun words (Antiquote.Text ss) = [(#1 (Symbol_Pos.range ss), Markup.words)]
+      | words (Antiquote.Antiq _) = [];
+
     fun expand (Antiquote.Text ss) = Symbol_Pos.content ss
       | expand (Antiquote.Antiq antiq) = eval_antiq lex state antiq;
+
     val ants = Antiquote.read (Symbol_Pos.explode (txt, pos), pos);
+    val _ = Position.reports (maps words ants);
   in
     if Toplevel.is_toplevel state andalso not (forall Antiquote.is_text ants) then
       error ("Unknown context -- cannot expand document antiquotations" ^ Position.here pos)
     else implode (map expand ants)
   end;
 
-
 fun check_text {delimited, text, pos} state =
  (Position.report pos (Markup.language_document delimited);
   if Toplevel.is_skipped_proof state then ()

--- a/src/Tools/jEdit/src/rendering.scala	Fri Apr 11 23:26:31 2014 +0200
+++ b/src/Tools/jEdit/src/rendering.scala	Sat Apr 12 17:46:54 2014 +0200
@@ -136,6 +136,8 @@
       Markup.CARTOUCHE, Markup.COMMENT, Markup.LANGUAGE,
       Markup.ML_STRING, Markup.ML_COMMENT)
 
+  private val prose_words_elements = Document.Elements(Markup.WORDS)
+
   private val highlight_elements =
     Document.Elements(Markup.LANGUAGE, Markup.ML_TYPING, Markup.TOKEN_RANGE,
       Markup.ENTITY, Markup.PATH, Markup.URL, Markup.SORTING,
@@ -283,6 +285,12 @@
       }).headOption.map(_.info)
 
 
+  /* prose words */
+
+  def prose_words(range: Text.Range): List[Text.Range] =
+    snapshot.select(range, Rendering.prose_words_elements, _ => _ => Some(())).map(_.range)
+
+
   /* command status overview */
 
   def overview_limit: Int = options.int("jedit_text_overview_limit")