# HG changeset patch
# User wenzelm
# Date 1392753007 -3600
# Node ID 88c40aff747dee1fad7a099ca19fbe2472fdb425
# Parent  7ac8f013321c0dd84185ad610926d52c973a5990
more markup;

diff -r 7ac8f013321c -r 88c40aff747d src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Tue Feb 18 20:37:45 2014 +0100
+++ b/src/Pure/PIDE/markup.ML	Tue Feb 18 20:50:07 2014 +0100
@@ -27,6 +27,7 @@
   val language_prop: T
   val language_ML: T
   val language_document: T
+  val language_text: T
   val bindingN: string val binding: T
   val entityN: string val entity: string -> string -> T
   val get_entity_kind: T -> string option
@@ -253,6 +254,7 @@
 
 val language_ML = language "ML";
 val language_document = language "document";
+val language_text = language "text";
 
 
 (* formal entities *)
diff -r 7ac8f013321c -r 88c40aff747d src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Tue Feb 18 20:37:45 2014 +0100
+++ b/src/Pure/Thy/thy_output.ML	Tue Feb 18 20:50:07 2014 +0100
@@ -470,6 +470,9 @@
 fun pretty_text ctxt =
   Pretty.chunks o map Pretty.str o map (tweak_line ctxt) o split_lines;
 
+fun pretty_text_report ctxt (s, pos) =
+  (Context_Position.report ctxt pos Markup.language_text; pretty_text ctxt s);
+
 fun pretty_term ctxt t = Syntax.pretty_term (Variable.auto_fixes t ctxt) t;
 
 fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of;
@@ -574,7 +577,7 @@
   basic_entity (Binding.name "typ") Args.typ_abbrev Syntax.pretty_typ #>
   basic_entity (Binding.name "class") (Scan.lift Args.name_inner_syntax) pretty_class #>
   basic_entity (Binding.name "type") (Scan.lift Args.name) pretty_type #>
-  basic_entity (Binding.name "text") (Scan.lift Args.name) pretty_text #>
+  basic_entity (Binding.name "text") (Scan.lift (Parse.position Args.name)) pretty_text_report #>
   basic_entities (Binding.name "prf") Attrib.thms (pretty_prf false) #>
   basic_entities (Binding.name "full_prf") Attrib.thms (pretty_prf true) #>
   basic_entity (Binding.name "theory") (Scan.lift (Parse.position Args.name)) pretty_theory);